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=\mathrm{Scalar}\left(W\right)$$
	ldual1.u	$$⊢\underset{\dot{}}{1}=1_R$$
	ldual1.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
	ldual1.s	$$⊢S=\mathrm{Scalar}\left(D\right)$$
	ldual1.i	$$⊢I=1_S$$
	ldual1.w	$$⊢\phi \to W\in \mathrm{LMod}$$
Assertion	ldual1	$$⊢\phi \to I=\underset{\dot{}}{1}$$

Proof

Step	Hyp	Ref	Expression
1		ldual1.r	$$⊢R=\mathrm{Scalar}\left(W\right)$$
2		ldual1.u	$$⊢\underset{\dot{}}{1}=1_R$$
3		ldual1.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
4		ldual1.s	$$⊢S=\mathrm{Scalar}\left(D\right)$$
5		ldual1.i	$$⊢I=1_S$$
6		ldual1.w	$$⊢\phi \to W\in \mathrm{LMod}$$
7		eqid	$$⊢{opp}_r\left(R\right)={opp}_r\left(R\right)$$
8	1 7 3 4 6	ldualsca	$$⊢\phi \to S={opp}_r\left(R\right)$$
9	8	fveq2d	$$⊢\phi \to 1_S=1_{{opp}_r\left(R\right)}$$
10	7 2	oppr1	$$⊢\underset{\dot{}}{1}=1_{{opp}_r\left(R\right)}$$
11	9 5 10	3eqtr4g	$$⊢\phi \to I=\underset{\dot{}}{1}$$