Step | Hyp | Ref
| Expression |
1 | | cncph.6 |
. 2
β’ π = β¨β¨ + , Β·
β©, absβ© |
2 | | eqid 2738 |
. . . 4
β’
β¨β¨ + , Β· β©, absβ© = β¨β¨ + , Β·
β©, absβ© |
3 | 2 | cnnv 29405 |
. . 3
β’
β¨β¨ + , Β· β©, absβ© β
NrmCVec |
4 | | mulm1 11530 |
. . . . . . . . . . 11
β’ (π¦ β β β (-1
Β· π¦) = -π¦) |
5 | 4 | adantl 483 |
. . . . . . . . . 10
β’ ((π₯ β β β§ π¦ β β) β (-1
Β· π¦) = -π¦) |
6 | 5 | oveq2d 7366 |
. . . . . . . . 9
β’ ((π₯ β β β§ π¦ β β) β (π₯ + (-1 Β· π¦)) = (π₯ + -π¦)) |
7 | | negsub 11383 |
. . . . . . . . 9
β’ ((π₯ β β β§ π¦ β β) β (π₯ + -π¦) = (π₯ β π¦)) |
8 | 6, 7 | eqtrd 2778 |
. . . . . . . 8
β’ ((π₯ β β β§ π¦ β β) β (π₯ + (-1 Β· π¦)) = (π₯ β π¦)) |
9 | 8 | fveq2d 6842 |
. . . . . . 7
β’ ((π₯ β β β§ π¦ β β) β
(absβ(π₯ + (-1
Β· π¦))) =
(absβ(π₯ β π¦))) |
10 | 9 | oveq1d 7365 |
. . . . . 6
β’ ((π₯ β β β§ π¦ β β) β
((absβ(π₯ + (-1
Β· π¦)))β2) =
((absβ(π₯ β
π¦))β2)) |
11 | 10 | oveq2d 7366 |
. . . . 5
β’ ((π₯ β β β§ π¦ β β) β
(((absβ(π₯ + π¦))β2) + ((absβ(π₯ + (-1 Β· π¦)))β2)) =
(((absβ(π₯ + π¦))β2) + ((absβ(π₯ β π¦))β2))) |
12 | | sqabsadd 15102 |
. . . . . . . 8
β’ ((π₯ β β β§ π¦ β β) β
((absβ(π₯ + π¦))β2) = ((((absβπ₯)β2) + ((absβπ¦)β2)) + (2 Β·
(ββ(π₯ Β·
(ββπ¦)))))) |
13 | | sqabssub 15103 |
. . . . . . . 8
β’ ((π₯ β β β§ π¦ β β) β
((absβ(π₯ β
π¦))β2) =
((((absβπ₯)β2) +
((absβπ¦)β2))
β (2 Β· (ββ(π₯ Β· (ββπ¦)))))) |
14 | 12, 13 | oveq12d 7368 |
. . . . . . 7
β’ ((π₯ β β β§ π¦ β β) β
(((absβ(π₯ + π¦))β2) + ((absβ(π₯ β π¦))β2)) = (((((absβπ₯)β2) + ((absβπ¦)β2)) + (2 Β·
(ββ(π₯ Β·
(ββπ¦))))) +
((((absβπ₯)β2) +
((absβπ¦)β2))
β (2 Β· (ββ(π₯ Β· (ββπ¦))))))) |
15 | | abscl 15098 |
. . . . . . . . . . 11
β’ (π₯ β β β
(absβπ₯) β
β) |
16 | 15 | recnd 11117 |
. . . . . . . . . 10
β’ (π₯ β β β
(absβπ₯) β
β) |
17 | 16 | sqcld 13976 |
. . . . . . . . 9
β’ (π₯ β β β
((absβπ₯)β2)
β β) |
18 | | abscl 15098 |
. . . . . . . . . . 11
β’ (π¦ β β β
(absβπ¦) β
β) |
19 | 18 | recnd 11117 |
. . . . . . . . . 10
β’ (π¦ β β β
(absβπ¦) β
β) |
20 | 19 | sqcld 13976 |
. . . . . . . . 9
β’ (π¦ β β β
((absβπ¦)β2)
β β) |
21 | | addcl 11067 |
. . . . . . . . 9
β’
((((absβπ₯)β2) β β β§
((absβπ¦)β2)
β β) β (((absβπ₯)β2) + ((absβπ¦)β2)) β β) |
22 | 17, 20, 21 | syl2an 597 |
. . . . . . . 8
β’ ((π₯ β β β§ π¦ β β) β
(((absβπ₯)β2) +
((absβπ¦)β2))
β β) |
23 | | 2cn 12162 |
. . . . . . . . 9
β’ 2 β
β |
24 | | cjcl 14924 |
. . . . . . . . . . 11
β’ (π¦ β β β
(ββπ¦) β
β) |
25 | | mulcl 11069 |
. . . . . . . . . . 11
β’ ((π₯ β β β§
(ββπ¦) β
β) β (π₯ Β·
(ββπ¦)) β
β) |
26 | 24, 25 | sylan2 594 |
. . . . . . . . . 10
β’ ((π₯ β β β§ π¦ β β) β (π₯ Β· (ββπ¦)) β
β) |
27 | | recl 14929 |
. . . . . . . . . . 11
β’ ((π₯ Β· (ββπ¦)) β β β
(ββ(π₯ Β·
(ββπ¦))) β
β) |
28 | 27 | recnd 11117 |
. . . . . . . . . 10
β’ ((π₯ Β· (ββπ¦)) β β β
(ββ(π₯ Β·
(ββπ¦))) β
β) |
29 | 26, 28 | syl 17 |
. . . . . . . . 9
β’ ((π₯ β β β§ π¦ β β) β
(ββ(π₯ Β·
(ββπ¦))) β
β) |
30 | | mulcl 11069 |
. . . . . . . . 9
β’ ((2
β β β§ (ββ(π₯ Β· (ββπ¦))) β β) β (2 Β·
(ββ(π₯ Β·
(ββπ¦))))
β β) |
31 | 23, 29, 30 | sylancr 588 |
. . . . . . . 8
β’ ((π₯ β β β§ π¦ β β) β (2
Β· (ββ(π₯
Β· (ββπ¦)))) β β) |
32 | 22, 31, 22 | ppncand 11486 |
. . . . . . 7
β’ ((π₯ β β β§ π¦ β β) β
(((((absβπ₯)β2) +
((absβπ¦)β2)) +
(2 Β· (ββ(π₯ Β· (ββπ¦))))) + ((((absβπ₯)β2) + ((absβπ¦)β2)) β (2 Β·
(ββ(π₯ Β·
(ββπ¦)))))) =
((((absβπ₯)β2) +
((absβπ¦)β2)) +
(((absβπ₯)β2) +
((absβπ¦)β2)))) |
33 | 14, 32 | eqtrd 2778 |
. . . . . 6
β’ ((π₯ β β β§ π¦ β β) β
(((absβ(π₯ + π¦))β2) + ((absβ(π₯ β π¦))β2)) = ((((absβπ₯)β2) + ((absβπ¦)β2)) + (((absβπ₯)β2) + ((absβπ¦)β2)))) |
34 | | 2times 12223 |
. . . . . . . 8
β’
((((absβπ₯)β2) + ((absβπ¦)β2)) β β β (2 Β·
(((absβπ₯)β2) +
((absβπ¦)β2))) =
((((absβπ₯)β2) +
((absβπ¦)β2)) +
(((absβπ₯)β2) +
((absβπ¦)β2)))) |
35 | 34 | eqcomd 2744 |
. . . . . . 7
β’
((((absβπ₯)β2) + ((absβπ¦)β2)) β β β
((((absβπ₯)β2) +
((absβπ¦)β2)) +
(((absβπ₯)β2) +
((absβπ¦)β2))) =
(2 Β· (((absβπ₯)β2) + ((absβπ¦)β2)))) |
36 | 22, 35 | syl 17 |
. . . . . 6
β’ ((π₯ β β β§ π¦ β β) β
((((absβπ₯)β2) +
((absβπ¦)β2)) +
(((absβπ₯)β2) +
((absβπ¦)β2))) =
(2 Β· (((absβπ₯)β2) + ((absβπ¦)β2)))) |
37 | 33, 36 | eqtrd 2778 |
. . . . 5
β’ ((π₯ β β β§ π¦ β β) β
(((absβ(π₯ + π¦))β2) + ((absβ(π₯ β π¦))β2)) = (2 Β· (((absβπ₯)β2) + ((absβπ¦)β2)))) |
38 | 11, 37 | eqtrd 2778 |
. . . 4
β’ ((π₯ β β β§ π¦ β β) β
(((absβ(π₯ + π¦))β2) + ((absβ(π₯ + (-1 Β· π¦)))β2)) = (2 Β·
(((absβπ₯)β2) +
((absβπ¦)β2)))) |
39 | 38 | rgen2 3193 |
. . 3
β’
βπ₯ β
β βπ¦ β
β (((absβ(π₯ +
π¦))β2) +
((absβ(π₯ + (-1
Β· π¦)))β2)) = (2
Β· (((absβπ₯)β2) + ((absβπ¦)β2))) |
40 | | addex 12842 |
. . . 4
β’ + β
V |
41 | | mulex 12843 |
. . . 4
β’ Β·
β V |
42 | | absf 15157 |
. . . . 5
β’
abs:ββΆβ |
43 | | cnex 11066 |
. . . . 5
β’ β
β V |
44 | | fex 7171 |
. . . . 5
β’
((abs:ββΆβ β§ β β V) β abs β
V) |
45 | 42, 43, 44 | mp2an 691 |
. . . 4
β’ abs
β V |
46 | | cnaddabloOLD 29309 |
. . . . . . 7
β’ + β
AbelOp |
47 | | ablogrpo 29275 |
. . . . . . 7
β’ ( +
β AbelOp β + β GrpOp) |
48 | 46, 47 | ax-mp 5 |
. . . . . 6
β’ + β
GrpOp |
49 | | ax-addf 11064 |
. . . . . . 7
β’ +
:(β Γ β)βΆβ |
50 | 49 | fdmi 6676 |
. . . . . 6
β’ dom + =
(β Γ β) |
51 | 48, 50 | grporn 29249 |
. . . . 5
β’ β =
ran + |
52 | 51 | isphg 29545 |
. . . 4
β’ (( +
β V β§ Β· β V β§ abs β V) β (β¨β¨ + ,
Β· β©, absβ© β CPreHilOLD β (β¨β¨ +
, Β· β©, absβ© β NrmCVec β§ βπ₯ β β βπ¦ β β (((absβ(π₯ + π¦))β2) + ((absβ(π₯ + (-1 Β· π¦)))β2)) = (2 Β· (((absβπ₯)β2) + ((absβπ¦)β2)))))) |
53 | 40, 41, 45, 52 | mp3an 1462 |
. . 3
β’
(β¨β¨ + , Β· β©, absβ© β
CPreHilOLD β (β¨β¨ + , Β· β©, absβ©
β NrmCVec β§ βπ₯ β β βπ¦ β β (((absβ(π₯ + π¦))β2) + ((absβ(π₯ + (-1 Β· π¦)))β2)) = (2 Β· (((absβπ₯)β2) + ((absβπ¦)β2))))) |
54 | 3, 39, 53 | mpbir2an 710 |
. 2
β’
β¨β¨ + , Β· β©, absβ© β
CPreHilOLD |
55 | 1, 54 | eqeltri 2835 |
1
β’ π β
CPreHilOLD |