Step | Hyp | Ref
| Expression |
1 | | cph2subdi.1 |
. . . . . 6
β’ (π β π β βPreHil) |
2 | | cphclm 25072 |
. . . . . 6
β’ (π β βPreHil β
π β
βMod) |
3 | 1, 2 | syl 17 |
. . . . 5
β’ (π β π β βMod) |
4 | | eqid 2726 |
. . . . . 6
β’
(Scalarβπ) =
(Scalarβπ) |
5 | 4 | clmadd 24956 |
. . . . 5
β’ (π β βMod β + =
(+gβ(Scalarβπ))) |
6 | 3, 5 | syl 17 |
. . . 4
β’ (π β + =
(+gβ(Scalarβπ))) |
7 | 6 | oveqd 7422 |
. . 3
β’ (π β ((π΄ , πΆ) + (π΅ , π·)) = ((π΄ , πΆ)(+gβ(Scalarβπ))(π΅ , π·))) |
8 | 6 | oveqd 7422 |
. . 3
β’ (π β ((π΄ , π·) + (π΅ , πΆ)) = ((π΄ , π·)(+gβ(Scalarβπ))(π΅ , πΆ))) |
9 | 7, 8 | oveq12d 7423 |
. 2
β’ (π β (((π΄ , πΆ) + (π΅ , π·))(-gβ(Scalarβπ))((π΄ , π·) + (π΅ , πΆ))) = (((π΄ , πΆ)(+gβ(Scalarβπ))(π΅ , π·))(-gβ(Scalarβπ))((π΄ , π·)(+gβ(Scalarβπ))(π΅ , πΆ)))) |
10 | | cphphl 25054 |
. . . . . 6
β’ (π β βPreHil β
π β
PreHil) |
11 | 1, 10 | syl 17 |
. . . . 5
β’ (π β π β PreHil) |
12 | | cph2subdi.2 |
. . . . 5
β’ (π β π΄ β π) |
13 | | cph2subdi.4 |
. . . . 5
β’ (π β πΆ β π) |
14 | | cphipcj.h |
. . . . . 6
β’ , =
(Β·πβπ) |
15 | | cphipcj.v |
. . . . . 6
β’ π = (Baseβπ) |
16 | | eqid 2726 |
. . . . . 6
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
17 | 4, 14, 15, 16 | ipcl 21526 |
. . . . 5
β’ ((π β PreHil β§ π΄ β π β§ πΆ β π) β (π΄ , πΆ) β (Baseβ(Scalarβπ))) |
18 | 11, 12, 13, 17 | syl3anc 1368 |
. . . 4
β’ (π β (π΄ , πΆ) β (Baseβ(Scalarβπ))) |
19 | | cph2subdi.3 |
. . . . 5
β’ (π β π΅ β π) |
20 | | cph2subdi.5 |
. . . . 5
β’ (π β π· β π) |
21 | 4, 14, 15, 16 | ipcl 21526 |
. . . . 5
β’ ((π β PreHil β§ π΅ β π β§ π· β π) β (π΅ , π·) β (Baseβ(Scalarβπ))) |
22 | 11, 19, 20, 21 | syl3anc 1368 |
. . . 4
β’ (π β (π΅ , π·) β (Baseβ(Scalarβπ))) |
23 | 4, 16 | clmacl 24966 |
. . . 4
β’ ((π β βMod β§ (π΄ , πΆ) β (Baseβ(Scalarβπ)) β§ (π΅ , π·) β (Baseβ(Scalarβπ))) β ((π΄ , πΆ) + (π΅ , π·)) β (Baseβ(Scalarβπ))) |
24 | 3, 18, 22, 23 | syl3anc 1368 |
. . 3
β’ (π β ((π΄ , πΆ) + (π΅ , π·)) β (Baseβ(Scalarβπ))) |
25 | 4, 14, 15, 16 | ipcl 21526 |
. . . . 5
β’ ((π β PreHil β§ π΄ β π β§ π· β π) β (π΄ , π·) β (Baseβ(Scalarβπ))) |
26 | 11, 12, 20, 25 | syl3anc 1368 |
. . . 4
β’ (π β (π΄ , π·) β (Baseβ(Scalarβπ))) |
27 | 4, 14, 15, 16 | ipcl 21526 |
. . . . 5
β’ ((π β PreHil β§ π΅ β π β§ πΆ β π) β (π΅ , πΆ) β (Baseβ(Scalarβπ))) |
28 | 11, 19, 13, 27 | syl3anc 1368 |
. . . 4
β’ (π β (π΅ , πΆ) β (Baseβ(Scalarβπ))) |
29 | 4, 16 | clmacl 24966 |
. . . 4
β’ ((π β βMod β§ (π΄ , π·) β (Baseβ(Scalarβπ)) β§ (π΅ , πΆ) β (Baseβ(Scalarβπ))) β ((π΄ , π·) + (π΅ , πΆ)) β (Baseβ(Scalarβπ))) |
30 | 3, 26, 28, 29 | syl3anc 1368 |
. . 3
β’ (π β ((π΄ , π·) + (π΅ , πΆ)) β (Baseβ(Scalarβπ))) |
31 | 4, 16 | clmsub 24962 |
. . 3
β’ ((π β βMod β§ ((π΄ , πΆ) + (π΅ , π·)) β (Baseβ(Scalarβπ)) β§ ((π΄ , π·) + (π΅ , πΆ)) β (Baseβ(Scalarβπ))) β (((π΄ , πΆ) + (π΅ , π·)) β ((π΄ , π·) + (π΅ , πΆ))) = (((π΄ , πΆ) + (π΅ , π·))(-gβ(Scalarβπ))((π΄ , π·) + (π΅ , πΆ)))) |
32 | 3, 24, 30, 31 | syl3anc 1368 |
. 2
β’ (π β (((π΄ , πΆ) + (π΅ , π·)) β ((π΄ , π·) + (π΅ , πΆ))) = (((π΄ , πΆ) + (π΅ , π·))(-gβ(Scalarβπ))((π΄ , π·) + (π΅ , πΆ)))) |
33 | | cphsubdir.m |
. . 3
β’ β =
(-gβπ) |
34 | | eqid 2726 |
. . 3
β’
(-gβ(Scalarβπ)) =
(-gβ(Scalarβπ)) |
35 | | eqid 2726 |
. . 3
β’
(+gβ(Scalarβπ)) =
(+gβ(Scalarβπ)) |
36 | 4, 14, 15, 33, 34, 35, 11, 12, 19, 13, 20 | ip2subdi 21537 |
. 2
β’ (π β ((π΄ β π΅) , (πΆ β π·)) = (((π΄ , πΆ)(+gβ(Scalarβπ))(π΅ , π·))(-gβ(Scalarβπ))((π΄ , π·)(+gβ(Scalarβπ))(π΅ , πΆ)))) |
37 | 9, 32, 36 | 3eqtr4rd 2777 |
1
β’ (π β ((π΄ β π΅) , (πΆ β π·)) = (((π΄ , πΆ) + (π΅ , π·)) β ((π΄ , π·) + (π΅ , πΆ)))) |