Proof of Theorem ip2subdi
Step | Hyp | Ref
| Expression |
1 | | eqid 2738 |
. . . 4
⊢
(Base‘𝐹) =
(Base‘𝐹) |
2 | | ip2subdi.p |
. . . 4
⊢ + =
(+g‘𝐹) |
3 | | ipsubdir.s |
. . . 4
⊢ 𝑆 = (-g‘𝐹) |
4 | | ip2subdi.1 |
. . . . . . 7
⊢ (𝜑 → 𝑊 ∈ PreHil) |
5 | | phllmod 20835 |
. . . . . . 7
⊢ (𝑊 ∈ PreHil → 𝑊 ∈ LMod) |
6 | 4, 5 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑊 ∈ LMod) |
7 | | phlsrng.f |
. . . . . . 7
⊢ 𝐹 = (Scalar‘𝑊) |
8 | 7 | lmodring 20131 |
. . . . . 6
⊢ (𝑊 ∈ LMod → 𝐹 ∈ Ring) |
9 | 6, 8 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ Ring) |
10 | | ringabl 19819 |
. . . . 5
⊢ (𝐹 ∈ Ring → 𝐹 ∈ Abel) |
11 | 9, 10 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ Abel) |
12 | | ip2subdi.2 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
13 | | ip2subdi.4 |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ 𝑉) |
14 | | phllmhm.h |
. . . . . 6
⊢ , =
(·𝑖‘𝑊) |
15 | | phllmhm.v |
. . . . . 6
⊢ 𝑉 = (Base‘𝑊) |
16 | 7, 14, 15, 1 | ipcl 20838 |
. . . . 5
⊢ ((𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝐴 , 𝐶) ∈ (Base‘𝐹)) |
17 | 4, 12, 13, 16 | syl3anc 1370 |
. . . 4
⊢ (𝜑 → (𝐴 , 𝐶) ∈ (Base‘𝐹)) |
18 | | ip2subdi.5 |
. . . . 5
⊢ (𝜑 → 𝐷 ∈ 𝑉) |
19 | 7, 14, 15, 1 | ipcl 20838 |
. . . . 5
⊢ ((𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉) → (𝐴 , 𝐷) ∈ (Base‘𝐹)) |
20 | 4, 12, 18, 19 | syl3anc 1370 |
. . . 4
⊢ (𝜑 → (𝐴 , 𝐷) ∈ (Base‘𝐹)) |
21 | | ip2subdi.3 |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ 𝑉) |
22 | 7, 14, 15, 1 | ipcl 20838 |
. . . . 5
⊢ ((𝑊 ∈ PreHil ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝐵 , 𝐶) ∈ (Base‘𝐹)) |
23 | 4, 21, 13, 22 | syl3anc 1370 |
. . . 4
⊢ (𝜑 → (𝐵 , 𝐶) ∈ (Base‘𝐹)) |
24 | 1, 2, 3, 11, 17, 20, 23 | ablsubsub4 19420 |
. . 3
⊢ (𝜑 → (((𝐴 , 𝐶)𝑆(𝐴 , 𝐷))𝑆(𝐵 , 𝐶)) = ((𝐴 , 𝐶)𝑆((𝐴 , 𝐷) + (𝐵 , 𝐶)))) |
25 | 24 | oveq1d 7290 |
. 2
⊢ (𝜑 → ((((𝐴 , 𝐶)𝑆(𝐴 , 𝐷))𝑆(𝐵 , 𝐶)) + (𝐵 , 𝐷)) = (((𝐴 , 𝐶)𝑆((𝐴 , 𝐷) + (𝐵 , 𝐶))) + (𝐵 , 𝐷))) |
26 | | ipsubdir.m |
. . . . . 6
⊢ − =
(-g‘𝑊) |
27 | 15, 26 | lmodvsubcl 20168 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉) → (𝐶 − 𝐷) ∈ 𝑉) |
28 | 6, 13, 18, 27 | syl3anc 1370 |
. . . 4
⊢ (𝜑 → (𝐶 − 𝐷) ∈ 𝑉) |
29 | 7, 14, 15, 26, 3 | ipsubdir 20847 |
. . . 4
⊢ ((𝑊 ∈ PreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ (𝐶 − 𝐷) ∈ 𝑉)) → ((𝐴 − 𝐵) , (𝐶 − 𝐷)) = ((𝐴 , (𝐶 − 𝐷))𝑆(𝐵 , (𝐶 − 𝐷)))) |
30 | 4, 12, 21, 28, 29 | syl13anc 1371 |
. . 3
⊢ (𝜑 → ((𝐴 − 𝐵) , (𝐶 − 𝐷)) = ((𝐴 , (𝐶 − 𝐷))𝑆(𝐵 , (𝐶 − 𝐷)))) |
31 | 7, 14, 15, 26, 3 | ipsubdi 20848 |
. . . . 5
⊢ ((𝑊 ∈ PreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → (𝐴 , (𝐶 − 𝐷)) = ((𝐴 , 𝐶)𝑆(𝐴 , 𝐷))) |
32 | 4, 12, 13, 18, 31 | syl13anc 1371 |
. . . 4
⊢ (𝜑 → (𝐴 , (𝐶 − 𝐷)) = ((𝐴 , 𝐶)𝑆(𝐴 , 𝐷))) |
33 | 7, 14, 15, 26, 3 | ipsubdi 20848 |
. . . . 5
⊢ ((𝑊 ∈ PreHil ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → (𝐵 , (𝐶 − 𝐷)) = ((𝐵 , 𝐶)𝑆(𝐵 , 𝐷))) |
34 | 4, 21, 13, 18, 33 | syl13anc 1371 |
. . . 4
⊢ (𝜑 → (𝐵 , (𝐶 − 𝐷)) = ((𝐵 , 𝐶)𝑆(𝐵 , 𝐷))) |
35 | 32, 34 | oveq12d 7293 |
. . 3
⊢ (𝜑 → ((𝐴 , (𝐶 − 𝐷))𝑆(𝐵 , (𝐶 − 𝐷))) = (((𝐴 , 𝐶)𝑆(𝐴 , 𝐷))𝑆((𝐵 , 𝐶)𝑆(𝐵 , 𝐷)))) |
36 | | ringgrp 19788 |
. . . . . 6
⊢ (𝐹 ∈ Ring → 𝐹 ∈ Grp) |
37 | 9, 36 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ Grp) |
38 | 1, 3 | grpsubcl 18655 |
. . . . 5
⊢ ((𝐹 ∈ Grp ∧ (𝐴 , 𝐶) ∈ (Base‘𝐹) ∧ (𝐴 , 𝐷) ∈ (Base‘𝐹)) → ((𝐴 , 𝐶)𝑆(𝐴 , 𝐷)) ∈ (Base‘𝐹)) |
39 | 37, 17, 20, 38 | syl3anc 1370 |
. . . 4
⊢ (𝜑 → ((𝐴 , 𝐶)𝑆(𝐴 , 𝐷)) ∈ (Base‘𝐹)) |
40 | 7, 14, 15, 1 | ipcl 20838 |
. . . . 5
⊢ ((𝑊 ∈ PreHil ∧ 𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉) → (𝐵 , 𝐷) ∈ (Base‘𝐹)) |
41 | 4, 21, 18, 40 | syl3anc 1370 |
. . . 4
⊢ (𝜑 → (𝐵 , 𝐷) ∈ (Base‘𝐹)) |
42 | 1, 2, 3, 11, 39, 23, 41 | ablsubsub 19419 |
. . 3
⊢ (𝜑 → (((𝐴 , 𝐶)𝑆(𝐴 , 𝐷))𝑆((𝐵 , 𝐶)𝑆(𝐵 , 𝐷))) = ((((𝐴 , 𝐶)𝑆(𝐴 , 𝐷))𝑆(𝐵 , 𝐶)) + (𝐵 , 𝐷))) |
43 | 30, 35, 42 | 3eqtrd 2782 |
. 2
⊢ (𝜑 → ((𝐴 − 𝐵) , (𝐶 − 𝐷)) = ((((𝐴 , 𝐶)𝑆(𝐴 , 𝐷))𝑆(𝐵 , 𝐶)) + (𝐵 , 𝐷))) |
44 | 1, 2 | ringacl 19817 |
. . . 4
⊢ ((𝐹 ∈ Ring ∧ (𝐴 , 𝐷) ∈ (Base‘𝐹) ∧ (𝐵 , 𝐶) ∈ (Base‘𝐹)) → ((𝐴 , 𝐷) + (𝐵 , 𝐶)) ∈ (Base‘𝐹)) |
45 | 9, 20, 23, 44 | syl3anc 1370 |
. . 3
⊢ (𝜑 → ((𝐴 , 𝐷) + (𝐵 , 𝐶)) ∈ (Base‘𝐹)) |
46 | 1, 2, 3 | abladdsub 19416 |
. . 3
⊢ ((𝐹 ∈ Abel ∧ ((𝐴 , 𝐶) ∈ (Base‘𝐹) ∧ (𝐵 , 𝐷) ∈ (Base‘𝐹) ∧ ((𝐴 , 𝐷) + (𝐵 , 𝐶)) ∈ (Base‘𝐹))) → (((𝐴 , 𝐶) + (𝐵 , 𝐷))𝑆((𝐴 , 𝐷) + (𝐵 , 𝐶))) = (((𝐴 , 𝐶)𝑆((𝐴 , 𝐷) + (𝐵 , 𝐶))) + (𝐵 , 𝐷))) |
47 | 11, 17, 41, 45, 46 | syl13anc 1371 |
. 2
⊢ (𝜑 → (((𝐴 , 𝐶) + (𝐵 , 𝐷))𝑆((𝐴 , 𝐷) + (𝐵 , 𝐶))) = (((𝐴 , 𝐶)𝑆((𝐴 , 𝐷) + (𝐵 , 𝐶))) + (𝐵 , 𝐷))) |
48 | 25, 43, 47 | 3eqtr4d 2788 |
1
⊢ (𝜑 → ((𝐴 − 𝐵) , (𝐶 − 𝐷)) = (((𝐴 , 𝐶) + (𝐵 , 𝐷))𝑆((𝐴 , 𝐷) + (𝐵 , 𝐶)))) |