Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . 3
β’
β¨β¨ +β , Β·β
β©, normββ© = β¨β¨ +β ,
Β·β β©,
normββ© |
2 | 1 | hhnv 29905 |
. 2
β’
β¨β¨ +β , Β·β
β©, normββ© β NrmCVec |
3 | | normpar 29895 |
. . . 4
β’ ((π₯ β β β§ π¦ β β) β
(((normββ(π₯ ββ π¦))β2) +
((normββ(π₯ +β π¦))β2)) = ((2 Β·
((normββπ₯)β2)) + (2 Β·
((normββπ¦)β2)))) |
4 | | hvsubval 29756 |
. . . . . . . 8
β’ ((π₯ β β β§ π¦ β β) β (π₯ ββ
π¦) = (π₯ +β (-1
Β·β π¦))) |
5 | 4 | fveq2d 6841 |
. . . . . . 7
β’ ((π₯ β β β§ π¦ β β) β
(normββ(π₯ ββ π¦)) =
(normββ(π₯ +β (-1
Β·β π¦)))) |
6 | 5 | oveq1d 7364 |
. . . . . 6
β’ ((π₯ β β β§ π¦ β β) β
((normββ(π₯ ββ π¦))β2) =
((normββ(π₯ +β (-1
Β·β π¦)))β2)) |
7 | 6 | oveq2d 7365 |
. . . . 5
β’ ((π₯ β β β§ π¦ β β) β
(((normββ(π₯ +β π¦))β2) +
((normββ(π₯ ββ π¦))β2)) =
(((normββ(π₯ +β π¦))β2) +
((normββ(π₯ +β (-1
Β·β π¦)))β2))) |
8 | | hvaddcl 29752 |
. . . . . . . . 9
β’ ((π₯ β β β§ π¦ β β) β (π₯ +β π¦) β
β) |
9 | | normcl 29865 |
. . . . . . . . 9
β’ ((π₯ +β π¦) β β β
(normββ(π₯ +β π¦)) β β) |
10 | 8, 9 | syl 17 |
. . . . . . . 8
β’ ((π₯ β β β§ π¦ β β) β
(normββ(π₯ +β π¦)) β β) |
11 | 10 | recnd 11116 |
. . . . . . 7
β’ ((π₯ β β β§ π¦ β β) β
(normββ(π₯ +β π¦)) β β) |
12 | 11 | sqcld 13975 |
. . . . . 6
β’ ((π₯ β β β§ π¦ β β) β
((normββ(π₯ +β π¦))β2) β β) |
13 | | hvsubcl 29757 |
. . . . . . . 8
β’ ((π₯ β β β§ π¦ β β) β (π₯ ββ
π¦) β
β) |
14 | | normcl 29865 |
. . . . . . . . 9
β’ ((π₯ ββ
π¦) β β β
(normββ(π₯ ββ π¦)) β
β) |
15 | 14 | recnd 11116 |
. . . . . . . 8
β’ ((π₯ ββ
π¦) β β β
(normββ(π₯ ββ π¦)) β
β) |
16 | 13, 15 | syl 17 |
. . . . . . 7
β’ ((π₯ β β β§ π¦ β β) β
(normββ(π₯ ββ π¦)) β
β) |
17 | 16 | sqcld 13975 |
. . . . . 6
β’ ((π₯ β β β§ π¦ β β) β
((normββ(π₯ ββ π¦))β2) β
β) |
18 | 12, 17 | addcomd 11290 |
. . . . 5
β’ ((π₯ β β β§ π¦ β β) β
(((normββ(π₯ +β π¦))β2) +
((normββ(π₯ ββ π¦))β2)) =
(((normββ(π₯ ββ π¦))β2) +
((normββ(π₯ +β π¦))β2))) |
19 | 7, 18 | eqtr3d 2779 |
. . . 4
β’ ((π₯ β β β§ π¦ β β) β
(((normββ(π₯ +β π¦))β2) +
((normββ(π₯ +β (-1
Β·β π¦)))β2)) =
(((normββ(π₯ ββ π¦))β2) +
((normββ(π₯ +β π¦))β2))) |
20 | | normcl 29865 |
. . . . . . 7
β’ (π₯ β β β
(normββπ₯) β β) |
21 | 20 | recnd 11116 |
. . . . . 6
β’ (π₯ β β β
(normββπ₯) β β) |
22 | 21 | sqcld 13975 |
. . . . 5
β’ (π₯ β β β
((normββπ₯)β2) β β) |
23 | | normcl 29865 |
. . . . . . 7
β’ (π¦ β β β
(normββπ¦) β β) |
24 | 23 | recnd 11116 |
. . . . . 6
β’ (π¦ β β β
(normββπ¦) β β) |
25 | 24 | sqcld 13975 |
. . . . 5
β’ (π¦ β β β
((normββπ¦)β2) β β) |
26 | | 2cn 12161 |
. . . . . 6
β’ 2 β
β |
27 | | adddi 11073 |
. . . . . 6
β’ ((2
β β β§ ((normββπ₯)β2) β β β§
((normββπ¦)β2) β β) β (2 Β·
(((normββπ₯)β2) +
((normββπ¦)β2))) = ((2 Β·
((normββπ₯)β2)) + (2 Β·
((normββπ¦)β2)))) |
28 | 26, 27 | mp3an1 1448 |
. . . . 5
β’
((((normββπ₯)β2) β β β§
((normββπ¦)β2) β β) β (2 Β·
(((normββπ₯)β2) +
((normββπ¦)β2))) = ((2 Β·
((normββπ₯)β2)) + (2 Β·
((normββπ¦)β2)))) |
29 | 22, 25, 28 | syl2an 596 |
. . . 4
β’ ((π₯ β β β§ π¦ β β) β (2
Β· (((normββπ₯)β2) +
((normββπ¦)β2))) = ((2 Β·
((normββπ₯)β2)) + (2 Β·
((normββπ¦)β2)))) |
30 | 3, 19, 29 | 3eqtr4d 2787 |
. . 3
β’ ((π₯ β β β§ π¦ β β) β
(((normββ(π₯ +β π¦))β2) +
((normββ(π₯ +β (-1
Β·β π¦)))β2)) = (2 Β·
(((normββπ₯)β2) +
((normββπ¦)β2)))) |
31 | 30 | rgen2 3192 |
. 2
β’
βπ₯ β
β βπ¦ β
β (((normββ(π₯ +β π¦))β2) +
((normββ(π₯ +β (-1
Β·β π¦)))β2)) = (2 Β·
(((normββπ₯)β2) +
((normββπ¦)β2))) |
32 | | hilablo 29900 |
. . . 4
β’
+β β AbelOp |
33 | 32 | elexi 3462 |
. . 3
β’
+β β V |
34 | | hvmulex 29751 |
. . 3
β’
Β·β β V |
35 | | normf 29863 |
. . . 4
β’
normβ: ββΆβ |
36 | | ax-hilex 29739 |
. . . 4
β’ β
β V |
37 | | fex 7170 |
. . . 4
β’
((normβ: ββΆβ β§ β β
V) β normβ β V) |
38 | 35, 36, 37 | mp2an 690 |
. . 3
β’
normβ β V |
39 | | hhnv.1 |
. . . . 5
β’ π = β¨β¨
+β , Β·β β©,
normββ© |
40 | 39 | eleq1i 2828 |
. . . 4
β’ (π β CPreHilOLD
β β¨β¨ +β , Β·β
β©, normββ© β
CPreHilOLD) |
41 | | ablogrpo 29287 |
. . . . . . 7
β’ (
+β β AbelOp β +β β
GrpOp) |
42 | 32, 41 | ax-mp 5 |
. . . . . 6
β’
+β β GrpOp |
43 | | ax-hfvadd 29740 |
. . . . . . 7
β’
+β :( β Γ β)βΆ
β |
44 | 43 | fdmi 6675 |
. . . . . 6
β’ dom
+β = ( β Γ β) |
45 | 42, 44 | grporn 29261 |
. . . . 5
β’ β
= ran +β |
46 | 45 | isphg 29557 |
. . . 4
β’ ((
+β β V β§ Β·β β V
β§ normβ β V) β (β¨β¨
+β , Β·β β©,
normββ© β CPreHilOLD β (β¨β¨
+β , Β·β β©,
normββ© β NrmCVec β§ βπ₯ β β βπ¦ β β
(((normββ(π₯ +β π¦))β2) +
((normββ(π₯ +β (-1
Β·β π¦)))β2)) = (2 Β·
(((normββπ₯)β2) +
((normββπ¦)β2)))))) |
47 | 40, 46 | bitrid 282 |
. . 3
β’ ((
+β β V β§ Β·β β V
β§ normβ β V) β (π β CPreHilOLD β
(β¨β¨ +β , Β·β β©,
normββ© β NrmCVec β§ βπ₯ β β βπ¦ β β
(((normββ(π₯ +β π¦))β2) +
((normββ(π₯ +β (-1
Β·β π¦)))β2)) = (2 Β·
(((normββπ₯)β2) +
((normββπ¦)β2)))))) |
48 | 33, 34, 38, 47 | mp3an 1461 |
. 2
β’ (π β CPreHilOLD
β (β¨β¨ +β , Β·β
β©, normββ© β NrmCVec β§ βπ₯ β β βπ¦ β β
(((normββ(π₯ +β π¦))β2) +
((normββ(π₯ +β (-1
Β·β π¦)))β2)) = (2 Β·
(((normββπ₯)β2) +
((normββπ¦)β2))))) |
49 | 2, 31, 48 | mpbir2an 709 |
1
β’ π β
CPreHilOLD |