Step | Hyp | Ref
| Expression |
1 | | eqid 2738 |
. . 3
β’
β¨β¨ +β , Β·β
β©, normββ© = β¨β¨ +β ,
Β·β β©,
normββ© |
2 | 1 | hhnv 29893 |
. 2
β’
β¨β¨ +β , Β·β
β©, normββ© β NrmCVec |
3 | | normpar 29883 |
. . . 4
β’ ((π₯ β β β§ π¦ β β) β
(((normββ(π₯ ββ π¦))β2) +
((normββ(π₯ +β π¦))β2)) = ((2 Β·
((normββπ₯)β2)) + (2 Β·
((normββπ¦)β2)))) |
4 | | hvsubval 29744 |
. . . . . . . 8
β’ ((π₯ β β β§ π¦ β β) β (π₯ ββ
π¦) = (π₯ +β (-1
Β·β π¦))) |
5 | 4 | fveq2d 6842 |
. . . . . . 7
β’ ((π₯ β β β§ π¦ β β) β
(normββ(π₯ ββ π¦)) =
(normββ(π₯ +β (-1
Β·β π¦)))) |
6 | 5 | oveq1d 7365 |
. . . . . 6
β’ ((π₯ β β β§ π¦ β β) β
((normββ(π₯ ββ π¦))β2) =
((normββ(π₯ +β (-1
Β·β π¦)))β2)) |
7 | 6 | oveq2d 7366 |
. . . . 5
β’ ((π₯ β β β§ π¦ β β) β
(((normββ(π₯ +β π¦))β2) +
((normββ(π₯ ββ π¦))β2)) =
(((normββ(π₯ +β π¦))β2) +
((normββ(π₯ +β (-1
Β·β π¦)))β2))) |
8 | | hvaddcl 29740 |
. . . . . . . . 9
β’ ((π₯ β β β§ π¦ β β) β (π₯ +β π¦) β
β) |
9 | | normcl 29853 |
. . . . . . . . 9
β’ ((π₯ +β π¦) β β β
(normββ(π₯ +β π¦)) β β) |
10 | 8, 9 | syl 17 |
. . . . . . . 8
β’ ((π₯ β β β§ π¦ β β) β
(normββ(π₯ +β π¦)) β β) |
11 | 10 | recnd 11117 |
. . . . . . 7
β’ ((π₯ β β β§ π¦ β β) β
(normββ(π₯ +β π¦)) β β) |
12 | 11 | sqcld 13976 |
. . . . . 6
β’ ((π₯ β β β§ π¦ β β) β
((normββ(π₯ +β π¦))β2) β β) |
13 | | hvsubcl 29745 |
. . . . . . . 8
β’ ((π₯ β β β§ π¦ β β) β (π₯ ββ
π¦) β
β) |
14 | | normcl 29853 |
. . . . . . . . 9
β’ ((π₯ ββ
π¦) β β β
(normββ(π₯ ββ π¦)) β
β) |
15 | 14 | recnd 11117 |
. . . . . . . 8
β’ ((π₯ ββ
π¦) β β β
(normββ(π₯ ββ π¦)) β
β) |
16 | 13, 15 | syl 17 |
. . . . . . 7
β’ ((π₯ β β β§ π¦ β β) β
(normββ(π₯ ββ π¦)) β
β) |
17 | 16 | sqcld 13976 |
. . . . . 6
β’ ((π₯ β β β§ π¦ β β) β
((normββ(π₯ ββ π¦))β2) β
β) |
18 | 12, 17 | addcomd 11291 |
. . . . 5
β’ ((π₯ β β β§ π¦ β β) β
(((normββ(π₯ +β π¦))β2) +
((normββ(π₯ ββ π¦))β2)) =
(((normββ(π₯ ββ π¦))β2) +
((normββ(π₯ +β π¦))β2))) |
19 | 7, 18 | eqtr3d 2780 |
. . . 4
β’ ((π₯ β β β§ π¦ β β) β
(((normββ(π₯ +β π¦))β2) +
((normββ(π₯ +β (-1
Β·β π¦)))β2)) =
(((normββ(π₯ ββ π¦))β2) +
((normββ(π₯ +β π¦))β2))) |
20 | | normcl 29853 |
. . . . . . 7
β’ (π₯ β β β
(normββπ₯) β β) |
21 | 20 | recnd 11117 |
. . . . . 6
β’ (π₯ β β β
(normββπ₯) β β) |
22 | 21 | sqcld 13976 |
. . . . 5
β’ (π₯ β β β
((normββπ₯)β2) β β) |
23 | | normcl 29853 |
. . . . . . 7
β’ (π¦ β β β
(normββπ¦) β β) |
24 | 23 | recnd 11117 |
. . . . . 6
β’ (π¦ β β β
(normββπ¦) β β) |
25 | 24 | sqcld 13976 |
. . . . 5
β’ (π¦ β β β
((normββπ¦)β2) β β) |
26 | | 2cn 12162 |
. . . . . 6
β’ 2 β
β |
27 | | adddi 11074 |
. . . . . 6
β’ ((2
β β β§ ((normββπ₯)β2) β β β§
((normββπ¦)β2) β β) β (2 Β·
(((normββπ₯)β2) +
((normββπ¦)β2))) = ((2 Β·
((normββπ₯)β2)) + (2 Β·
((normββπ¦)β2)))) |
28 | 26, 27 | mp3an1 1449 |
. . . . 5
β’
((((normββπ₯)β2) β β β§
((normββπ¦)β2) β β) β (2 Β·
(((normββπ₯)β2) +
((normββπ¦)β2))) = ((2 Β·
((normββπ₯)β2)) + (2 Β·
((normββπ¦)β2)))) |
29 | 22, 25, 28 | syl2an 597 |
. . . 4
β’ ((π₯ β β β§ π¦ β β) β (2
Β· (((normββπ₯)β2) +
((normββπ¦)β2))) = ((2 Β·
((normββπ₯)β2)) + (2 Β·
((normββπ¦)β2)))) |
30 | 3, 19, 29 | 3eqtr4d 2788 |
. . 3
β’ ((π₯ β β β§ π¦ β β) β
(((normββ(π₯ +β π¦))β2) +
((normββ(π₯ +β (-1
Β·β π¦)))β2)) = (2 Β·
(((normββπ₯)β2) +
((normββπ¦)β2)))) |
31 | 30 | rgen2 3193 |
. 2
β’
βπ₯ β
β βπ¦ β
β (((normββ(π₯ +β π¦))β2) +
((normββ(π₯ +β (-1
Β·β π¦)))β2)) = (2 Β·
(((normββπ₯)β2) +
((normββπ¦)β2))) |
32 | | hilablo 29888 |
. . . 4
β’
+β β AbelOp |
33 | 32 | elexi 3463 |
. . 3
β’
+β β V |
34 | | hvmulex 29739 |
. . 3
β’
Β·β β V |
35 | | normf 29851 |
. . . 4
β’
normβ: ββΆβ |
36 | | ax-hilex 29727 |
. . . 4
β’ β
β V |
37 | | fex 7171 |
. . . 4
β’
((normβ: ββΆβ β§ β β
V) β normβ β V) |
38 | 35, 36, 37 | mp2an 691 |
. . 3
β’
normβ β V |
39 | | hhnv.1 |
. . . . 5
β’ π = β¨β¨
+β , Β·β β©,
normββ© |
40 | 39 | eleq1i 2829 |
. . . 4
β’ (π β CPreHilOLD
β β¨β¨ +β , Β·β
β©, normββ© β
CPreHilOLD) |
41 | | ablogrpo 29275 |
. . . . . . 7
β’ (
+β β AbelOp β +β β
GrpOp) |
42 | 32, 41 | ax-mp 5 |
. . . . . 6
β’
+β β GrpOp |
43 | | ax-hfvadd 29728 |
. . . . . . 7
β’
+β :( β Γ β)βΆ
β |
44 | 43 | fdmi 6676 |
. . . . . 6
β’ dom
+β = ( β Γ β) |
45 | 42, 44 | grporn 29249 |
. . . . 5
β’ β
= ran +β |
46 | 45 | isphg 29545 |
. . . 4
β’ ((
+β β V β§ Β·β β V
β§ normβ β V) β (β¨β¨
+β , Β·β β©,
normββ© β CPreHilOLD β (β¨β¨
+β , Β·β β©,
normββ© β NrmCVec β§ βπ₯ β β βπ¦ β β
(((normββ(π₯ +β π¦))β2) +
((normββ(π₯ +β (-1
Β·β π¦)))β2)) = (2 Β·
(((normββπ₯)β2) +
((normββπ¦)β2)))))) |
47 | 40, 46 | bitrid 283 |
. . 3
β’ ((
+β β V β§ Β·β β V
β§ normβ β V) β (π β CPreHilOLD β
(β¨β¨ +β , Β·β β©,
normββ© β NrmCVec β§ βπ₯ β β βπ¦ β β
(((normββ(π₯ +β π¦))β2) +
((normββ(π₯ +β (-1
Β·β π¦)))β2)) = (2 Β·
(((normββπ₯)β2) +
((normββπ¦)β2)))))) |
48 | 33, 34, 38, 47 | mp3an 1462 |
. 2
β’ (π β CPreHilOLD
β (β¨β¨ +β , Β·β
β©, normββ© β NrmCVec β§ βπ₯ β β βπ¦ β β
(((normββ(π₯ +β π¦))β2) +
((normββ(π₯ +β (-1
Β·β π¦)))β2)) = (2 Β·
(((normββπ₯)β2) +
((normββπ¦)β2))))) |
49 | 2, 31, 48 | mpbir2an 710 |
1
β’ π β
CPreHilOLD |