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=\mathrm{Scalar}\left(W\right)$$
	ldual0.z	$$⊢\underset{\dot{}}{0}=0_R$$
	ldual0.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
	ldual0.s	$$⊢S=\mathrm{Scalar}\left(D\right)$$
	ldual0.o	$$⊢O=0_S$$
	ldual0.w	$$⊢\phi \to W\in \mathrm{LMod}$$
Assertion	ldual0	$$⊢\phi \to O=\underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		ldual0.r	$$⊢R=\mathrm{Scalar}\left(W\right)$$
2		ldual0.z	$$⊢\underset{\dot{}}{0}=0_R$$
3		ldual0.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
4		ldual0.s	$$⊢S=\mathrm{Scalar}\left(D\right)$$
5		ldual0.o	$$⊢O=0_S$$
6		ldual0.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 0_S=0_{{opp}_r\left(R\right)}$$
10	7 2	oppr0	$$⊢\underset{\dot{}}{0}=0_{{opp}_r\left(R\right)}$$
11	9 5 10	3eqtr4g	$$⊢\phi \to O=\underset{\dot{}}{0}$$