Step | Hyp | Ref
| Expression |
1 | | dip0r.1 |
. . . . 5
β’ π = (BaseSetβπ) |
2 | | dip0r.5 |
. . . . 5
β’ π = (0vecβπ) |
3 | 1, 2 | nvzcl 29887 |
. . . 4
β’ (π β NrmCVec β π β π) |
4 | 3 | adantr 482 |
. . 3
β’ ((π β NrmCVec β§ π΄ β π) β π β π) |
5 | | eqid 2733 |
. . . 4
β’ (
+π£ βπ) = ( +π£ βπ) |
6 | | eqid 2733 |
. . . 4
β’ (
Β·π OLD βπ) = ( Β·π OLD
βπ) |
7 | | eqid 2733 |
. . . 4
β’
(normCVβπ) = (normCVβπ) |
8 | | dip0r.7 |
. . . 4
β’ π =
(Β·πOLDβπ) |
9 | 1, 5, 6, 7, 8 | ipval2 29960 |
. . 3
β’ ((π β NrmCVec β§ π΄ β π β§ π β π) β (π΄ππ) = ((((((normCVβπ)β(π΄( +π£ βπ)π))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π)))β2)) + (i Β·
((((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π)))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π)))β2)))) / 4)) |
10 | 4, 9 | mpd3an3 1463 |
. 2
β’ ((π β NrmCVec β§ π΄ β π) β (π΄ππ) = ((((((normCVβπ)β(π΄( +π£ βπ)π))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π)))β2)) + (i Β·
((((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π)))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π)))β2)))) / 4)) |
11 | | neg1cn 12326 |
. . . . . . . . . . . . 13
β’ -1 β
β |
12 | 6, 2 | nvsz 29891 |
. . . . . . . . . . . . 13
β’ ((π β NrmCVec β§ -1 β
β) β (-1( Β·π OLD βπ)π) = π) |
13 | 11, 12 | mpan2 690 |
. . . . . . . . . . . 12
β’ (π β NrmCVec β (-1(
Β·π OLD βπ)π) = π) |
14 | 13 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β NrmCVec β§ π΄ β π) β (-1(
Β·π OLD βπ)π) = π) |
15 | 14 | oveq2d 7425 |
. . . . . . . . . 10
β’ ((π β NrmCVec β§ π΄ β π) β (π΄( +π£ βπ)(-1(
Β·π OLD βπ)π)) = (π΄( +π£ βπ)π)) |
16 | 15 | fveq2d 6896 |
. . . . . . . . 9
β’ ((π β NrmCVec β§ π΄ β π) β ((normCVβπ)β(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π))) = ((normCVβπ)β(π΄( +π£ βπ)π))) |
17 | 16 | oveq1d 7424 |
. . . . . . . 8
β’ ((π β NrmCVec β§ π΄ β π) β (((normCVβπ)β(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π)))β2) =
(((normCVβπ)β(π΄( +π£ βπ)π))β2)) |
18 | 17 | oveq2d 7425 |
. . . . . . 7
β’ ((π β NrmCVec β§ π΄ β π) β ((((normCVβπ)β(π΄( +π£ βπ)π))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π)))β2)) =
((((normCVβπ)β(π΄( +π£ βπ)π))β2) β
(((normCVβπ)β(π΄( +π£ βπ)π))β2))) |
19 | 1, 5, 6, 7, 8 | ipval2lem3 29958 |
. . . . . . . . . 10
β’ ((π β NrmCVec β§ π΄ β π β§ π β π) β (((normCVβπ)β(π΄( +π£ βπ)π))β2) β β) |
20 | 4, 19 | mpd3an3 1463 |
. . . . . . . . 9
β’ ((π β NrmCVec β§ π΄ β π) β (((normCVβπ)β(π΄( +π£ βπ)π))β2) β β) |
21 | 20 | recnd 11242 |
. . . . . . . 8
β’ ((π β NrmCVec β§ π΄ β π) β (((normCVβπ)β(π΄( +π£ βπ)π))β2) β β) |
22 | 21 | subidd 11559 |
. . . . . . 7
β’ ((π β NrmCVec β§ π΄ β π) β ((((normCVβπ)β(π΄( +π£ βπ)π))β2) β
(((normCVβπ)β(π΄( +π£ βπ)π))β2)) = 0) |
23 | 18, 22 | eqtrd 2773 |
. . . . . 6
β’ ((π β NrmCVec β§ π΄ β π) β ((((normCVβπ)β(π΄( +π£ βπ)π))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π)))β2)) = 0) |
24 | | negicn 11461 |
. . . . . . . . . . . . . . 15
β’ -i β
β |
25 | 6, 2 | nvsz 29891 |
. . . . . . . . . . . . . . 15
β’ ((π β NrmCVec β§ -i β
β) β (-i( Β·π OLD βπ)π) = π) |
26 | 24, 25 | mpan2 690 |
. . . . . . . . . . . . . 14
β’ (π β NrmCVec β (-i(
Β·π OLD βπ)π) = π) |
27 | | ax-icn 11169 |
. . . . . . . . . . . . . . 15
β’ i β
β |
28 | 6, 2 | nvsz 29891 |
. . . . . . . . . . . . . . 15
β’ ((π β NrmCVec β§ i β
β) β (i( Β·π OLD βπ)π) = π) |
29 | 27, 28 | mpan2 690 |
. . . . . . . . . . . . . 14
β’ (π β NrmCVec β (i(
Β·π OLD βπ)π) = π) |
30 | 26, 29 | eqtr4d 2776 |
. . . . . . . . . . . . 13
β’ (π β NrmCVec β (-i(
Β·π OLD βπ)π) = (i(
Β·π OLD βπ)π)) |
31 | 30 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β NrmCVec β§ π΄ β π) β (-i(
Β·π OLD βπ)π) = (i(
Β·π OLD βπ)π)) |
32 | 31 | oveq2d 7425 |
. . . . . . . . . . 11
β’ ((π β NrmCVec β§ π΄ β π) β (π΄( +π£ βπ)(-i(
Β·π OLD βπ)π)) = (π΄( +π£ βπ)(i(
Β·π OLD βπ)π))) |
33 | 32 | fveq2d 6896 |
. . . . . . . . . 10
β’ ((π β NrmCVec β§ π΄ β π) β ((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π))) = ((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π)))) |
34 | 33 | oveq1d 7424 |
. . . . . . . . 9
β’ ((π β NrmCVec β§ π΄ β π) β (((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π)))β2) =
(((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π)))β2)) |
35 | 34 | oveq2d 7425 |
. . . . . . . 8
β’ ((π β NrmCVec β§ π΄ β π) β ((((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π)))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π)))β2)) =
((((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π)))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π)))β2))) |
36 | 1, 5, 6, 7, 8 | ipval2lem4 29959 |
. . . . . . . . . . 11
β’ (((π β NrmCVec β§ π΄ β π β§ π β π) β§ i β β) β
(((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π)))β2) β β) |
37 | 27, 36 | mpan2 690 |
. . . . . . . . . 10
β’ ((π β NrmCVec β§ π΄ β π β§ π β π) β (((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π)))β2) β β) |
38 | 4, 37 | mpd3an3 1463 |
. . . . . . . . 9
β’ ((π β NrmCVec β§ π΄ β π) β (((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π)))β2) β β) |
39 | 38 | subidd 11559 |
. . . . . . . 8
β’ ((π β NrmCVec β§ π΄ β π) β ((((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π)))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π)))β2)) = 0) |
40 | 35, 39 | eqtrd 2773 |
. . . . . . 7
β’ ((π β NrmCVec β§ π΄ β π) β ((((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π)))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π)))β2)) = 0) |
41 | 40 | oveq2d 7425 |
. . . . . 6
β’ ((π β NrmCVec β§ π΄ β π) β (i Β·
((((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π)))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π)))β2))) = (i Β·
0)) |
42 | 23, 41 | oveq12d 7427 |
. . . . 5
β’ ((π β NrmCVec β§ π΄ β π) β (((((normCVβπ)β(π΄( +π£ βπ)π))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π)))β2)) + (i Β·
((((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π)))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π)))β2)))) = (0 + (i Β·
0))) |
43 | | it0e0 12434 |
. . . . . . 7
β’ (i
Β· 0) = 0 |
44 | 43 | oveq2i 7420 |
. . . . . 6
β’ (0 + (i
Β· 0)) = (0 + 0) |
45 | | 00id 11389 |
. . . . . 6
β’ (0 + 0) =
0 |
46 | 44, 45 | eqtri 2761 |
. . . . 5
β’ (0 + (i
Β· 0)) = 0 |
47 | 42, 46 | eqtrdi 2789 |
. . . 4
β’ ((π β NrmCVec β§ π΄ β π) β (((((normCVβπ)β(π΄( +π£ βπ)π))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π)))β2)) + (i Β·
((((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π)))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π)))β2)))) = 0) |
48 | 47 | oveq1d 7424 |
. . 3
β’ ((π β NrmCVec β§ π΄ β π) β ((((((normCVβπ)β(π΄( +π£ βπ)π))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π)))β2)) + (i Β·
((((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π)))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π)))β2)))) / 4) = (0 /
4)) |
49 | | 4cn 12297 |
. . . 4
β’ 4 β
β |
50 | | 4ne0 12320 |
. . . 4
β’ 4 β
0 |
51 | 49, 50 | div0i 11948 |
. . 3
β’ (0 / 4) =
0 |
52 | 48, 51 | eqtrdi 2789 |
. 2
β’ ((π β NrmCVec β§ π΄ β π) β ((((((normCVβπ)β(π΄( +π£ βπ)π))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π)))β2)) + (i Β·
((((normCVβπ)β(π΄( +π£ βπ)(i(
Β·π OLD βπ)π)))β2) β
(((normCVβπ)β(π΄( +π£ βπ)(-i(
Β·π OLD βπ)π)))β2)))) / 4) = 0) |
53 | 10, 52 | eqtrd 2773 |
1
β’ ((π β NrmCVec β§ π΄ β π) β (π΄ππ) = 0) |