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 )