Proof of Theorem mulsval2lem
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqeq1 2740 | . . . 4
⊢ (𝑎 = 𝑏 → (𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞)) ↔ 𝑏 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞)))) | 
| 2 | 1 | 2rexbidv 3221 | . . 3
⊢ (𝑎 = 𝑏 → (∃𝑝 ∈ 𝑋 ∃𝑞 ∈ 𝑌 𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞)) ↔ ∃𝑝 ∈ 𝑋 ∃𝑞 ∈ 𝑌 𝑏 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞)))) | 
| 3 |  | oveq1 7439 | . . . . . . 7
⊢ (𝑝 = 𝑟 → (𝑝 ·s 𝐵) = (𝑟 ·s 𝐵)) | 
| 4 | 3 | oveq1d 7447 | . . . . . 6
⊢ (𝑝 = 𝑟 → ((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) = ((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑞))) | 
| 5 |  | oveq1 7439 | . . . . . 6
⊢ (𝑝 = 𝑟 → (𝑝 ·s 𝑞) = (𝑟 ·s 𝑞)) | 
| 6 | 4, 5 | oveq12d 7450 | . . . . 5
⊢ (𝑝 = 𝑟 → (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞)) = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑟 ·s 𝑞))) | 
| 7 | 6 | eqeq2d 2747 | . . . 4
⊢ (𝑝 = 𝑟 → (𝑏 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞)) ↔ 𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑟 ·s 𝑞)))) | 
| 8 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑞 = 𝑠 → (𝐴 ·s 𝑞) = (𝐴 ·s 𝑠)) | 
| 9 | 8 | oveq2d 7448 | . . . . . 6
⊢ (𝑞 = 𝑠 → ((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑞)) = ((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠))) | 
| 10 |  | oveq2 7440 | . . . . . 6
⊢ (𝑞 = 𝑠 → (𝑟 ·s 𝑞) = (𝑟 ·s 𝑠)) | 
| 11 | 9, 10 | oveq12d 7450 | . . . . 5
⊢ (𝑞 = 𝑠 → (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑟 ·s 𝑞)) = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))) | 
| 12 | 11 | eqeq2d 2747 | . . . 4
⊢ (𝑞 = 𝑠 → (𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑟 ·s 𝑞)) ↔ 𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠)))) | 
| 13 | 7, 12 | cbvrex2vw 3241 | . . 3
⊢
(∃𝑝 ∈
𝑋 ∃𝑞 ∈ 𝑌 𝑏 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞)) ↔ ∃𝑟 ∈ 𝑋 ∃𝑠 ∈ 𝑌 𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))) | 
| 14 | 2, 13 | bitrdi 287 | . 2
⊢ (𝑎 = 𝑏 → (∃𝑝 ∈ 𝑋 ∃𝑞 ∈ 𝑌 𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞)) ↔ ∃𝑟 ∈ 𝑋 ∃𝑠 ∈ 𝑌 𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠)))) | 
| 15 | 14 | cbvabv 2811 | 1
⊢ {𝑎 ∣ ∃𝑝 ∈ 𝑋 ∃𝑞 ∈ 𝑌 𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} = {𝑏 ∣ ∃𝑟 ∈ 𝑋 ∃𝑠 ∈ 𝑌 𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))} |