Theorem ldualsbase

Description: Base set of scalar ring for the dual of a vector space. (Contributed by NM, 24-Oct-2014)

	Ref	Expression
Hypotheses	ldualsbase.f	|- F = ( Scalar ` W )
	ldualsbase.l	|- L = ( Base ` F )
	ldualsbase.d	|- D = ( LDual ` W )
	ldualsbase.r	|- R = ( Scalar ` D )
	ldualsbase.k	|- K = ( Base ` R )
	ldualsbase.w	|- ( ph -> W e. V )
Assertion	ldualsbase	|- ( ph -> K = L )

Proof

Step	Hyp	Ref	Expression
1		ldualsbase.f	|- F = ( Scalar ` W )
2		ldualsbase.l	|- L = ( Base ` F )
3		ldualsbase.d	|- D = ( LDual ` W )
4		ldualsbase.r	|- R = ( Scalar ` D )
5		ldualsbase.k	|- K = ( Base ` R )
6		ldualsbase.w	|- ( ph -> W e. V )
7		eqid	|- ( oppR ` F ) = ( oppR ` F )
8	1 7 3 4 6	ldualsca	|- ( ph -> R = ( oppR ` F ) )
9	8	fveq2d	|- ( ph -> ( Base ` R ) = ( Base ` ( oppR ` F ) ) )
10	7 2	opprbas	|- L = ( Base ` ( oppR ` F ) )
11	9 5 10	3eqtr4g	|- ( ph -> K = L )