Proof of Theorem ipsubdir
Step | Hyp | Ref
| Expression |
1 | | simpl 483 |
. . . . 5
⊢ ((𝑊 ∈ PreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → 𝑊 ∈ PreHil) |
2 | | phllmod 20702 |
. . . . . . . 8
⊢ (𝑊 ∈ PreHil → 𝑊 ∈ LMod) |
3 | 2 | adantr 481 |
. . . . . . 7
⊢ ((𝑊 ∈ PreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → 𝑊 ∈ LMod) |
4 | | lmodgrp 19570 |
. . . . . . 7
⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp) |
5 | 3, 4 | syl 17 |
. . . . . 6
⊢ ((𝑊 ∈ PreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → 𝑊 ∈ Grp) |
6 | | simpr1 1186 |
. . . . . 6
⊢ ((𝑊 ∈ PreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → 𝐴 ∈ 𝑉) |
7 | | simpr2 1187 |
. . . . . 6
⊢ ((𝑊 ∈ PreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → 𝐵 ∈ 𝑉) |
8 | | phllmhm.v |
. . . . . . 7
⊢ 𝑉 = (Base‘𝑊) |
9 | | ipsubdir.m |
. . . . . . 7
⊢ − =
(-g‘𝑊) |
10 | 8, 9 | grpsubcl 18117 |
. . . . . 6
⊢ ((𝑊 ∈ Grp ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴 − 𝐵) ∈ 𝑉) |
11 | 5, 6, 7, 10 | syl3anc 1363 |
. . . . 5
⊢ ((𝑊 ∈ PreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝐴 − 𝐵) ∈ 𝑉) |
12 | | simpr3 1188 |
. . . . 5
⊢ ((𝑊 ∈ PreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → 𝐶 ∈ 𝑉) |
13 | | phlsrng.f |
. . . . . 6
⊢ 𝐹 = (Scalar‘𝑊) |
14 | | phllmhm.h |
. . . . . 6
⊢ , =
(·𝑖‘𝑊) |
15 | | eqid 2818 |
. . . . . 6
⊢
(+g‘𝑊) = (+g‘𝑊) |
16 | | eqid 2818 |
. . . . . 6
⊢
(+g‘𝐹) = (+g‘𝐹) |
17 | 13, 14, 8, 15, 16 | ipdir 20711 |
. . . . 5
⊢ ((𝑊 ∈ PreHil ∧ ((𝐴 − 𝐵) ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (((𝐴 − 𝐵)(+g‘𝑊)𝐵) , 𝐶) = (((𝐴 − 𝐵) , 𝐶)(+g‘𝐹)(𝐵 , 𝐶))) |
18 | 1, 11, 7, 12, 17 | syl13anc 1364 |
. . . 4
⊢ ((𝑊 ∈ PreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (((𝐴 − 𝐵)(+g‘𝑊)𝐵) , 𝐶) = (((𝐴 − 𝐵) , 𝐶)(+g‘𝐹)(𝐵 , 𝐶))) |
19 | 8, 15, 9 | grpnpcan 18129 |
. . . . . 6
⊢ ((𝑊 ∈ Grp ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ((𝐴 − 𝐵)(+g‘𝑊)𝐵) = 𝐴) |
20 | 5, 6, 7, 19 | syl3anc 1363 |
. . . . 5
⊢ ((𝑊 ∈ PreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝐴 − 𝐵)(+g‘𝑊)𝐵) = 𝐴) |
21 | 20 | oveq1d 7160 |
. . . 4
⊢ ((𝑊 ∈ PreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (((𝐴 − 𝐵)(+g‘𝑊)𝐵) , 𝐶) = (𝐴 , 𝐶)) |
22 | 18, 21 | eqtr3d 2855 |
. . 3
⊢ ((𝑊 ∈ PreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (((𝐴 − 𝐵) , 𝐶)(+g‘𝐹)(𝐵 , 𝐶)) = (𝐴 , 𝐶)) |
23 | 13 | lmodfgrp 19572 |
. . . . 5
⊢ (𝑊 ∈ LMod → 𝐹 ∈ Grp) |
24 | 3, 23 | syl 17 |
. . . 4
⊢ ((𝑊 ∈ PreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → 𝐹 ∈ Grp) |
25 | | eqid 2818 |
. . . . . 6
⊢
(Base‘𝐹) =
(Base‘𝐹) |
26 | 13, 14, 8, 25 | ipcl 20705 |
. . . . 5
⊢ ((𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝐴 , 𝐶) ∈ (Base‘𝐹)) |
27 | 1, 6, 12, 26 | syl3anc 1363 |
. . . 4
⊢ ((𝑊 ∈ PreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝐴 , 𝐶) ∈ (Base‘𝐹)) |
28 | 13, 14, 8, 25 | ipcl 20705 |
. . . . 5
⊢ ((𝑊 ∈ PreHil ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝐵 , 𝐶) ∈ (Base‘𝐹)) |
29 | 1, 7, 12, 28 | syl3anc 1363 |
. . . 4
⊢ ((𝑊 ∈ PreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝐵 , 𝐶) ∈ (Base‘𝐹)) |
30 | 13, 14, 8, 25 | ipcl 20705 |
. . . . 5
⊢ ((𝑊 ∈ PreHil ∧ (𝐴 − 𝐵) ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ((𝐴 − 𝐵) , 𝐶) ∈ (Base‘𝐹)) |
31 | 1, 11, 12, 30 | syl3anc 1363 |
. . . 4
⊢ ((𝑊 ∈ PreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝐴 − 𝐵) , 𝐶) ∈ (Base‘𝐹)) |
32 | | ipsubdir.s |
. . . . 5
⊢ 𝑆 = (-g‘𝐹) |
33 | 25, 16, 32 | grpsubadd 18125 |
. . . 4
⊢ ((𝐹 ∈ Grp ∧ ((𝐴 , 𝐶) ∈ (Base‘𝐹) ∧ (𝐵 , 𝐶) ∈ (Base‘𝐹) ∧ ((𝐴 − 𝐵) , 𝐶) ∈ (Base‘𝐹))) → (((𝐴 , 𝐶)𝑆(𝐵 , 𝐶)) = ((𝐴 − 𝐵) , 𝐶) ↔ (((𝐴 − 𝐵) , 𝐶)(+g‘𝐹)(𝐵 , 𝐶)) = (𝐴 , 𝐶))) |
34 | 24, 27, 29, 31, 33 | syl13anc 1364 |
. . 3
⊢ ((𝑊 ∈ PreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (((𝐴 , 𝐶)𝑆(𝐵 , 𝐶)) = ((𝐴 − 𝐵) , 𝐶) ↔ (((𝐴 − 𝐵) , 𝐶)(+g‘𝐹)(𝐵 , 𝐶)) = (𝐴 , 𝐶))) |
35 | 22, 34 | mpbird 258 |
. 2
⊢ ((𝑊 ∈ PreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝐴 , 𝐶)𝑆(𝐵 , 𝐶)) = ((𝐴 − 𝐵) , 𝐶)) |
36 | 35 | eqcomd 2824 |
1
⊢ ((𝑊 ∈ PreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝐴 − 𝐵) , 𝐶) = ((𝐴 , 𝐶)𝑆(𝐵 , 𝐶))) |