Proof of Theorem ip2eq
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | oveq2 7439 | . . 3
⊢ (𝐴 = 𝐵 → (𝑥 , 𝐴) = (𝑥 , 𝐵)) | 
| 2 | 1 | ralrimivw 3150 | . 2
⊢ (𝐴 = 𝐵 → ∀𝑥 ∈ 𝑉 (𝑥 , 𝐴) = (𝑥 , 𝐵)) | 
| 3 |  | phllmod 21648 | . . . . 5
⊢ (𝑊 ∈ PreHil → 𝑊 ∈ LMod) | 
| 4 |  | ip2eq.v | . . . . . 6
⊢ 𝑉 = (Base‘𝑊) | 
| 5 |  | eqid 2737 | . . . . . 6
⊢
(-g‘𝑊) = (-g‘𝑊) | 
| 6 | 4, 5 | lmodvsubcl 20905 | . . . . 5
⊢ ((𝑊 ∈ LMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴(-g‘𝑊)𝐵) ∈ 𝑉) | 
| 7 | 3, 6 | syl3an1 1164 | . . . 4
⊢ ((𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴(-g‘𝑊)𝐵) ∈ 𝑉) | 
| 8 |  | oveq1 7438 | . . . . . 6
⊢ (𝑥 = (𝐴(-g‘𝑊)𝐵) → (𝑥 , 𝐴) = ((𝐴(-g‘𝑊)𝐵) , 𝐴)) | 
| 9 |  | oveq1 7438 | . . . . . 6
⊢ (𝑥 = (𝐴(-g‘𝑊)𝐵) → (𝑥 , 𝐵) = ((𝐴(-g‘𝑊)𝐵) , 𝐵)) | 
| 10 | 8, 9 | eqeq12d 2753 | . . . . 5
⊢ (𝑥 = (𝐴(-g‘𝑊)𝐵) → ((𝑥 , 𝐴) = (𝑥 , 𝐵) ↔ ((𝐴(-g‘𝑊)𝐵) , 𝐴) = ((𝐴(-g‘𝑊)𝐵) , 𝐵))) | 
| 11 | 10 | rspcv 3618 | . . . 4
⊢ ((𝐴(-g‘𝑊)𝐵) ∈ 𝑉 → (∀𝑥 ∈ 𝑉 (𝑥 , 𝐴) = (𝑥 , 𝐵) → ((𝐴(-g‘𝑊)𝐵) , 𝐴) = ((𝐴(-g‘𝑊)𝐵) , 𝐵))) | 
| 12 | 7, 11 | syl 17 | . . 3
⊢ ((𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (∀𝑥 ∈ 𝑉 (𝑥 , 𝐴) = (𝑥 , 𝐵) → ((𝐴(-g‘𝑊)𝐵) , 𝐴) = ((𝐴(-g‘𝑊)𝐵) , 𝐵))) | 
| 13 |  | simp1 1137 | . . . . . . 7
⊢ ((𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → 𝑊 ∈ PreHil) | 
| 14 |  | simp2 1138 | . . . . . . 7
⊢ ((𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ 𝑉) | 
| 15 |  | simp3 1139 | . . . . . . 7
⊢ ((𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ 𝑉) | 
| 16 |  | eqid 2737 | . . . . . . . 8
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) | 
| 17 |  | ip2eq.h | . . . . . . . 8
⊢  , =
(·𝑖‘𝑊) | 
| 18 |  | eqid 2737 | . . . . . . . 8
⊢
(-g‘(Scalar‘𝑊)) =
(-g‘(Scalar‘𝑊)) | 
| 19 | 16, 17, 4, 5, 18 | ipsubdi 21661 | . . . . . . 7
⊢ ((𝑊 ∈ PreHil ∧ ((𝐴(-g‘𝑊)𝐵) ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → ((𝐴(-g‘𝑊)𝐵) , (𝐴(-g‘𝑊)𝐵)) = (((𝐴(-g‘𝑊)𝐵) , 𝐴)(-g‘(Scalar‘𝑊))((𝐴(-g‘𝑊)𝐵) , 𝐵))) | 
| 20 | 13, 7, 14, 15, 19 | syl13anc 1374 | . . . . . 6
⊢ ((𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ((𝐴(-g‘𝑊)𝐵) , (𝐴(-g‘𝑊)𝐵)) = (((𝐴(-g‘𝑊)𝐵) , 𝐴)(-g‘(Scalar‘𝑊))((𝐴(-g‘𝑊)𝐵) , 𝐵))) | 
| 21 | 20 | eqeq1d 2739 | . . . . 5
⊢ ((𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (((𝐴(-g‘𝑊)𝐵) , (𝐴(-g‘𝑊)𝐵)) =
(0g‘(Scalar‘𝑊)) ↔ (((𝐴(-g‘𝑊)𝐵) , 𝐴)(-g‘(Scalar‘𝑊))((𝐴(-g‘𝑊)𝐵) , 𝐵)) =
(0g‘(Scalar‘𝑊)))) | 
| 22 |  | eqid 2737 | . . . . . . 7
⊢
(0g‘(Scalar‘𝑊)) =
(0g‘(Scalar‘𝑊)) | 
| 23 |  | eqid 2737 | . . . . . . 7
⊢
(0g‘𝑊) = (0g‘𝑊) | 
| 24 | 16, 17, 4, 22, 23 | ipeq0 21656 | . . . . . 6
⊢ ((𝑊 ∈ PreHil ∧ (𝐴(-g‘𝑊)𝐵) ∈ 𝑉) → (((𝐴(-g‘𝑊)𝐵) , (𝐴(-g‘𝑊)𝐵)) =
(0g‘(Scalar‘𝑊)) ↔ (𝐴(-g‘𝑊)𝐵) = (0g‘𝑊))) | 
| 25 | 13, 7, 24 | syl2anc 584 | . . . . 5
⊢ ((𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (((𝐴(-g‘𝑊)𝐵) , (𝐴(-g‘𝑊)𝐵)) =
(0g‘(Scalar‘𝑊)) ↔ (𝐴(-g‘𝑊)𝐵) = (0g‘𝑊))) | 
| 26 | 21, 25 | bitr3d 281 | . . . 4
⊢ ((𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ((((𝐴(-g‘𝑊)𝐵) , 𝐴)(-g‘(Scalar‘𝑊))((𝐴(-g‘𝑊)𝐵) , 𝐵)) =
(0g‘(Scalar‘𝑊)) ↔ (𝐴(-g‘𝑊)𝐵) = (0g‘𝑊))) | 
| 27 | 3 | 3ad2ant1 1134 | . . . . . 6
⊢ ((𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → 𝑊 ∈ LMod) | 
| 28 | 16 | lmodfgrp 20867 | . . . . . 6
⊢ (𝑊 ∈ LMod →
(Scalar‘𝑊) ∈
Grp) | 
| 29 | 27, 28 | syl 17 | . . . . 5
⊢ ((𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (Scalar‘𝑊) ∈ Grp) | 
| 30 |  | eqid 2737 | . . . . . . 7
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) | 
| 31 | 16, 17, 4, 30 | ipcl 21651 | . . . . . 6
⊢ ((𝑊 ∈ PreHil ∧ (𝐴(-g‘𝑊)𝐵) ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) → ((𝐴(-g‘𝑊)𝐵) , 𝐴) ∈ (Base‘(Scalar‘𝑊))) | 
| 32 | 13, 7, 14, 31 | syl3anc 1373 | . . . . 5
⊢ ((𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ((𝐴(-g‘𝑊)𝐵) , 𝐴) ∈ (Base‘(Scalar‘𝑊))) | 
| 33 | 16, 17, 4, 30 | ipcl 21651 | . . . . . 6
⊢ ((𝑊 ∈ PreHil ∧ (𝐴(-g‘𝑊)𝐵) ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ((𝐴(-g‘𝑊)𝐵) , 𝐵) ∈ (Base‘(Scalar‘𝑊))) | 
| 34 | 13, 7, 15, 33 | syl3anc 1373 | . . . . 5
⊢ ((𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ((𝐴(-g‘𝑊)𝐵) , 𝐵) ∈ (Base‘(Scalar‘𝑊))) | 
| 35 | 30, 22, 18 | grpsubeq0 19044 | . . . . 5
⊢
(((Scalar‘𝑊)
∈ Grp ∧ ((𝐴(-g‘𝑊)𝐵) , 𝐴) ∈ (Base‘(Scalar‘𝑊)) ∧ ((𝐴(-g‘𝑊)𝐵) , 𝐵) ∈ (Base‘(Scalar‘𝑊))) → ((((𝐴(-g‘𝑊)𝐵) , 𝐴)(-g‘(Scalar‘𝑊))((𝐴(-g‘𝑊)𝐵) , 𝐵)) =
(0g‘(Scalar‘𝑊)) ↔ ((𝐴(-g‘𝑊)𝐵) , 𝐴) = ((𝐴(-g‘𝑊)𝐵) , 𝐵))) | 
| 36 | 29, 32, 34, 35 | syl3anc 1373 | . . . 4
⊢ ((𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ((((𝐴(-g‘𝑊)𝐵) , 𝐴)(-g‘(Scalar‘𝑊))((𝐴(-g‘𝑊)𝐵) , 𝐵)) =
(0g‘(Scalar‘𝑊)) ↔ ((𝐴(-g‘𝑊)𝐵) , 𝐴) = ((𝐴(-g‘𝑊)𝐵) , 𝐵))) | 
| 37 |  | lmodgrp 20865 | . . . . . 6
⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp) | 
| 38 | 3, 37 | syl 17 | . . . . 5
⊢ (𝑊 ∈ PreHil → 𝑊 ∈ Grp) | 
| 39 | 4, 23, 5 | grpsubeq0 19044 | . . . . 5
⊢ ((𝑊 ∈ Grp ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ((𝐴(-g‘𝑊)𝐵) = (0g‘𝑊) ↔ 𝐴 = 𝐵)) | 
| 40 | 38, 39 | syl3an1 1164 | . . . 4
⊢ ((𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ((𝐴(-g‘𝑊)𝐵) = (0g‘𝑊) ↔ 𝐴 = 𝐵)) | 
| 41 | 26, 36, 40 | 3bitr3d 309 | . . 3
⊢ ((𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (((𝐴(-g‘𝑊)𝐵) , 𝐴) = ((𝐴(-g‘𝑊)𝐵) , 𝐵) ↔ 𝐴 = 𝐵)) | 
| 42 | 12, 41 | sylibd 239 | . 2
⊢ ((𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (∀𝑥 ∈ 𝑉 (𝑥 , 𝐴) = (𝑥 , 𝐵) → 𝐴 = 𝐵)) | 
| 43 | 2, 42 | impbid2 226 | 1
⊢ ((𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴 = 𝐵 ↔ ∀𝑥 ∈ 𝑉 (𝑥 , 𝐴) = (𝑥 , 𝐵))) |