Step | Hyp | Ref
| Expression |
1 | | nmpar.h |
. . . . 5
β’ , =
(Β·πβπ) |
2 | | nmpar.v |
. . . . 5
β’ π = (Baseβπ) |
3 | | nmpar.p |
. . . . 5
β’ + =
(+gβπ) |
4 | | nmpar.1 |
. . . . 5
β’ (π β π β βPreHil) |
5 | | nmpar.2 |
. . . . 5
β’ (π β π΄ β π) |
6 | | nmpar.3 |
. . . . 5
β’ (π β π΅ β π) |
7 | 1, 2, 3, 4, 5, 6, 5, 6 | cph2di 24587 |
. . . 4
β’ (π β ((π΄ + π΅) , (π΄ + π΅)) = (((π΄ , π΄) + (π΅ , π΅)) + ((π΄ , π΅) + (π΅ , π΄)))) |
8 | | nmpar.m |
. . . . 5
β’ β =
(-gβπ) |
9 | 1, 2, 8, 4, 5, 6, 5, 6 | cph2subdi 24590 |
. . . 4
β’ (π β ((π΄ β π΅) , (π΄ β π΅)) = (((π΄ , π΄) + (π΅ , π΅)) β ((π΄ , π΅) + (π΅ , π΄)))) |
10 | 7, 9 | oveq12d 7376 |
. . 3
β’ (π β (((π΄ + π΅) , (π΄ + π΅)) + ((π΄ β π΅) , (π΄ β π΅))) = ((((π΄ , π΄) + (π΅ , π΅)) + ((π΄ , π΅) + (π΅ , π΄))) + (((π΄ , π΄) + (π΅ , π΅)) β ((π΄ , π΅) + (π΅ , π΄))))) |
11 | | cphclm 24569 |
. . . . . . 7
β’ (π β βPreHil β
π β
βMod) |
12 | 4, 11 | syl 17 |
. . . . . 6
β’ (π β π β βMod) |
13 | | nmpar.f |
. . . . . . 7
β’ πΉ = (Scalarβπ) |
14 | | nmpar.k |
. . . . . . 7
β’ πΎ = (BaseβπΉ) |
15 | 13, 14 | clmsscn 24458 |
. . . . . 6
β’ (π β βMod β πΎ β
β) |
16 | 12, 15 | syl 17 |
. . . . 5
β’ (π β πΎ β β) |
17 | | cphphl 24551 |
. . . . . . . 8
β’ (π β βPreHil β
π β
PreHil) |
18 | 4, 17 | syl 17 |
. . . . . . 7
β’ (π β π β PreHil) |
19 | 13, 1, 2, 14 | ipcl 21053 |
. . . . . . 7
β’ ((π β PreHil β§ π΄ β π β§ π΄ β π) β (π΄ , π΄) β πΎ) |
20 | 18, 5, 5, 19 | syl3anc 1372 |
. . . . . 6
β’ (π β (π΄ , π΄) β πΎ) |
21 | 13, 1, 2, 14 | ipcl 21053 |
. . . . . . 7
β’ ((π β PreHil β§ π΅ β π β§ π΅ β π) β (π΅ , π΅) β πΎ) |
22 | 18, 6, 6, 21 | syl3anc 1372 |
. . . . . 6
β’ (π β (π΅ , π΅) β πΎ) |
23 | 13, 14 | clmacl 24463 |
. . . . . 6
β’ ((π β βMod β§ (π΄ , π΄) β πΎ β§ (π΅ , π΅) β πΎ) β ((π΄ , π΄) + (π΅ , π΅)) β πΎ) |
24 | 12, 20, 22, 23 | syl3anc 1372 |
. . . . 5
β’ (π β ((π΄ , π΄) + (π΅ , π΅)) β πΎ) |
25 | 16, 24 | sseldd 3946 |
. . . 4
β’ (π β ((π΄ , π΄) + (π΅ , π΅)) β β) |
26 | 13, 1, 2, 14 | ipcl 21053 |
. . . . . . 7
β’ ((π β PreHil β§ π΄ β π β§ π΅ β π) β (π΄ , π΅) β πΎ) |
27 | 18, 5, 6, 26 | syl3anc 1372 |
. . . . . 6
β’ (π β (π΄ , π΅) β πΎ) |
28 | 13, 1, 2, 14 | ipcl 21053 |
. . . . . . 7
β’ ((π β PreHil β§ π΅ β π β§ π΄ β π) β (π΅ , π΄) β πΎ) |
29 | 18, 6, 5, 28 | syl3anc 1372 |
. . . . . 6
β’ (π β (π΅ , π΄) β πΎ) |
30 | 13, 14 | clmacl 24463 |
. . . . . 6
β’ ((π β βMod β§ (π΄ , π΅) β πΎ β§ (π΅ , π΄) β πΎ) β ((π΄ , π΅) + (π΅ , π΄)) β πΎ) |
31 | 12, 27, 29, 30 | syl3anc 1372 |
. . . . 5
β’ (π β ((π΄ , π΅) + (π΅ , π΄)) β πΎ) |
32 | 16, 31 | sseldd 3946 |
. . . 4
β’ (π β ((π΄ , π΅) + (π΅ , π΄)) β β) |
33 | 25, 32, 25 | ppncand 11557 |
. . 3
β’ (π β ((((π΄ , π΄) + (π΅ , π΅)) + ((π΄ , π΅) + (π΅ , π΄))) + (((π΄ , π΄) + (π΅ , π΅)) β ((π΄ , π΅) + (π΅ , π΄)))) = (((π΄ , π΄) + (π΅ , π΅)) + ((π΄ , π΄) + (π΅ , π΅)))) |
34 | 10, 33 | eqtrd 2773 |
. 2
β’ (π β (((π΄ + π΅) , (π΄ + π΅)) + ((π΄ β π΅) , (π΄ β π΅))) = (((π΄ , π΄) + (π΅ , π΅)) + ((π΄ , π΄) + (π΅ , π΅)))) |
35 | | cphlmod 24554 |
. . . . . 6
β’ (π β βPreHil β
π β
LMod) |
36 | 4, 35 | syl 17 |
. . . . 5
β’ (π β π β LMod) |
37 | 2, 3 | lmodvacl 20351 |
. . . . 5
β’ ((π β LMod β§ π΄ β π β§ π΅ β π) β (π΄ + π΅) β π) |
38 | 36, 5, 6, 37 | syl3anc 1372 |
. . . 4
β’ (π β (π΄ + π΅) β π) |
39 | | nmpar.n |
. . . . 5
β’ π = (normβπ) |
40 | 2, 1, 39 | nmsq 24574 |
. . . 4
β’ ((π β βPreHil β§
(π΄ + π΅) β π) β ((πβ(π΄ + π΅))β2) = ((π΄ + π΅) , (π΄ + π΅))) |
41 | 4, 38, 40 | syl2anc 585 |
. . 3
β’ (π β ((πβ(π΄ + π΅))β2) = ((π΄ + π΅) , (π΄ + π΅))) |
42 | 2, 8 | lmodvsubcl 20382 |
. . . . 5
β’ ((π β LMod β§ π΄ β π β§ π΅ β π) β (π΄ β π΅) β π) |
43 | 36, 5, 6, 42 | syl3anc 1372 |
. . . 4
β’ (π β (π΄ β π΅) β π) |
44 | 2, 1, 39 | nmsq 24574 |
. . . 4
β’ ((π β βPreHil β§
(π΄ β π΅) β π) β ((πβ(π΄ β π΅))β2) = ((π΄ β π΅) , (π΄ β π΅))) |
45 | 4, 43, 44 | syl2anc 585 |
. . 3
β’ (π β ((πβ(π΄ β π΅))β2) = ((π΄ β π΅) , (π΄ β π΅))) |
46 | 41, 45 | oveq12d 7376 |
. 2
β’ (π β (((πβ(π΄ + π΅))β2) + ((πβ(π΄ β π΅))β2)) = (((π΄ + π΅) , (π΄ + π΅)) + ((π΄ β π΅) , (π΄ β π΅)))) |
47 | 2, 1, 39 | nmsq 24574 |
. . . . . 6
β’ ((π β βPreHil β§
π΄ β π) β ((πβπ΄)β2) = (π΄ , π΄)) |
48 | 4, 5, 47 | syl2anc 585 |
. . . . 5
β’ (π β ((πβπ΄)β2) = (π΄ , π΄)) |
49 | 2, 1, 39 | nmsq 24574 |
. . . . . 6
β’ ((π β βPreHil β§
π΅ β π) β ((πβπ΅)β2) = (π΅ , π΅)) |
50 | 4, 6, 49 | syl2anc 585 |
. . . . 5
β’ (π β ((πβπ΅)β2) = (π΅ , π΅)) |
51 | 48, 50 | oveq12d 7376 |
. . . 4
β’ (π β (((πβπ΄)β2) + ((πβπ΅)β2)) = ((π΄ , π΄) + (π΅ , π΅))) |
52 | 51 | oveq2d 7374 |
. . 3
β’ (π β (2 Β· (((πβπ΄)β2) + ((πβπ΅)β2))) = (2 Β· ((π΄ , π΄) + (π΅ , π΅)))) |
53 | 25 | 2timesd 12401 |
. . 3
β’ (π β (2 Β· ((π΄ , π΄) + (π΅ , π΅))) = (((π΄ , π΄) + (π΅ , π΅)) + ((π΄ , π΄) + (π΅ , π΅)))) |
54 | 52, 53 | eqtrd 2773 |
. 2
β’ (π β (2 Β· (((πβπ΄)β2) + ((πβπ΅)β2))) = (((π΄ , π΄) + (π΅ , π΅)) + ((π΄ , π΄) + (π΅ , π΅)))) |
55 | 34, 46, 54 | 3eqtr4d 2783 |
1
β’ (π β (((πβ(π΄ + π΅))β2) + ((πβ(π΄ β π΅))β2)) = (2 Β· (((πβπ΄)β2) + ((πβπ΅)β2)))) |