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 )