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=\mathrm{Scalar}\left(W\right)$$
	ldualsbase.l	$$⊢L={\mathrm{Base}}_F$$
	ldualsbase.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
	ldualsbase.r	$$⊢R=\mathrm{Scalar}\left(D\right)$$
	ldualsbase.k	$$⊢K={\mathrm{Base}}_R$$
	ldualsbase.w	$$⊢\phi \to W\in V$$
Assertion	ldualsbase	$$⊢\phi \to K=L$$

Proof

Step	Hyp	Ref	Expression
1		ldualsbase.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
2		ldualsbase.l	$$⊢L={\mathrm{Base}}_F$$
3		ldualsbase.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
4		ldualsbase.r	$$⊢R=\mathrm{Scalar}\left(D\right)$$
5		ldualsbase.k	$$⊢K={\mathrm{Base}}_R$$
6		ldualsbase.w	$$⊢\phi \to W\in V$$
7		eqid	$$⊢{opp}_r\left(F\right)={opp}_r\left(F\right)$$
8	1 7 3 4 6	ldualsca	$$⊢\phi \to R={opp}_r\left(F\right)$$
9	8	fveq2d	$$⊢\phi \to {\mathrm{Base}}_R={\mathrm{Base}}_{{opp}_r\left(F\right)}$$
10	7 2	opprbas	$$⊢L={\mathrm{Base}}_{{opp}_r\left(F\right)}$$
11	9 5 10	3eqtr4g	$$⊢\phi \to K=L$$