Theorem ldual1

Description: The unit scalar of the dual of a vector space. (Contributed by NM, 26-Feb-2015)

	Ref	Expression
Hypotheses	ldual1.r	|- R = ( Scalar ` W )
	ldual1.u	|- .1. = ( 1r ` R )
	ldual1.d	|- D = ( LDual ` W )
	ldual1.s	|- S = ( Scalar ` D )
	ldual1.i	|- I = ( 1r ` S )
	ldual1.w	|- ( ph -> W e. LMod )
Assertion	ldual1	|- ( ph -> I = .1. )

Proof

Step	Hyp	Ref	Expression
1		ldual1.r	|- R = ( Scalar ` W )
2		ldual1.u	|- .1. = ( 1r ` R )
3		ldual1.d	|- D = ( LDual ` W )
4		ldual1.s	|- S = ( Scalar ` D )
5		ldual1.i	|- I = ( 1r ` S )
6		ldual1.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 -> ( 1r ` S ) = ( 1r ` ( oppR ` R ) ) )
10	7 2	oppr1	|- .1. = ( 1r ` ( oppR ` R ) )
11	9 5 10	3eqtr4g	|- ( ph -> I = .1. )