Metamath Proof Explorer

Theorem dip0r

Description: Inner product with a zero second argument. (Contributed by NM, 5-Feb-2007) (New usage is discouraged.)

Ref Expression
Hypotheses dip0r.1 
|- X = ( BaseSet ` U )
dip0r.5 
|- Z = ( 0vec ` U )
dip0r.7 
|- P = ( .iOLD ` U )
Assertion dip0r 
|- ( ( U e. NrmCVec /\ A e. X ) -> ( A P Z ) = 0 )

Proof

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 )