Theorem ldual0

Description: The zero scalar of the dual of a vector space. (Contributed by NM, 28-Dec-2014)

	Ref	Expression
Hypotheses	ldual0.r	|- R = ( Scalar ` W )
	ldual0.z	|- .0. = ( 0g ` R )
	ldual0.d	|- D = ( LDual ` W )
	ldual0.s	|- S = ( Scalar ` D )
	ldual0.o	|- O = ( 0g ` S )
	ldual0.w	|- ( ph -> W e. LMod )
Assertion	ldual0	|- ( ph -> O = .0. )

Proof

Step	Hyp	Ref	Expression
1		ldual0.r	|- R = ( Scalar ` W )
2		ldual0.z	|- .0. = ( 0g ` R )
3		ldual0.d	|- D = ( LDual ` W )
4		ldual0.s	|- S = ( Scalar ` D )
5		ldual0.o	|- O = ( 0g ` S )
6		ldual0.w	|- ( ph -> W e. LMod )
7		eqid	|- ( oppR ` R ) = ( oppR ` R )
8	1 7 3 4 6	ldualsca	|- ( ph -> S = ( oppR ` R ) )
9	8	fveq2d	|- ( ph -> ( 0g ` S ) = ( 0g ` ( oppR ` R ) ) )
10	7 2	oppr0	|- .0. = ( 0g ` ( oppR ` R ) )
11	9 5 10	3eqtr4g	|- ( ph -> O = .0. )