Step | Hyp | Ref
| Expression |
1 | | 2cn 12236 |
. . . 4
β’ 2 β
β |
2 | | ip1i.1 |
. . . . . . 7
β’ π = (BaseSetβπ) |
3 | | ip1i.6 |
. . . . . . 7
β’ π =
(normCVβπ) |
4 | | ip1i.9 |
. . . . . . . 8
β’ π β
CPreHilOLD |
5 | 4 | phnvi 29807 |
. . . . . . 7
β’ π β NrmCVec |
6 | | ip1i.a |
. . . . . . . 8
β’ π΄ β π |
7 | | ip0i.j |
. . . . . . . . 9
β’ π½ β β |
8 | | ip1i.c |
. . . . . . . . 9
β’ πΆ β π |
9 | | ip1i.4 |
. . . . . . . . . 10
β’ π = (
Β·π OLD βπ) |
10 | 2, 9 | nvscl 29617 |
. . . . . . . . 9
β’ ((π β NrmCVec β§ π½ β β β§ πΆ β π) β (π½ππΆ) β π) |
11 | 5, 7, 8, 10 | mp3an 1462 |
. . . . . . . 8
β’ (π½ππΆ) β π |
12 | | ip1i.2 |
. . . . . . . . 9
β’ πΊ = ( +π£
βπ) |
13 | 2, 12 | nvgcl 29611 |
. . . . . . . 8
β’ ((π β NrmCVec β§ π΄ β π β§ (π½ππΆ) β π) β (π΄πΊ(π½ππΆ)) β π) |
14 | 5, 6, 11, 13 | mp3an 1462 |
. . . . . . 7
β’ (π΄πΊ(π½ππΆ)) β π |
15 | 2, 3, 5, 14 | nvcli 29653 |
. . . . . 6
β’ (πβ(π΄πΊ(π½ππΆ))) β β |
16 | 15 | recni 11177 |
. . . . 5
β’ (πβ(π΄πΊ(π½ππΆ))) β β |
17 | 16 | sqcli 14094 |
. . . 4
β’ ((πβ(π΄πΊ(π½ππΆ)))β2) β β |
18 | 7 | negcli 11477 |
. . . . . . . . 9
β’ -π½ β β |
19 | 2, 9 | nvscl 29617 |
. . . . . . . . 9
β’ ((π β NrmCVec β§ -π½ β β β§ πΆ β π) β (-π½ππΆ) β π) |
20 | 5, 18, 8, 19 | mp3an 1462 |
. . . . . . . 8
β’ (-π½ππΆ) β π |
21 | 2, 12 | nvgcl 29611 |
. . . . . . . 8
β’ ((π β NrmCVec β§ π΄ β π β§ (-π½ππΆ) β π) β (π΄πΊ(-π½ππΆ)) β π) |
22 | 5, 6, 20, 21 | mp3an 1462 |
. . . . . . 7
β’ (π΄πΊ(-π½ππΆ)) β π |
23 | 2, 3, 5, 22 | nvcli 29653 |
. . . . . 6
β’ (πβ(π΄πΊ(-π½ππΆ))) β β |
24 | 23 | recni 11177 |
. . . . 5
β’ (πβ(π΄πΊ(-π½ππΆ))) β β |
25 | 24 | sqcli 14094 |
. . . 4
β’ ((πβ(π΄πΊ(-π½ππΆ)))β2) β β |
26 | 1, 17, 25 | subdii 11612 |
. . 3
β’ (2
Β· (((πβ(π΄πΊ(π½ππΆ)))β2) β ((πβ(π΄πΊ(-π½ππΆ)))β2))) = ((2 Β· ((πβ(π΄πΊ(π½ππΆ)))β2)) β (2 Β· ((πβ(π΄πΊ(-π½ππΆ)))β2))) |
27 | 1, 17 | mulcli 11170 |
. . . 4
β’ (2
Β· ((πβ(π΄πΊ(π½ππΆ)))β2)) β β |
28 | 1, 25 | mulcli 11170 |
. . . 4
β’ (2
Β· ((πβ(π΄πΊ(-π½ππΆ)))β2)) β β |
29 | | ip1i.b |
. . . . . . . 8
β’ π΅ β π |
30 | 2, 3, 5, 29 | nvcli 29653 |
. . . . . . 7
β’ (πβπ΅) β β |
31 | 30 | recni 11177 |
. . . . . 6
β’ (πβπ΅) β β |
32 | 31 | sqcli 14094 |
. . . . 5
β’ ((πβπ΅)β2) β β |
33 | 1, 32 | mulcli 11170 |
. . . 4
β’ (2
Β· ((πβπ΅)β2)) β
β |
34 | | pnpcan2 11449 |
. . . 4
β’ (((2
Β· ((πβ(π΄πΊ(π½ππΆ)))β2)) β β β§ (2
Β· ((πβ(π΄πΊ(-π½ππΆ)))β2)) β β β§ (2
Β· ((πβπ΅)β2)) β β)
β (((2 Β· ((πβ(π΄πΊ(π½ππΆ)))β2)) + (2 Β· ((πβπ΅)β2))) β ((2 Β· ((πβ(π΄πΊ(-π½ππΆ)))β2)) + (2 Β· ((πβπ΅)β2)))) = ((2 Β· ((πβ(π΄πΊ(π½ππΆ)))β2)) β (2 Β· ((πβ(π΄πΊ(-π½ππΆ)))β2)))) |
35 | 27, 28, 33, 34 | mp3an 1462 |
. . 3
β’ (((2
Β· ((πβ(π΄πΊ(π½ππΆ)))β2)) + (2 Β· ((πβπ΅)β2))) β ((2 Β· ((πβ(π΄πΊ(-π½ππΆ)))β2)) + (2 Β· ((πβπ΅)β2)))) = ((2 Β· ((πβ(π΄πΊ(π½ππΆ)))β2)) β (2 Β· ((πβ(π΄πΊ(-π½ππΆ)))β2))) |
36 | 26, 35 | eqtr4i 2764 |
. 2
β’ (2
Β· (((πβ(π΄πΊ(π½ππΆ)))β2) β ((πβ(π΄πΊ(-π½ππΆ)))β2))) = (((2 Β· ((πβ(π΄πΊ(π½ππΆ)))β2)) + (2 Β· ((πβπ΅)β2))) β ((2 Β· ((πβ(π΄πΊ(-π½ππΆ)))β2)) + (2 Β· ((πβπ΅)β2)))) |
37 | | eqid 2733 |
. . . . . . . . . 10
β’
(1st βπ) = (1st βπ) |
38 | 37 | nvvc 29606 |
. . . . . . . . 9
β’ (π β NrmCVec β
(1st βπ)
β CVecOLD) |
39 | 12 | vafval 29594 |
. . . . . . . . . 10
β’ πΊ = (1st
β(1st βπ)) |
40 | 39 | vcablo 29560 |
. . . . . . . . 9
β’
((1st βπ) β CVecOLD β πΊ β AbelOp) |
41 | 5, 38, 40 | mp2b 10 |
. . . . . . . 8
β’ πΊ β AbelOp |
42 | 6, 29, 11 | 3pm3.2i 1340 |
. . . . . . . 8
β’ (π΄ β π β§ π΅ β π β§ (π½ππΆ) β π) |
43 | 2, 12 | bafval 29595 |
. . . . . . . . 9
β’ π = ran πΊ |
44 | 43 | ablo32 29540 |
. . . . . . . 8
β’ ((πΊ β AbelOp β§ (π΄ β π β§ π΅ β π β§ (π½ππΆ) β π)) β ((π΄πΊπ΅)πΊ(π½ππΆ)) = ((π΄πΊ(π½ππΆ))πΊπ΅)) |
45 | 41, 42, 44 | mp2an 691 |
. . . . . . 7
β’ ((π΄πΊπ΅)πΊ(π½ππΆ)) = ((π΄πΊ(π½ππΆ))πΊπ΅) |
46 | 45 | fveq2i 6849 |
. . . . . 6
β’ (πβ((π΄πΊπ΅)πΊ(π½ππΆ))) = (πβ((π΄πΊ(π½ππΆ))πΊπ΅)) |
47 | 46 | oveq1i 7371 |
. . . . 5
β’ ((πβ((π΄πΊπ΅)πΊ(π½ππΆ)))β2) = ((πβ((π΄πΊ(π½ππΆ))πΊπ΅))β2) |
48 | | neg1cn 12275 |
. . . . . . . . . 10
β’ -1 β
β |
49 | 2, 9 | nvscl 29617 |
. . . . . . . . . 10
β’ ((π β NrmCVec β§ -1 β
β β§ π΅ β
π) β (-1ππ΅) β π) |
50 | 5, 48, 29, 49 | mp3an 1462 |
. . . . . . . . 9
β’ (-1ππ΅) β π |
51 | 6, 50, 11 | 3pm3.2i 1340 |
. . . . . . . 8
β’ (π΄ β π β§ (-1ππ΅) β π β§ (π½ππΆ) β π) |
52 | 43 | ablo32 29540 |
. . . . . . . 8
β’ ((πΊ β AbelOp β§ (π΄ β π β§ (-1ππ΅) β π β§ (π½ππΆ) β π)) β ((π΄πΊ(-1ππ΅))πΊ(π½ππΆ)) = ((π΄πΊ(π½ππΆ))πΊ(-1ππ΅))) |
53 | 41, 51, 52 | mp2an 691 |
. . . . . . 7
β’ ((π΄πΊ(-1ππ΅))πΊ(π½ππΆ)) = ((π΄πΊ(π½ππΆ))πΊ(-1ππ΅)) |
54 | 53 | fveq2i 6849 |
. . . . . 6
β’ (πβ((π΄πΊ(-1ππ΅))πΊ(π½ππΆ))) = (πβ((π΄πΊ(π½ππΆ))πΊ(-1ππ΅))) |
55 | 54 | oveq1i 7371 |
. . . . 5
β’ ((πβ((π΄πΊ(-1ππ΅))πΊ(π½ππΆ)))β2) = ((πβ((π΄πΊ(π½ππΆ))πΊ(-1ππ΅)))β2) |
56 | 47, 55 | oveq12i 7373 |
. . . 4
β’ (((πβ((π΄πΊπ΅)πΊ(π½ππΆ)))β2) + ((πβ((π΄πΊ(-1ππ΅))πΊ(π½ππΆ)))β2)) = (((πβ((π΄πΊ(π½ππΆ))πΊπ΅))β2) + ((πβ((π΄πΊ(π½ππΆ))πΊ(-1ππ΅)))β2)) |
57 | 2, 12, 9, 3 | phpar 29815 |
. . . . 5
β’ ((π β CPreHilOLD
β§ (π΄πΊ(π½ππΆ)) β π β§ π΅ β π) β (((πβ((π΄πΊ(π½ππΆ))πΊπ΅))β2) + ((πβ((π΄πΊ(π½ππΆ))πΊ(-1ππ΅)))β2)) = (2 Β· (((πβ(π΄πΊ(π½ππΆ)))β2) + ((πβπ΅)β2)))) |
58 | 4, 14, 29, 57 | mp3an 1462 |
. . . 4
β’ (((πβ((π΄πΊ(π½ππΆ))πΊπ΅))β2) + ((πβ((π΄πΊ(π½ππΆ))πΊ(-1ππ΅)))β2)) = (2 Β· (((πβ(π΄πΊ(π½ππΆ)))β2) + ((πβπ΅)β2))) |
59 | 1, 17, 32 | adddii 11175 |
. . . 4
β’ (2
Β· (((πβ(π΄πΊ(π½ππΆ)))β2) + ((πβπ΅)β2))) = ((2 Β· ((πβ(π΄πΊ(π½ππΆ)))β2)) + (2 Β· ((πβπ΅)β2))) |
60 | 56, 58, 59 | 3eqtri 2765 |
. . 3
β’ (((πβ((π΄πΊπ΅)πΊ(π½ππΆ)))β2) + ((πβ((π΄πΊ(-1ππ΅))πΊ(π½ππΆ)))β2)) = ((2 Β· ((πβ(π΄πΊ(π½ππΆ)))β2)) + (2 Β· ((πβπ΅)β2))) |
61 | 6, 29, 20 | 3pm3.2i 1340 |
. . . . . . . 8
β’ (π΄ β π β§ π΅ β π β§ (-π½ππΆ) β π) |
62 | 43 | ablo32 29540 |
. . . . . . . 8
β’ ((πΊ β AbelOp β§ (π΄ β π β§ π΅ β π β§ (-π½ππΆ) β π)) β ((π΄πΊπ΅)πΊ(-π½ππΆ)) = ((π΄πΊ(-π½ππΆ))πΊπ΅)) |
63 | 41, 61, 62 | mp2an 691 |
. . . . . . 7
β’ ((π΄πΊπ΅)πΊ(-π½ππΆ)) = ((π΄πΊ(-π½ππΆ))πΊπ΅) |
64 | 63 | fveq2i 6849 |
. . . . . 6
β’ (πβ((π΄πΊπ΅)πΊ(-π½ππΆ))) = (πβ((π΄πΊ(-π½ππΆ))πΊπ΅)) |
65 | 64 | oveq1i 7371 |
. . . . 5
β’ ((πβ((π΄πΊπ΅)πΊ(-π½ππΆ)))β2) = ((πβ((π΄πΊ(-π½ππΆ))πΊπ΅))β2) |
66 | 6, 50, 20 | 3pm3.2i 1340 |
. . . . . . . 8
β’ (π΄ β π β§ (-1ππ΅) β π β§ (-π½ππΆ) β π) |
67 | 43 | ablo32 29540 |
. . . . . . . 8
β’ ((πΊ β AbelOp β§ (π΄ β π β§ (-1ππ΅) β π β§ (-π½ππΆ) β π)) β ((π΄πΊ(-1ππ΅))πΊ(-π½ππΆ)) = ((π΄πΊ(-π½ππΆ))πΊ(-1ππ΅))) |
68 | 41, 66, 67 | mp2an 691 |
. . . . . . 7
β’ ((π΄πΊ(-1ππ΅))πΊ(-π½ππΆ)) = ((π΄πΊ(-π½ππΆ))πΊ(-1ππ΅)) |
69 | 68 | fveq2i 6849 |
. . . . . 6
β’ (πβ((π΄πΊ(-1ππ΅))πΊ(-π½ππΆ))) = (πβ((π΄πΊ(-π½ππΆ))πΊ(-1ππ΅))) |
70 | 69 | oveq1i 7371 |
. . . . 5
β’ ((πβ((π΄πΊ(-1ππ΅))πΊ(-π½ππΆ)))β2) = ((πβ((π΄πΊ(-π½ππΆ))πΊ(-1ππ΅)))β2) |
71 | 65, 70 | oveq12i 7373 |
. . . 4
β’ (((πβ((π΄πΊπ΅)πΊ(-π½ππΆ)))β2) + ((πβ((π΄πΊ(-1ππ΅))πΊ(-π½ππΆ)))β2)) = (((πβ((π΄πΊ(-π½ππΆ))πΊπ΅))β2) + ((πβ((π΄πΊ(-π½ππΆ))πΊ(-1ππ΅)))β2)) |
72 | 2, 12, 9, 3 | phpar 29815 |
. . . . 5
β’ ((π β CPreHilOLD
β§ (π΄πΊ(-π½ππΆ)) β π β§ π΅ β π) β (((πβ((π΄πΊ(-π½ππΆ))πΊπ΅))β2) + ((πβ((π΄πΊ(-π½ππΆ))πΊ(-1ππ΅)))β2)) = (2 Β· (((πβ(π΄πΊ(-π½ππΆ)))β2) + ((πβπ΅)β2)))) |
73 | 4, 22, 29, 72 | mp3an 1462 |
. . . 4
β’ (((πβ((π΄πΊ(-π½ππΆ))πΊπ΅))β2) + ((πβ((π΄πΊ(-π½ππΆ))πΊ(-1ππ΅)))β2)) = (2 Β· (((πβ(π΄πΊ(-π½ππΆ)))β2) + ((πβπ΅)β2))) |
74 | 1, 25, 32 | adddii 11175 |
. . . 4
β’ (2
Β· (((πβ(π΄πΊ(-π½ππΆ)))β2) + ((πβπ΅)β2))) = ((2 Β· ((πβ(π΄πΊ(-π½ππΆ)))β2)) + (2 Β· ((πβπ΅)β2))) |
75 | 71, 73, 74 | 3eqtri 2765 |
. . 3
β’ (((πβ((π΄πΊπ΅)πΊ(-π½ππΆ)))β2) + ((πβ((π΄πΊ(-1ππ΅))πΊ(-π½ππΆ)))β2)) = ((2 Β· ((πβ(π΄πΊ(-π½ππΆ)))β2)) + (2 Β· ((πβπ΅)β2))) |
76 | 60, 75 | oveq12i 7373 |
. 2
β’ ((((πβ((π΄πΊπ΅)πΊ(π½ππΆ)))β2) + ((πβ((π΄πΊ(-1ππ΅))πΊ(π½ππΆ)))β2)) β (((πβ((π΄πΊπ΅)πΊ(-π½ππΆ)))β2) + ((πβ((π΄πΊ(-1ππ΅))πΊ(-π½ππΆ)))β2))) = (((2 Β· ((πβ(π΄πΊ(π½ππΆ)))β2)) + (2 Β· ((πβπ΅)β2))) β ((2 Β· ((πβ(π΄πΊ(-π½ππΆ)))β2)) + (2 Β· ((πβπ΅)β2)))) |
77 | 2, 12 | nvgcl 29611 |
. . . . . . . 8
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (π΄πΊπ΅) β π) |
78 | 5, 6, 29, 77 | mp3an 1462 |
. . . . . . 7
β’ (π΄πΊπ΅) β π |
79 | 2, 12 | nvgcl 29611 |
. . . . . . 7
β’ ((π β NrmCVec β§ (π΄πΊπ΅) β π β§ (π½ππΆ) β π) β ((π΄πΊπ΅)πΊ(π½ππΆ)) β π) |
80 | 5, 78, 11, 79 | mp3an 1462 |
. . . . . 6
β’ ((π΄πΊπ΅)πΊ(π½ππΆ)) β π |
81 | 2, 3, 5, 80 | nvcli 29653 |
. . . . 5
β’ (πβ((π΄πΊπ΅)πΊ(π½ππΆ))) β β |
82 | 81 | recni 11177 |
. . . 4
β’ (πβ((π΄πΊπ΅)πΊ(π½ππΆ))) β β |
83 | 82 | sqcli 14094 |
. . 3
β’ ((πβ((π΄πΊπ΅)πΊ(π½ππΆ)))β2) β β |
84 | 2, 12 | nvgcl 29611 |
. . . . . . . 8
β’ ((π β NrmCVec β§ π΄ β π β§ (-1ππ΅) β π) β (π΄πΊ(-1ππ΅)) β π) |
85 | 5, 6, 50, 84 | mp3an 1462 |
. . . . . . 7
β’ (π΄πΊ(-1ππ΅)) β π |
86 | 2, 12 | nvgcl 29611 |
. . . . . . 7
β’ ((π β NrmCVec β§ (π΄πΊ(-1ππ΅)) β π β§ (π½ππΆ) β π) β ((π΄πΊ(-1ππ΅))πΊ(π½ππΆ)) β π) |
87 | 5, 85, 11, 86 | mp3an 1462 |
. . . . . 6
β’ ((π΄πΊ(-1ππ΅))πΊ(π½ππΆ)) β π |
88 | 2, 3, 5, 87 | nvcli 29653 |
. . . . 5
β’ (πβ((π΄πΊ(-1ππ΅))πΊ(π½ππΆ))) β β |
89 | 88 | recni 11177 |
. . . 4
β’ (πβ((π΄πΊ(-1ππ΅))πΊ(π½ππΆ))) β β |
90 | 89 | sqcli 14094 |
. . 3
β’ ((πβ((π΄πΊ(-1ππ΅))πΊ(π½ππΆ)))β2) β β |
91 | 2, 12 | nvgcl 29611 |
. . . . . . 7
β’ ((π β NrmCVec β§ (π΄πΊπ΅) β π β§ (-π½ππΆ) β π) β ((π΄πΊπ΅)πΊ(-π½ππΆ)) β π) |
92 | 5, 78, 20, 91 | mp3an 1462 |
. . . . . 6
β’ ((π΄πΊπ΅)πΊ(-π½ππΆ)) β π |
93 | 2, 3, 5, 92 | nvcli 29653 |
. . . . 5
β’ (πβ((π΄πΊπ΅)πΊ(-π½ππΆ))) β β |
94 | 93 | recni 11177 |
. . . 4
β’ (πβ((π΄πΊπ΅)πΊ(-π½ππΆ))) β β |
95 | 94 | sqcli 14094 |
. . 3
β’ ((πβ((π΄πΊπ΅)πΊ(-π½ππΆ)))β2) β β |
96 | 2, 12 | nvgcl 29611 |
. . . . . . 7
β’ ((π β NrmCVec β§ (π΄πΊ(-1ππ΅)) β π β§ (-π½ππΆ) β π) β ((π΄πΊ(-1ππ΅))πΊ(-π½ππΆ)) β π) |
97 | 5, 85, 20, 96 | mp3an 1462 |
. . . . . 6
β’ ((π΄πΊ(-1ππ΅))πΊ(-π½ππΆ)) β π |
98 | 2, 3, 5, 97 | nvcli 29653 |
. . . . 5
β’ (πβ((π΄πΊ(-1ππ΅))πΊ(-π½ππΆ))) β β |
99 | 98 | recni 11177 |
. . . 4
β’ (πβ((π΄πΊ(-1ππ΅))πΊ(-π½ππΆ))) β β |
100 | 99 | sqcli 14094 |
. . 3
β’ ((πβ((π΄πΊ(-1ππ΅))πΊ(-π½ππΆ)))β2) β β |
101 | 83, 90, 95, 100 | addsub4i 11505 |
. 2
β’ ((((πβ((π΄πΊπ΅)πΊ(π½ππΆ)))β2) + ((πβ((π΄πΊ(-1ππ΅))πΊ(π½ππΆ)))β2)) β (((πβ((π΄πΊπ΅)πΊ(-π½ππΆ)))β2) + ((πβ((π΄πΊ(-1ππ΅))πΊ(-π½ππΆ)))β2))) = ((((πβ((π΄πΊπ΅)πΊ(π½ππΆ)))β2) β ((πβ((π΄πΊπ΅)πΊ(-π½ππΆ)))β2)) + (((πβ((π΄πΊ(-1ππ΅))πΊ(π½ππΆ)))β2) β ((πβ((π΄πΊ(-1ππ΅))πΊ(-π½ππΆ)))β2))) |
102 | 36, 76, 101 | 3eqtr2ri 2768 |
1
β’ ((((πβ((π΄πΊπ΅)πΊ(π½ππΆ)))β2) β ((πβ((π΄πΊπ΅)πΊ(-π½ππΆ)))β2)) + (((πβ((π΄πΊ(-1ππ΅))πΊ(π½ππΆ)))β2) β ((πβ((π΄πΊ(-1ππ΅))πΊ(-π½ππΆ)))β2))) = (2 Β· (((πβ(π΄πΊ(π½ππΆ)))β2) β ((πβ(π΄πΊ(-π½ππΆ)))β2))) |