Step | Hyp | Ref
| Expression |
1 | | ipcl.1 |
. . . 4
β’ π = (BaseSetβπ) |
2 | | eqid 2733 |
. . . 4
β’ (
+π£ βπ) = ( +π£ βπ) |
3 | | eqid 2733 |
. . . 4
β’ (
Β·π OLD βπ) = ( Β·π OLD
βπ) |
4 | | eqid 2733 |
. . . 4
β’
(normCVβπ) = (normCVβπ) |
5 | | ipcl.7 |
. . . 4
β’ π =
(Β·πOLDβπ) |
6 | 1, 2, 3, 4, 5 | ipval2 29691 |
. . 3
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (π΄ππ΅) = ((((((normCVβπ)β(π΄( +π£ βπ)π΅))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅)))β2)) + (i Β·
((((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π΅)))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π΅)))β2)))) / 4)) |
7 | 6 | fveq2d 6847 |
. 2
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (ββ(π΄ππ΅)) =
(ββ((((((normCVβπ)β(π΄( +π£ βπ)π΅))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅)))β2)) + (i Β·
((((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π΅)))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π΅)))β2)))) / 4))) |
8 | 1, 2, 3, 4, 5 | ipval2 29691 |
. . . 4
β’ ((π β NrmCVec β§ π΅ β π β§ π΄ β π) β (π΅ππ΄) = ((((((normCVβπ)β(π΅( +π£ βπ)π΄))β2) β
(((normCVβπ)β(π΅( +π£ βπ)(-1(
Β·π OLD βπ)π΄)))β2)) + (i Β·
((((normCVβπ)β(π΅( +π£ βπ)(i(
Β·π OLD βπ)π΄)))β2) β
(((normCVβπ)β(π΅( +π£ βπ)(-i(
Β·π OLD βπ)π΄)))β2)))) / 4)) |
9 | 8 | 3com23 1127 |
. . 3
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (π΅ππ΄) = ((((((normCVβπ)β(π΅( +π£ βπ)π΄))β2) β
(((normCVβπ)β(π΅( +π£ βπ)(-1(
Β·π OLD βπ)π΄)))β2)) + (i Β·
((((normCVβπ)β(π΅( +π£ βπ)(i(
Β·π OLD βπ)π΄)))β2) β
(((normCVβπ)β(π΅( +π£ βπ)(-i(
Β·π OLD βπ)π΄)))β2)))) / 4)) |
10 | 1, 2, 3, 4, 5 | ipval2lem3 29689 |
. . . . . . . 8
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (((normCVβπ)β(π΄( +π£ βπ)π΅))β2) β β) |
11 | 10 | recnd 11188 |
. . . . . . 7
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (((normCVβπ)β(π΄( +π£ βπ)π΅))β2) β β) |
12 | | neg1cn 12272 |
. . . . . . . 8
β’ -1 β
β |
13 | 1, 2, 3, 4, 5 | ipval2lem4 29690 |
. . . . . . . 8
β’ (((π β NrmCVec β§ π΄ β π β§ π΅ β π) β§ -1 β β) β
(((normCVβπ)β(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅)))β2) β β) |
14 | 12, 13 | mpan2 690 |
. . . . . . 7
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (((normCVβπ)β(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅)))β2) β β) |
15 | 11, 14 | subcld 11517 |
. . . . . 6
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β ((((normCVβπ)β(π΄( +π£ βπ)π΅))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅)))β2)) β
β) |
16 | | ax-icn 11115 |
. . . . . . 7
β’ i β
β |
17 | 1, 2, 3, 4, 5 | ipval2lem4 29690 |
. . . . . . . . 9
β’ (((π β NrmCVec β§ π΄ β π β§ π΅ β π) β§ i β β) β
(((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π΅)))β2) β β) |
18 | 16, 17 | mpan2 690 |
. . . . . . . 8
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π΅)))β2) β β) |
19 | | negicn 11407 |
. . . . . . . . 9
β’ -i β
β |
20 | 1, 2, 3, 4, 5 | ipval2lem4 29690 |
. . . . . . . . 9
β’ (((π β NrmCVec β§ π΄ β π β§ π΅ β π) β§ -i β β) β
(((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π΅)))β2) β β) |
21 | 19, 20 | mpan2 690 |
. . . . . . . 8
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π΅)))β2) β β) |
22 | 18, 21 | subcld 11517 |
. . . . . . 7
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β ((((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π΅)))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π΅)))β2)) β
β) |
23 | | mulcl 11140 |
. . . . . . 7
β’ ((i
β β β§ ((((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π΅)))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π΅)))β2)) β β) β (i
Β· ((((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π΅)))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π΅)))β2))) β
β) |
24 | 16, 22, 23 | sylancr 588 |
. . . . . 6
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (i Β·
((((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π΅)))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π΅)))β2))) β
β) |
25 | 15, 24 | addcld 11179 |
. . . . 5
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (((((normCVβπ)β(π΄( +π£ βπ)π΅))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅)))β2)) + (i Β·
((((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π΅)))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π΅)))β2)))) β
β) |
26 | | 4cn 12243 |
. . . . . 6
β’ 4 β
β |
27 | | 4ne0 12266 |
. . . . . 6
β’ 4 β
0 |
28 | | cjdiv 15055 |
. . . . . 6
β’
(((((((normCVβπ)β(π΄( +π£ βπ)π΅))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅)))β2)) + (i Β·
((((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π΅)))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π΅)))β2)))) β β β§ 4 β
β β§ 4 β 0) β
(ββ((((((normCVβπ)β(π΄( +π£ βπ)π΅))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅)))β2)) + (i Β·
((((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π΅)))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π΅)))β2)))) / 4)) =
((ββ(((((normCVβπ)β(π΄( +π£ βπ)π΅))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅)))β2)) + (i Β·
((((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π΅)))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π΅)))β2))))) /
(ββ4))) |
29 | 26, 27, 28 | mp3an23 1454 |
. . . . 5
β’
((((((normCVβπ)β(π΄( +π£ βπ)π΅))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅)))β2)) + (i Β·
((((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π΅)))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π΅)))β2)))) β β β
(ββ((((((normCVβπ)β(π΄( +π£ βπ)π΅))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅)))β2)) + (i Β·
((((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π΅)))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π΅)))β2)))) / 4)) =
((ββ(((((normCVβπ)β(π΄( +π£ βπ)π΅))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅)))β2)) + (i Β·
((((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π΅)))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π΅)))β2))))) /
(ββ4))) |
30 | 25, 29 | syl 17 |
. . . 4
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β
(ββ((((((normCVβπ)β(π΄( +π£ βπ)π΅))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅)))β2)) + (i Β·
((((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π΅)))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π΅)))β2)))) / 4)) =
((ββ(((((normCVβπ)β(π΄( +π£ βπ)π΅))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅)))β2)) + (i Β·
((((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π΅)))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π΅)))β2))))) /
(ββ4))) |
31 | | 4re 12242 |
. . . . . . 7
β’ 4 β
β |
32 | | cjre 15030 |
. . . . . . 7
β’ (4 β
β β (ββ4) = 4) |
33 | 31, 32 | ax-mp 5 |
. . . . . 6
β’
(ββ4) = 4 |
34 | 33 | oveq2i 7369 |
. . . . 5
β’
((ββ(((((normCVβπ)β(π΄( +π£ βπ)π΅))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅)))β2)) + (i Β·
((((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π΅)))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π΅)))β2))))) / (ββ4)) =
((ββ(((((normCVβπ)β(π΄( +π£ βπ)π΅))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅)))β2)) + (i Β·
((((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π΅)))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π΅)))β2))))) / 4) |
35 | 1, 2, 3, 4, 5 | ipval2lem2 29688 |
. . . . . . . . . 10
β’ (((π β NrmCVec β§ π΄ β π β§ π΅ β π) β§ -1 β β) β
(((normCVβπ)β(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅)))β2) β β) |
36 | 12, 35 | mpan2 690 |
. . . . . . . . 9
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (((normCVβπ)β(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅)))β2) β β) |
37 | 10, 36 | resubcld 11588 |
. . . . . . . 8
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β ((((normCVβπ)β(π΄( +π£ βπ)π΅))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅)))β2)) β
β) |
38 | 1, 2, 3, 4, 5 | ipval2lem2 29688 |
. . . . . . . . . 10
β’ (((π β NrmCVec β§ π΄ β π β§ π΅ β π) β§ i β β) β
(((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π΅)))β2) β β) |
39 | 16, 38 | mpan2 690 |
. . . . . . . . 9
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π΅)))β2) β β) |
40 | 1, 2, 3, 4, 5 | ipval2lem2 29688 |
. . . . . . . . . 10
β’ (((π β NrmCVec β§ π΄ β π β§ π΅ β π) β§ -i β β) β
(((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π΅)))β2) β β) |
41 | 19, 40 | mpan2 690 |
. . . . . . . . 9
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π΅)))β2) β β) |
42 | 39, 41 | resubcld 11588 |
. . . . . . . 8
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β ((((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π΅)))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π΅)))β2)) β
β) |
43 | | cjreim 15051 |
. . . . . . . 8
β’
((((((normCVβπ)β(π΄( +π£ βπ)π΅))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅)))β2)) β β β§
((((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π΅)))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π΅)))β2)) β β) β
(ββ(((((normCVβπ)β(π΄( +π£ βπ)π΅))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅)))β2)) + (i Β·
((((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π΅)))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π΅)))β2))))) =
(((((normCVβπ)β(π΄( +π£ βπ)π΅))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅)))β2)) β (i Β·
((((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π΅)))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π΅)))β2))))) |
44 | 37, 42, 43 | syl2anc 585 |
. . . . . . 7
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β
(ββ(((((normCVβπ)β(π΄( +π£ βπ)π΅))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅)))β2)) + (i Β·
((((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π΅)))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π΅)))β2))))) =
(((((normCVβπ)β(π΄( +π£ βπ)π΅))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅)))β2)) β (i Β·
((((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π΅)))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π΅)))β2))))) |
45 | | submul2 11600 |
. . . . . . . . 9
β’
((((((normCVβπ)β(π΄( +π£ βπ)π΅))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅)))β2)) β β β§ i β
β β§ ((((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π΅)))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π΅)))β2)) β β) β
(((((normCVβπ)β(π΄( +π£ βπ)π΅))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅)))β2)) β (i Β·
((((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π΅)))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π΅)))β2)))) =
(((((normCVβπ)β(π΄( +π£ βπ)π΅))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅)))β2)) + (i Β·
-((((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π΅)))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π΅)))β2))))) |
46 | 16, 45 | mp3an2 1450 |
. . . . . . . 8
β’
((((((normCVβπ)β(π΄( +π£ βπ)π΅))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅)))β2)) β β β§
((((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π΅)))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π΅)))β2)) β β) β
(((((normCVβπ)β(π΄( +π£ βπ)π΅))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅)))β2)) β (i Β·
((((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π΅)))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π΅)))β2)))) =
(((((normCVβπ)β(π΄( +π£ βπ)π΅))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅)))β2)) + (i Β·
-((((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π΅)))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π΅)))β2))))) |
47 | 15, 22, 46 | syl2anc 585 |
. . . . . . 7
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (((((normCVβπ)β(π΄( +π£ βπ)π΅))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅)))β2)) β (i Β·
((((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π΅)))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π΅)))β2)))) =
(((((normCVβπ)β(π΄( +π£ βπ)π΅))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅)))β2)) + (i Β·
-((((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π΅)))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π΅)))β2))))) |
48 | 1, 2 | nvcom 29605 |
. . . . . . . . . . 11
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (π΄( +π£ βπ)π΅) = (π΅( +π£ βπ)π΄)) |
49 | 48 | fveq2d 6847 |
. . . . . . . . . 10
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β ((normCVβπ)β(π΄( +π£ βπ)π΅)) = ((normCVβπ)β(π΅( +π£ βπ)π΄))) |
50 | 49 | oveq1d 7373 |
. . . . . . . . 9
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (((normCVβπ)β(π΄( +π£ βπ)π΅))β2) =
(((normCVβπ)β(π΅( +π£ βπ)π΄))β2)) |
51 | 1, 2, 3, 4 | nvdif 29650 |
. . . . . . . . . 10
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β ((normCVβπ)β(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅))) = ((normCVβπ)β(π΅( +π£ βπ)(-1(
Β·π OLD βπ)π΄)))) |
52 | 51 | oveq1d 7373 |
. . . . . . . . 9
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (((normCVβπ)β(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅)))β2) =
(((normCVβπ)β(π΅( +π£ βπ)(-1(
Β·π OLD βπ)π΄)))β2)) |
53 | 50, 52 | oveq12d 7376 |
. . . . . . . 8
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β ((((normCVβπ)β(π΄( +π£ βπ)π΅))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅)))β2)) =
((((normCVβπ)β(π΅( +π£ βπ)π΄))β2) β
(((normCVβπ)β(π΅( +π£ βπ)(-1(
Β·π OLD βπ)π΄)))β2))) |
54 | 18, 21 | negsubdi2d 11533 |
. . . . . . . . . 10
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β -((((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π΅)))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π΅)))β2)) =
((((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π΅)))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π΅)))β2))) |
55 | 1, 2, 3, 4 | nvpi 29651 |
. . . . . . . . . . . . . 14
β’ ((π β NrmCVec β§ π΅ β π β§ π΄ β π) β ((normCVβπ)β(π΅( +π£ βπ)(i(
Β·π OLD βπ)π΄))) = ((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π΅)))) |
56 | 55 | 3com23 1127 |
. . . . . . . . . . . . 13
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β ((normCVβπ)β(π΅( +π£ βπ)(i(
Β·π OLD βπ)π΄))) = ((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π΅)))) |
57 | 56 | eqcomd 2739 |
. . . . . . . . . . . 12
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β ((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π΅))) = ((normCVβπ)β(π΅( +π£ βπ)(i(
Β·π OLD βπ)π΄)))) |
58 | 57 | oveq1d 7373 |
. . . . . . . . . . 11
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π΅)))β2) =
(((normCVβπ)β(π΅( +π£ βπ)(i(
Β·π OLD βπ)π΄)))β2)) |
59 | 1, 2, 3, 4 | nvpi 29651 |
. . . . . . . . . . . 12
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β ((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π΅))) = ((normCVβπ)β(π΅( +π£ βπ)(-i(
Β·π OLD βπ)π΄)))) |
60 | 59 | oveq1d 7373 |
. . . . . . . . . . 11
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π΅)))β2) =
(((normCVβπ)β(π΅( +π£ βπ)(-i(
Β·π OLD βπ)π΄)))β2)) |
61 | 58, 60 | oveq12d 7376 |
. . . . . . . . . 10
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β ((((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π΅)))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π΅)))β2)) =
((((normCVβπ)β(π΅( +π£ βπ)(i(
Β·π OLD βπ)π΄)))β2) β
(((normCVβπ)β(π΅( +π£ βπ)(-i(
Β·π OLD βπ)π΄)))β2))) |
62 | 54, 61 | eqtrd 2773 |
. . . . . . . . 9
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β -((((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π΅)))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π΅)))β2)) =
((((normCVβπ)β(π΅( +π£ βπ)(i(
Β·π OLD βπ)π΄)))β2) β
(((normCVβπ)β(π΅( +π£ βπ)(-i(
Β·π OLD βπ)π΄)))β2))) |
63 | 62 | oveq2d 7374 |
. . . . . . . 8
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (i Β·
-((((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π΅)))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π΅)))β2))) = (i Β·
((((normCVβπ)β(π΅( +π£ βπ)(i(
Β·π OLD βπ)π΄)))β2) β
(((normCVβπ)β(π΅( +π£ βπ)(-i(
Β·π OLD βπ)π΄)))β2)))) |
64 | 53, 63 | oveq12d 7376 |
. . . . . . 7
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (((((normCVβπ)β(π΄( +π£ βπ)π΅))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅)))β2)) + (i Β·
-((((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π΅)))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π΅)))β2)))) =
(((((normCVβπ)β(π΅( +π£ βπ)π΄))β2) β
(((normCVβπ)β(π΅( +π£ βπ)(-1(
Β·π OLD βπ)π΄)))β2)) + (i Β·
((((normCVβπ)β(π΅( +π£ βπ)(i(
Β·π OLD βπ)π΄)))β2) β
(((normCVβπ)β(π΅( +π£ βπ)(-i(
Β·π OLD βπ)π΄)))β2))))) |
65 | 44, 47, 64 | 3eqtrd 2777 |
. . . . . 6
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β
(ββ(((((normCVβπ)β(π΄( +π£ βπ)π΅))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅)))β2)) + (i Β·
((((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π΅)))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π΅)))β2))))) =
(((((normCVβπ)β(π΅( +π£ βπ)π΄))β2) β
(((normCVβπ)β(π΅( +π£ βπ)(-1(
Β·π OLD βπ)π΄)))β2)) + (i Β·
((((normCVβπ)β(π΅( +π£ βπ)(i(
Β·π OLD βπ)π΄)))β2) β
(((normCVβπ)β(π΅( +π£ βπ)(-i(
Β·π OLD βπ)π΄)))β2))))) |
66 | 65 | oveq1d 7373 |
. . . . 5
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β
((ββ(((((normCVβπ)β(π΄( +π£ βπ)π΅))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅)))β2)) + (i Β·
((((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π΅)))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π΅)))β2))))) / 4) =
((((((normCVβπ)β(π΅( +π£ βπ)π΄))β2) β
(((normCVβπ)β(π΅( +π£ βπ)(-1(
Β·π OLD βπ)π΄)))β2)) + (i Β·
((((normCVβπ)β(π΅( +π£ βπ)(i(
Β·π OLD βπ)π΄)))β2) β
(((normCVβπ)β(π΅( +π£ βπ)(-i(
Β·π OLD βπ)π΄)))β2)))) / 4)) |
67 | 34, 66 | eqtrid 2785 |
. . . 4
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β
((ββ(((((normCVβπ)β(π΄( +π£ βπ)π΅))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅)))β2)) + (i Β·
((((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π΅)))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π΅)))β2))))) / (ββ4)) =
((((((normCVβπ)β(π΅( +π£ βπ)π΄))β2) β
(((normCVβπ)β(π΅( +π£ βπ)(-1(
Β·π OLD βπ)π΄)))β2)) + (i Β·
((((normCVβπ)β(π΅( +π£ βπ)(i(
Β·π OLD βπ)π΄)))β2) β
(((normCVβπ)β(π΅( +π£ βπ)(-i(
Β·π OLD βπ)π΄)))β2)))) / 4)) |
68 | 30, 67 | eqtrd 2773 |
. . 3
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β
(ββ((((((normCVβπ)β(π΄( +π£ βπ)π΅))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅)))β2)) + (i Β·
((((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π΅)))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π΅)))β2)))) / 4)) =
((((((normCVβπ)β(π΅( +π£ βπ)π΄))β2) β
(((normCVβπ)β(π΅( +π£ βπ)(-1(
Β·π OLD βπ)π΄)))β2)) + (i Β·
((((normCVβπ)β(π΅( +π£ βπ)(i(
Β·π OLD βπ)π΄)))β2) β
(((normCVβπ)β(π΅( +π£ βπ)(-i(
Β·π OLD βπ)π΄)))β2)))) / 4)) |
69 | 9, 68 | eqtr4d 2776 |
. 2
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (π΅ππ΄) =
(ββ((((((normCVβπ)β(π΄( +π£ βπ)π΅))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΅)))β2)) + (i Β·
((((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π΅)))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π΅)))β2)))) / 4))) |
70 | 7, 69 | eqtr4d 2776 |
1
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (ββ(π΄ππ΅)) = (π΅ππ΄)) |