Step | Hyp | Ref
| Expression |
1 | | 2cn 12289 |
. . . . . . 7
β’ 2 β
β |
2 | | 2ne0 12318 |
. . . . . . 7
β’ 2 β
0 |
3 | 1, 2 | recidi 11947 |
. . . . . 6
β’ (2
Β· (1 / 2)) = 1 |
4 | 3 | oveq1i 7421 |
. . . . 5
β’ ((2
Β· (1 / 2))π(π΄πΊπ΅)) = (1π(π΄πΊπ΅)) |
5 | | ip1i.9 |
. . . . . . 7
β’ π β
CPreHilOLD |
6 | 5 | phnvi 30107 |
. . . . . 6
β’ π β NrmCVec |
7 | | halfcn 12429 |
. . . . . . 7
β’ (1 / 2)
β β |
8 | | ipdiri.8 |
. . . . . . . 8
β’ π΄ β π |
9 | | ipdiri.9 |
. . . . . . . 8
β’ π΅ β π |
10 | | ip1i.1 |
. . . . . . . . 9
β’ π = (BaseSetβπ) |
11 | | ip1i.2 |
. . . . . . . . 9
β’ πΊ = ( +π£
βπ) |
12 | 10, 11 | nvgcl 29911 |
. . . . . . . 8
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (π΄πΊπ΅) β π) |
13 | 6, 8, 9, 12 | mp3an 1461 |
. . . . . . 7
β’ (π΄πΊπ΅) β π |
14 | 1, 7, 13 | 3pm3.2i 1339 |
. . . . . 6
β’ (2 β
β β§ (1 / 2) β β β§ (π΄πΊπ΅) β π) |
15 | | ip1i.4 |
. . . . . . 7
β’ π = (
Β·π OLD βπ) |
16 | 10, 15 | nvsass 29919 |
. . . . . 6
β’ ((π β NrmCVec β§ (2 β
β β§ (1 / 2) β β β§ (π΄πΊπ΅) β π)) β ((2 Β· (1 / 2))π(π΄πΊπ΅)) = (2π((1 / 2)π(π΄πΊπ΅)))) |
17 | 6, 14, 16 | mp2an 690 |
. . . . 5
β’ ((2
Β· (1 / 2))π(π΄πΊπ΅)) = (2π((1 / 2)π(π΄πΊπ΅))) |
18 | 10, 15 | nvsid 29918 |
. . . . . 6
β’ ((π β NrmCVec β§ (π΄πΊπ΅) β π) β (1π(π΄πΊπ΅)) = (π΄πΊπ΅)) |
19 | 6, 13, 18 | mp2an 690 |
. . . . 5
β’ (1π(π΄πΊπ΅)) = (π΄πΊπ΅) |
20 | 4, 17, 19 | 3eqtr3i 2768 |
. . . 4
β’ (2π((1 / 2)π(π΄πΊπ΅))) = (π΄πΊπ΅) |
21 | 20 | oveq1i 7421 |
. . 3
β’ ((2π((1 / 2)π(π΄πΊπ΅)))ππΆ) = ((π΄πΊπ΅)ππΆ) |
22 | | ip1i.7 |
. . . 4
β’ π =
(Β·πOLDβπ) |
23 | 10, 15 | nvscl 29917 |
. . . . 5
β’ ((π β NrmCVec β§ (1 / 2)
β β β§ (π΄πΊπ΅) β π) β ((1 / 2)π(π΄πΊπ΅)) β π) |
24 | 6, 7, 13, 23 | mp3an 1461 |
. . . 4
β’ ((1 /
2)π(π΄πΊπ΅)) β π |
25 | | ipdiri.10 |
. . . 4
β’ πΆ β π |
26 | 10, 11, 15, 22, 5, 24, 25 | ip2i 30119 |
. . 3
β’ ((2π((1 / 2)π(π΄πΊπ΅)))ππΆ) = (2 Β· (((1 / 2)π(π΄πΊπ΅))ππΆ)) |
27 | 21, 26 | eqtr3i 2762 |
. 2
β’ ((π΄πΊπ΅)ππΆ) = (2 Β· (((1 / 2)π(π΄πΊπ΅))ππΆ)) |
28 | | neg1cn 12328 |
. . . . . 6
β’ -1 β
β |
29 | 10, 15 | nvscl 29917 |
. . . . . 6
β’ ((π β NrmCVec β§ -1 β
β β§ π΅ β
π) β (-1ππ΅) β π) |
30 | 6, 28, 9, 29 | mp3an 1461 |
. . . . 5
β’ (-1ππ΅) β π |
31 | 10, 11 | nvgcl 29911 |
. . . . 5
β’ ((π β NrmCVec β§ π΄ β π β§ (-1ππ΅) β π) β (π΄πΊ(-1ππ΅)) β π) |
32 | 6, 8, 30, 31 | mp3an 1461 |
. . . 4
β’ (π΄πΊ(-1ππ΅)) β π |
33 | 10, 15 | nvscl 29917 |
. . . 4
β’ ((π β NrmCVec β§ (1 / 2)
β β β§ (π΄πΊ(-1ππ΅)) β π) β ((1 / 2)π(π΄πΊ(-1ππ΅))) β π) |
34 | 6, 7, 32, 33 | mp3an 1461 |
. . 3
β’ ((1 /
2)π(π΄πΊ(-1ππ΅))) β π |
35 | 10, 11, 15, 22, 5, 24, 34, 25 | ip1i 30118 |
. 2
β’ (((((1 /
2)π(π΄πΊπ΅))πΊ((1 / 2)π(π΄πΊ(-1ππ΅))))ππΆ) + ((((1 / 2)π(π΄πΊπ΅))πΊ(-1π((1 / 2)π(π΄πΊ(-1ππ΅)))))ππΆ)) = (2 Β· (((1 / 2)π(π΄πΊπ΅))ππΆ)) |
36 | | eqid 2732 |
. . . . . . . . . . . 12
β’
(1st βπ) = (1st βπ) |
37 | 36 | nvvc 29906 |
. . . . . . . . . . 11
β’ (π β NrmCVec β
(1st βπ)
β CVecOLD) |
38 | 6, 37 | ax-mp 5 |
. . . . . . . . . 10
β’
(1st βπ) β CVecOLD |
39 | 11 | vafval 29894 |
. . . . . . . . . . 11
β’ πΊ = (1st
β(1st βπ)) |
40 | 39 | vcablo 29860 |
. . . . . . . . . 10
β’
((1st βπ) β CVecOLD β πΊ β AbelOp) |
41 | 38, 40 | ax-mp 5 |
. . . . . . . . 9
β’ πΊ β AbelOp |
42 | 8, 9 | pm3.2i 471 |
. . . . . . . . 9
β’ (π΄ β π β§ π΅ β π) |
43 | 8, 30 | pm3.2i 471 |
. . . . . . . . 9
β’ (π΄ β π β§ (-1ππ΅) β π) |
44 | 10, 11 | bafval 29895 |
. . . . . . . . . 10
β’ π = ran πΊ |
45 | 44 | ablo4 29841 |
. . . . . . . . 9
β’ ((πΊ β AbelOp β§ (π΄ β π β§ π΅ β π) β§ (π΄ β π β§ (-1ππ΅) β π)) β ((π΄πΊπ΅)πΊ(π΄πΊ(-1ππ΅))) = ((π΄πΊπ΄)πΊ(π΅πΊ(-1ππ΅)))) |
46 | 41, 42, 43, 45 | mp3an 1461 |
. . . . . . . 8
β’ ((π΄πΊπ΅)πΊ(π΄πΊ(-1ππ΅))) = ((π΄πΊπ΄)πΊ(π΅πΊ(-1ππ΅))) |
47 | 15 | smfval 29896 |
. . . . . . . . . . 11
β’ π = (2nd
β(1st βπ)) |
48 | 39, 47, 44 | vc2OLD 29859 |
. . . . . . . . . 10
β’
(((1st βπ) β CVecOLD β§ π΄ β π) β (π΄πΊπ΄) = (2ππ΄)) |
49 | 38, 8, 48 | mp2an 690 |
. . . . . . . . 9
β’ (π΄πΊπ΄) = (2ππ΄) |
50 | | eqid 2732 |
. . . . . . . . . . 11
β’
(0vecβπ) = (0vecβπ) |
51 | 10, 11, 15, 50 | nvrinv 29942 |
. . . . . . . . . 10
β’ ((π β NrmCVec β§ π΅ β π) β (π΅πΊ(-1ππ΅)) = (0vecβπ)) |
52 | 6, 9, 51 | mp2an 690 |
. . . . . . . . 9
β’ (π΅πΊ(-1ππ΅)) = (0vecβπ) |
53 | 49, 52 | oveq12i 7423 |
. . . . . . . 8
β’ ((π΄πΊπ΄)πΊ(π΅πΊ(-1ππ΅))) = ((2ππ΄)πΊ(0vecβπ)) |
54 | 10, 15 | nvscl 29917 |
. . . . . . . . . 10
β’ ((π β NrmCVec β§ 2 β
β β§ π΄ β
π) β (2ππ΄) β π) |
55 | 6, 1, 8, 54 | mp3an 1461 |
. . . . . . . . 9
β’ (2ππ΄) β π |
56 | 10, 11, 50 | nv0rid 29926 |
. . . . . . . . 9
β’ ((π β NrmCVec β§ (2ππ΄) β π) β ((2ππ΄)πΊ(0vecβπ)) = (2ππ΄)) |
57 | 6, 55, 56 | mp2an 690 |
. . . . . . . 8
β’ ((2ππ΄)πΊ(0vecβπ)) = (2ππ΄) |
58 | 46, 53, 57 | 3eqtri 2764 |
. . . . . . 7
β’ ((π΄πΊπ΅)πΊ(π΄πΊ(-1ππ΅))) = (2ππ΄) |
59 | 58 | oveq2i 7422 |
. . . . . 6
β’ ((1 /
2)π((π΄πΊπ΅)πΊ(π΄πΊ(-1ππ΅)))) = ((1 / 2)π(2ππ΄)) |
60 | 7, 1, 8 | 3pm3.2i 1339 |
. . . . . . 7
β’ ((1 / 2)
β β β§ 2 β β β§ π΄ β π) |
61 | 10, 15 | nvsass 29919 |
. . . . . . 7
β’ ((π β NrmCVec β§ ((1 / 2)
β β β§ 2 β β β§ π΄ β π)) β (((1 / 2) Β· 2)ππ΄) = ((1 / 2)π(2ππ΄))) |
62 | 6, 60, 61 | mp2an 690 |
. . . . . 6
β’ (((1 / 2)
Β· 2)ππ΄) = ((1 / 2)π(2ππ΄)) |
63 | 59, 62 | eqtr4i 2763 |
. . . . 5
β’ ((1 /
2)π((π΄πΊπ΅)πΊ(π΄πΊ(-1ππ΅)))) = (((1 / 2) Β· 2)ππ΄) |
64 | 7, 13, 32 | 3pm3.2i 1339 |
. . . . . 6
β’ ((1 / 2)
β β β§ (π΄πΊπ΅) β π β§ (π΄πΊ(-1ππ΅)) β π) |
65 | 10, 11, 15 | nvdi 29921 |
. . . . . 6
β’ ((π β NrmCVec β§ ((1 / 2)
β β β§ (π΄πΊπ΅) β π β§ (π΄πΊ(-1ππ΅)) β π)) β ((1 / 2)π((π΄πΊπ΅)πΊ(π΄πΊ(-1ππ΅)))) = (((1 / 2)π(π΄πΊπ΅))πΊ((1 / 2)π(π΄πΊ(-1ππ΅))))) |
66 | 6, 64, 65 | mp2an 690 |
. . . . 5
β’ ((1 /
2)π((π΄πΊπ΅)πΊ(π΄πΊ(-1ππ΅)))) = (((1 / 2)π(π΄πΊπ΅))πΊ((1 / 2)π(π΄πΊ(-1ππ΅)))) |
67 | | ax-1cn 11170 |
. . . . . . . 8
β’ 1 β
β |
68 | 67, 1, 2 | divcan1i 11960 |
. . . . . . 7
β’ ((1 / 2)
Β· 2) = 1 |
69 | 68 | oveq1i 7421 |
. . . . . 6
β’ (((1 / 2)
Β· 2)ππ΄) = (1ππ΄) |
70 | 10, 15 | nvsid 29918 |
. . . . . . 7
β’ ((π β NrmCVec β§ π΄ β π) β (1ππ΄) = π΄) |
71 | 6, 8, 70 | mp2an 690 |
. . . . . 6
β’ (1ππ΄) = π΄ |
72 | 69, 71 | eqtri 2760 |
. . . . 5
β’ (((1 / 2)
Β· 2)ππ΄) = π΄ |
73 | 63, 66, 72 | 3eqtr3i 2768 |
. . . 4
β’ (((1 /
2)π(π΄πΊπ΅))πΊ((1 / 2)π(π΄πΊ(-1ππ΅)))) = π΄ |
74 | 73 | oveq1i 7421 |
. . 3
β’ ((((1 /
2)π(π΄πΊπ΅))πΊ((1 / 2)π(π΄πΊ(-1ππ΅))))ππΆ) = (π΄ππΆ) |
75 | 28, 7 | mulcomi 11224 |
. . . . . . . . 9
β’ (-1
Β· (1 / 2)) = ((1 / 2) Β· -1) |
76 | 75 | oveq1i 7421 |
. . . . . . . 8
β’ ((-1
Β· (1 / 2))π(π΄πΊ(-1ππ΅))) = (((1 / 2) Β· -1)π(π΄πΊ(-1ππ΅))) |
77 | 28, 7, 32 | 3pm3.2i 1339 |
. . . . . . . . 9
β’ (-1
β β β§ (1 / 2) β β β§ (π΄πΊ(-1ππ΅)) β π) |
78 | 10, 15 | nvsass 29919 |
. . . . . . . . 9
β’ ((π β NrmCVec β§ (-1 β
β β§ (1 / 2) β β β§ (π΄πΊ(-1ππ΅)) β π)) β ((-1 Β· (1 / 2))π(π΄πΊ(-1ππ΅))) = (-1π((1 / 2)π(π΄πΊ(-1ππ΅))))) |
79 | 6, 77, 78 | mp2an 690 |
. . . . . . . 8
β’ ((-1
Β· (1 / 2))π(π΄πΊ(-1ππ΅))) = (-1π((1 / 2)π(π΄πΊ(-1ππ΅)))) |
80 | 7, 28, 32 | 3pm3.2i 1339 |
. . . . . . . . . 10
β’ ((1 / 2)
β β β§ -1 β β β§ (π΄πΊ(-1ππ΅)) β π) |
81 | 10, 15 | nvsass 29919 |
. . . . . . . . . 10
β’ ((π β NrmCVec β§ ((1 / 2)
β β β§ -1 β β β§ (π΄πΊ(-1ππ΅)) β π)) β (((1 / 2) Β· -1)π(π΄πΊ(-1ππ΅))) = ((1 / 2)π(-1π(π΄πΊ(-1ππ΅))))) |
82 | 6, 80, 81 | mp2an 690 |
. . . . . . . . 9
β’ (((1 / 2)
Β· -1)π(π΄πΊ(-1ππ΅))) = ((1 / 2)π(-1π(π΄πΊ(-1ππ΅)))) |
83 | 28, 8, 30 | 3pm3.2i 1339 |
. . . . . . . . . . . 12
β’ (-1
β β β§ π΄
β π β§ (-1ππ΅) β π) |
84 | 10, 11, 15 | nvdi 29921 |
. . . . . . . . . . . 12
β’ ((π β NrmCVec β§ (-1 β
β β§ π΄ β
π β§ (-1ππ΅) β π)) β (-1π(π΄πΊ(-1ππ΅))) = ((-1ππ΄)πΊ(-1π(-1ππ΅)))) |
85 | 6, 83, 84 | mp2an 690 |
. . . . . . . . . . 11
β’ (-1π(π΄πΊ(-1ππ΅))) = ((-1ππ΄)πΊ(-1π(-1ππ΅))) |
86 | | neg1mulneg1e1 12427 |
. . . . . . . . . . . . . 14
β’ (-1
Β· -1) = 1 |
87 | 86 | oveq1i 7421 |
. . . . . . . . . . . . 13
β’ ((-1
Β· -1)ππ΅) = (1ππ΅) |
88 | 28, 28, 9 | 3pm3.2i 1339 |
. . . . . . . . . . . . . 14
β’ (-1
β β β§ -1 β β β§ π΅ β π) |
89 | 10, 15 | nvsass 29919 |
. . . . . . . . . . . . . 14
β’ ((π β NrmCVec β§ (-1 β
β β§ -1 β β β§ π΅ β π)) β ((-1 Β· -1)ππ΅) = (-1π(-1ππ΅))) |
90 | 6, 88, 89 | mp2an 690 |
. . . . . . . . . . . . 13
β’ ((-1
Β· -1)ππ΅) = (-1π(-1ππ΅)) |
91 | 10, 15 | nvsid 29918 |
. . . . . . . . . . . . . 14
β’ ((π β NrmCVec β§ π΅ β π) β (1ππ΅) = π΅) |
92 | 6, 9, 91 | mp2an 690 |
. . . . . . . . . . . . 13
β’ (1ππ΅) = π΅ |
93 | 87, 90, 92 | 3eqtr3i 2768 |
. . . . . . . . . . . 12
β’ (-1π(-1ππ΅)) = π΅ |
94 | 93 | oveq2i 7422 |
. . . . . . . . . . 11
β’ ((-1ππ΄)πΊ(-1π(-1ππ΅))) = ((-1ππ΄)πΊπ΅) |
95 | 85, 94 | eqtri 2760 |
. . . . . . . . . 10
β’ (-1π(π΄πΊ(-1ππ΅))) = ((-1ππ΄)πΊπ΅) |
96 | 95 | oveq2i 7422 |
. . . . . . . . 9
β’ ((1 /
2)π(-1π(π΄πΊ(-1ππ΅)))) = ((1 / 2)π((-1ππ΄)πΊπ΅)) |
97 | 82, 96 | eqtri 2760 |
. . . . . . . 8
β’ (((1 / 2)
Β· -1)π(π΄πΊ(-1ππ΅))) = ((1 / 2)π((-1ππ΄)πΊπ΅)) |
98 | 76, 79, 97 | 3eqtr3i 2768 |
. . . . . . 7
β’ (-1π((1 / 2)π(π΄πΊ(-1ππ΅)))) = ((1 / 2)π((-1ππ΄)πΊπ΅)) |
99 | 98 | oveq2i 7422 |
. . . . . 6
β’ (((1 /
2)π(π΄πΊπ΅))πΊ(-1π((1 / 2)π(π΄πΊ(-1ππ΅))))) = (((1 / 2)π(π΄πΊπ΅))πΊ((1 / 2)π((-1ππ΄)πΊπ΅))) |
100 | 10, 15 | nvscl 29917 |
. . . . . . . . . 10
β’ ((π β NrmCVec β§ -1 β
β β§ π΄ β
π) β (-1ππ΄) β π) |
101 | 6, 28, 8, 100 | mp3an 1461 |
. . . . . . . . 9
β’ (-1ππ΄) β π |
102 | 10, 11 | nvgcl 29911 |
. . . . . . . . 9
β’ ((π β NrmCVec β§ (-1ππ΄) β π β§ π΅ β π) β ((-1ππ΄)πΊπ΅) β π) |
103 | 6, 101, 9, 102 | mp3an 1461 |
. . . . . . . 8
β’ ((-1ππ΄)πΊπ΅) β π |
104 | 7, 13, 103 | 3pm3.2i 1339 |
. . . . . . 7
β’ ((1 / 2)
β β β§ (π΄πΊπ΅) β π β§ ((-1ππ΄)πΊπ΅) β π) |
105 | 10, 11, 15 | nvdi 29921 |
. . . . . . 7
β’ ((π β NrmCVec β§ ((1 / 2)
β β β§ (π΄πΊπ΅) β π β§ ((-1ππ΄)πΊπ΅) β π)) β ((1 / 2)π((π΄πΊπ΅)πΊ((-1ππ΄)πΊπ΅))) = (((1 / 2)π(π΄πΊπ΅))πΊ((1 / 2)π((-1ππ΄)πΊπ΅)))) |
106 | 6, 104, 105 | mp2an 690 |
. . . . . 6
β’ ((1 /
2)π((π΄πΊπ΅)πΊ((-1ππ΄)πΊπ΅))) = (((1 / 2)π(π΄πΊπ΅))πΊ((1 / 2)π((-1ππ΄)πΊπ΅))) |
107 | 99, 106 | eqtr4i 2763 |
. . . . 5
β’ (((1 /
2)π(π΄πΊπ΅))πΊ(-1π((1 / 2)π(π΄πΊ(-1ππ΅))))) = ((1 / 2)π((π΄πΊπ΅)πΊ((-1ππ΄)πΊπ΅))) |
108 | 101, 9 | pm3.2i 471 |
. . . . . . . . 9
β’ ((-1ππ΄) β π β§ π΅ β π) |
109 | 44 | ablo4 29841 |
. . . . . . . . 9
β’ ((πΊ β AbelOp β§ (π΄ β π β§ π΅ β π) β§ ((-1ππ΄) β π β§ π΅ β π)) β ((π΄πΊπ΅)πΊ((-1ππ΄)πΊπ΅)) = ((π΄πΊ(-1ππ΄))πΊ(π΅πΊπ΅))) |
110 | 41, 42, 108, 109 | mp3an 1461 |
. . . . . . . 8
β’ ((π΄πΊπ΅)πΊ((-1ππ΄)πΊπ΅)) = ((π΄πΊ(-1ππ΄))πΊ(π΅πΊπ΅)) |
111 | 10, 11, 15, 50 | nvrinv 29942 |
. . . . . . . . . . 11
β’ ((π β NrmCVec β§ π΄ β π) β (π΄πΊ(-1ππ΄)) = (0vecβπ)) |
112 | 6, 8, 111 | mp2an 690 |
. . . . . . . . . 10
β’ (π΄πΊ(-1ππ΄)) = (0vecβπ) |
113 | 112 | oveq1i 7421 |
. . . . . . . . 9
β’ ((π΄πΊ(-1ππ΄))πΊ(π΅πΊπ΅)) = ((0vecβπ)πΊ(π΅πΊπ΅)) |
114 | 10, 11 | nvgcl 29911 |
. . . . . . . . . . 11
β’ ((π β NrmCVec β§ π΅ β π β§ π΅ β π) β (π΅πΊπ΅) β π) |
115 | 6, 9, 9, 114 | mp3an 1461 |
. . . . . . . . . 10
β’ (π΅πΊπ΅) β π |
116 | 10, 11, 50 | nv0lid 29927 |
. . . . . . . . . 10
β’ ((π β NrmCVec β§ (π΅πΊπ΅) β π) β ((0vecβπ)πΊ(π΅πΊπ΅)) = (π΅πΊπ΅)) |
117 | 6, 115, 116 | mp2an 690 |
. . . . . . . . 9
β’
((0vecβπ)πΊ(π΅πΊπ΅)) = (π΅πΊπ΅) |
118 | 113, 117 | eqtri 2760 |
. . . . . . . 8
β’ ((π΄πΊ(-1ππ΄))πΊ(π΅πΊπ΅)) = (π΅πΊπ΅) |
119 | 39, 47, 44 | vc2OLD 29859 |
. . . . . . . . 9
β’
(((1st βπ) β CVecOLD β§ π΅ β π) β (π΅πΊπ΅) = (2ππ΅)) |
120 | 38, 9, 119 | mp2an 690 |
. . . . . . . 8
β’ (π΅πΊπ΅) = (2ππ΅) |
121 | 110, 118,
120 | 3eqtri 2764 |
. . . . . . 7
β’ ((π΄πΊπ΅)πΊ((-1ππ΄)πΊπ΅)) = (2ππ΅) |
122 | 121 | oveq2i 7422 |
. . . . . 6
β’ ((1 /
2)π((π΄πΊπ΅)πΊ((-1ππ΄)πΊπ΅))) = ((1 / 2)π(2ππ΅)) |
123 | 7, 1, 9 | 3pm3.2i 1339 |
. . . . . . 7
β’ ((1 / 2)
β β β§ 2 β β β§ π΅ β π) |
124 | 10, 15 | nvsass 29919 |
. . . . . . 7
β’ ((π β NrmCVec β§ ((1 / 2)
β β β§ 2 β β β§ π΅ β π)) β (((1 / 2) Β· 2)ππ΅) = ((1 / 2)π(2ππ΅))) |
125 | 6, 123, 124 | mp2an 690 |
. . . . . 6
β’ (((1 / 2)
Β· 2)ππ΅) = ((1 / 2)π(2ππ΅)) |
126 | 68 | oveq1i 7421 |
. . . . . 6
β’ (((1 / 2)
Β· 2)ππ΅) = (1ππ΅) |
127 | 122, 125,
126 | 3eqtr2i 2766 |
. . . . 5
β’ ((1 /
2)π((π΄πΊπ΅)πΊ((-1ππ΄)πΊπ΅))) = (1ππ΅) |
128 | 107, 127,
92 | 3eqtri 2764 |
. . . 4
β’ (((1 /
2)π(π΄πΊπ΅))πΊ(-1π((1 / 2)π(π΄πΊ(-1ππ΅))))) = π΅ |
129 | 128 | oveq1i 7421 |
. . 3
β’ ((((1 /
2)π(π΄πΊπ΅))πΊ(-1π((1 / 2)π(π΄πΊ(-1ππ΅)))))ππΆ) = (π΅ππΆ) |
130 | 74, 129 | oveq12i 7423 |
. 2
β’ (((((1 /
2)π(π΄πΊπ΅))πΊ((1 / 2)π(π΄πΊ(-1ππ΅))))ππΆ) + ((((1 / 2)π(π΄πΊπ΅))πΊ(-1π((1 / 2)π(π΄πΊ(-1ππ΅)))))ππΆ)) = ((π΄ππΆ) + (π΅ππΆ)) |
131 | 27, 35, 130 | 3eqtr2i 2766 |
1
β’ ((π΄πΊπ΅)ππΆ) = ((π΄ππΆ) + (π΅ππΆ)) |