Step |
Hyp |
Ref |
Expression |
1 |
|
dip0r.1 |
|- X = ( BaseSet ` U ) |
2 |
|
dip0r.5 |
|- Z = ( 0vec ` U ) |
3 |
|
dip0r.7 |
|- P = ( .iOLD ` U ) |
4 |
1 2
|
nvzcl |
|- ( U e. NrmCVec -> Z e. X ) |
5 |
4
|
adantr |
|- ( ( U e. NrmCVec /\ A e. X ) -> Z e. X ) |
6 |
|
eqid |
|- ( +v ` U ) = ( +v ` U ) |
7 |
|
eqid |
|- ( .sOLD ` U ) = ( .sOLD ` U ) |
8 |
|
eqid |
|- ( normCV ` U ) = ( normCV ` U ) |
9 |
1 6 7 8 3
|
ipval2 |
|- ( ( U e. NrmCVec /\ A e. X /\ Z e. X ) -> ( A P Z ) = ( ( ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) Z ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) Z ) ) ) ^ 2 ) ) + ( _i x. ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) Z ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) Z ) ) ) ^ 2 ) ) ) ) / 4 ) ) |
10 |
5 9
|
mpd3an3 |
|- ( ( U e. NrmCVec /\ A e. X ) -> ( A P Z ) = ( ( ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) Z ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) Z ) ) ) ^ 2 ) ) + ( _i x. ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) Z ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) Z ) ) ) ^ 2 ) ) ) ) / 4 ) ) |
11 |
|
neg1cn |
|- -u 1 e. CC |
12 |
7 2
|
nvsz |
|- ( ( U e. NrmCVec /\ -u 1 e. CC ) -> ( -u 1 ( .sOLD ` U ) Z ) = Z ) |
13 |
11 12
|
mpan2 |
|- ( U e. NrmCVec -> ( -u 1 ( .sOLD ` U ) Z ) = Z ) |
14 |
13
|
adantr |
|- ( ( U e. NrmCVec /\ A e. X ) -> ( -u 1 ( .sOLD ` U ) Z ) = Z ) |
15 |
14
|
oveq2d |
|- ( ( U e. NrmCVec /\ A e. X ) -> ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) Z ) ) = ( A ( +v ` U ) Z ) ) |
16 |
15
|
fveq2d |
|- ( ( U e. NrmCVec /\ A e. X ) -> ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) Z ) ) ) = ( ( normCV ` U ) ` ( A ( +v ` U ) Z ) ) ) |
17 |
16
|
oveq1d |
|- ( ( U e. NrmCVec /\ A e. X ) -> ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) Z ) ) ) ^ 2 ) = ( ( ( normCV ` U ) ` ( A ( +v ` U ) Z ) ) ^ 2 ) ) |
18 |
17
|
oveq2d |
|- ( ( U e. NrmCVec /\ A e. X ) -> ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) Z ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) Z ) ) ) ^ 2 ) ) = ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) Z ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) Z ) ) ^ 2 ) ) ) |
19 |
1 6 7 8 3
|
ipval2lem3 |
|- ( ( U e. NrmCVec /\ A e. X /\ Z e. X ) -> ( ( ( normCV ` U ) ` ( A ( +v ` U ) Z ) ) ^ 2 ) e. RR ) |
20 |
5 19
|
mpd3an3 |
|- ( ( U e. NrmCVec /\ A e. X ) -> ( ( ( normCV ` U ) ` ( A ( +v ` U ) Z ) ) ^ 2 ) e. RR ) |
21 |
20
|
recnd |
|- ( ( U e. NrmCVec /\ A e. X ) -> ( ( ( normCV ` U ) ` ( A ( +v ` U ) Z ) ) ^ 2 ) e. CC ) |
22 |
21
|
subidd |
|- ( ( U e. NrmCVec /\ A e. X ) -> ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) Z ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) Z ) ) ^ 2 ) ) = 0 ) |
23 |
18 22
|
eqtrd |
|- ( ( U e. NrmCVec /\ A e. X ) -> ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) Z ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) Z ) ) ) ^ 2 ) ) = 0 ) |
24 |
|
negicn |
|- -u _i e. CC |
25 |
7 2
|
nvsz |
|- ( ( U e. NrmCVec /\ -u _i e. CC ) -> ( -u _i ( .sOLD ` U ) Z ) = Z ) |
26 |
24 25
|
mpan2 |
|- ( U e. NrmCVec -> ( -u _i ( .sOLD ` U ) Z ) = Z ) |
27 |
|
ax-icn |
|- _i e. CC |
28 |
7 2
|
nvsz |
|- ( ( U e. NrmCVec /\ _i e. CC ) -> ( _i ( .sOLD ` U ) Z ) = Z ) |
29 |
27 28
|
mpan2 |
|- ( U e. NrmCVec -> ( _i ( .sOLD ` U ) Z ) = Z ) |
30 |
26 29
|
eqtr4d |
|- ( U e. NrmCVec -> ( -u _i ( .sOLD ` U ) Z ) = ( _i ( .sOLD ` U ) Z ) ) |
31 |
30
|
adantr |
|- ( ( U e. NrmCVec /\ A e. X ) -> ( -u _i ( .sOLD ` U ) Z ) = ( _i ( .sOLD ` U ) Z ) ) |
32 |
31
|
oveq2d |
|- ( ( U e. NrmCVec /\ A e. X ) -> ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) Z ) ) = ( A ( +v ` U ) ( _i ( .sOLD ` U ) Z ) ) ) |
33 |
32
|
fveq2d |
|- ( ( U e. NrmCVec /\ A e. X ) -> ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) Z ) ) ) = ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) Z ) ) ) ) |
34 |
33
|
oveq1d |
|- ( ( U e. NrmCVec /\ A e. X ) -> ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) Z ) ) ) ^ 2 ) = ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) Z ) ) ) ^ 2 ) ) |
35 |
34
|
oveq2d |
|- ( ( U e. NrmCVec /\ A e. X ) -> ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) Z ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) Z ) ) ) ^ 2 ) ) = ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) Z ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) Z ) ) ) ^ 2 ) ) ) |
36 |
1 6 7 8 3
|
ipval2lem4 |
|- ( ( ( U e. NrmCVec /\ A e. X /\ Z e. X ) /\ _i e. CC ) -> ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) Z ) ) ) ^ 2 ) e. CC ) |
37 |
27 36
|
mpan2 |
|- ( ( U e. NrmCVec /\ A e. X /\ Z e. X ) -> ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) Z ) ) ) ^ 2 ) e. CC ) |
38 |
5 37
|
mpd3an3 |
|- ( ( U e. NrmCVec /\ A e. X ) -> ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) Z ) ) ) ^ 2 ) e. CC ) |
39 |
38
|
subidd |
|- ( ( U e. NrmCVec /\ A e. X ) -> ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) Z ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) Z ) ) ) ^ 2 ) ) = 0 ) |
40 |
35 39
|
eqtrd |
|- ( ( U e. NrmCVec /\ A e. X ) -> ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) Z ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) Z ) ) ) ^ 2 ) ) = 0 ) |
41 |
40
|
oveq2d |
|- ( ( U e. NrmCVec /\ A e. X ) -> ( _i x. ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) Z ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) Z ) ) ) ^ 2 ) ) ) = ( _i x. 0 ) ) |
42 |
23 41
|
oveq12d |
|- ( ( U e. NrmCVec /\ A e. X ) -> ( ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) Z ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) Z ) ) ) ^ 2 ) ) + ( _i x. ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) Z ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) Z ) ) ) ^ 2 ) ) ) ) = ( 0 + ( _i x. 0 ) ) ) |
43 |
|
it0e0 |
|- ( _i x. 0 ) = 0 |
44 |
43
|
oveq2i |
|- ( 0 + ( _i x. 0 ) ) = ( 0 + 0 ) |
45 |
|
00id |
|- ( 0 + 0 ) = 0 |
46 |
44 45
|
eqtri |
|- ( 0 + ( _i x. 0 ) ) = 0 |
47 |
42 46
|
eqtrdi |
|- ( ( U e. NrmCVec /\ A e. X ) -> ( ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) Z ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) Z ) ) ) ^ 2 ) ) + ( _i x. ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) Z ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) Z ) ) ) ^ 2 ) ) ) ) = 0 ) |
48 |
47
|
oveq1d |
|- ( ( U e. NrmCVec /\ A e. X ) -> ( ( ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) Z ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) Z ) ) ) ^ 2 ) ) + ( _i x. ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) Z ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) Z ) ) ) ^ 2 ) ) ) ) / 4 ) = ( 0 / 4 ) ) |
49 |
|
4cn |
|- 4 e. CC |
50 |
|
4ne0 |
|- 4 =/= 0 |
51 |
49 50
|
div0i |
|- ( 0 / 4 ) = 0 |
52 |
48 51
|
eqtrdi |
|- ( ( U e. NrmCVec /\ A e. X ) -> ( ( ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) Z ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) Z ) ) ) ^ 2 ) ) + ( _i x. ( ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( _i ( .sOLD ` U ) Z ) ) ) ^ 2 ) - ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( -u _i ( .sOLD ` U ) Z ) ) ) ^ 2 ) ) ) ) / 4 ) = 0 ) |
53 |
10 52
|
eqtrd |
|- ( ( U e. NrmCVec /\ A e. X ) -> ( A P Z ) = 0 ) |