This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dip0l

Description: Inner product with a zero first argument. Part of proof of Theorem 6.44 of Ponnusamy p. 361. (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 dip0l 
|- ( ( U e. NrmCVec /\ A e. X ) -> ( Z P A ) = 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 1 3 dipcj 
 |-  ( ( U e. NrmCVec /\ A e. X /\ Z e. X ) -> ( * ` ( A P Z ) ) = ( Z P A ) )
7 5 6 mpd3an3 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( * ` ( A P Z ) ) = ( Z P A ) )
8 1 2 3 dip0r 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( A P Z ) = 0 )
9 8 fveq2d 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( * ` ( A P Z ) ) = ( * ` 0 ) )
10 cj0 
 |-  ( * ` 0 ) = 0
11 9 10 eqtrdi 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( * ` ( A P Z ) ) = 0 )
12 7 11 eqtr3d 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( Z P A ) = 0 )