Theorem ldual0v

Description: The zero vector of the dual of a vector space. (Contributed by NM, 24-Oct-2014)

	Ref	Expression
Hypotheses	ldualv0.v	$$⊢V={\mathrm{Base}}_W$$
	ldualv0.r	$$⊢R=\mathrm{Scalar}\left(W\right)$$
	ldualv0.z	$$⊢\underset{\dot{}}{0}=0_R$$
	ldualv0.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
	ldualv0.o	$$⊢O=0_D$$
	ldualv0.w	$$⊢\phi \to W\in \mathrm{LMod}$$
Assertion	ldual0v	$$⊢\phi \to O=V\times \left\{\underset{\dot{}}{0}\right\}$$

Proof

Step	Hyp	Ref	Expression
1		ldualv0.v	$$⊢V={\mathrm{Base}}_W$$
2		ldualv0.r	$$⊢R=\mathrm{Scalar}\left(W\right)$$
3		ldualv0.z	$$⊢\underset{\dot{}}{0}=0_R$$
4		ldualv0.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
5		ldualv0.o	$$⊢O=0_D$$
6		ldualv0.w	$$⊢\phi \to W\in \mathrm{LMod}$$
7		eqid	$$⊢\mathrm{LFnl}\left(W\right)=\mathrm{LFnl}\left(W\right)$$
8		eqid	$$⊢{+}_R={+}_R$$
9		eqid	$$⊢{+}_D={+}_D$$
10	2 3 1 7	lfl0f	$$⊢W\in \mathrm{LMod}\to V\times \left\{\underset{\dot{}}{0}\right\}\in \mathrm{LFnl}\left(W\right)$$
11	6 10	syl	$$⊢\phi \to V\times \left\{\underset{\dot{}}{0}\right\}\in \mathrm{LFnl}\left(W\right)$$
12	7 2 8 4 9 6 11 11	ldualvadd	$$⊢\phi \to \left(V\times \left\{\underset{\dot{}}{0}\right\}\right){+}_D\left(V\times \left\{\underset{\dot{}}{0}\right\}\right)=\left(V\times \left\{\underset{\dot{}}{0}\right\}\right){{+}_R}_f\left(V\times \left\{\underset{\dot{}}{0}\right\}\right)$$
13	1 2 8 3 7 6 11	lfladd0l	$$⊢\phi \to \left(V\times \left\{\underset{\dot{}}{0}\right\}\right){{+}_R}_f\left(V\times \left\{\underset{\dot{}}{0}\right\}\right)=V\times \left\{\underset{\dot{}}{0}\right\}$$
14	12 13	eqtrd	$$⊢\phi \to \left(V\times \left\{\underset{\dot{}}{0}\right\}\right){+}_D\left(V\times \left\{\underset{\dot{}}{0}\right\}\right)=V\times \left\{\underset{\dot{}}{0}\right\}$$
15	4 6	ldualgrp	$$⊢\phi \to D\in \mathrm{Grp}$$
16		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
17	7 4 16 6 11	ldualelvbase	$$⊢\phi \to V\times \left\{\underset{\dot{}}{0}\right\}\in {\mathrm{Base}}_D$$
18	16 9 5	grpid	$$⊢\left(D\in \mathrm{Grp}\wedge V\times \left\{\underset{\dot{}}{0}\right\}\in {\mathrm{Base}}_D\right)\to \left(\left(V\times \left\{\underset{\dot{}}{0}\right\}\right){+}_D\left(V\times \left\{\underset{\dot{}}{0}\right\}\right)=V\times \left\{\underset{\dot{}}{0}\right\}\leftrightarrow O=V\times \left\{\underset{\dot{}}{0}\right\}\right)$$
19	15 17 18	syl2anc	$$⊢\phi \to \left(\left(V\times \left\{\underset{\dot{}}{0}\right\}\right){+}_D\left(V\times \left\{\underset{\dot{}}{0}\right\}\right)=V\times \left\{\underset{\dot{}}{0}\right\}\leftrightarrow O=V\times \left\{\underset{\dot{}}{0}\right\}\right)$$
20	14 19	mpbid	$$⊢\phi \to O=V\times \left\{\underset{\dot{}}{0}\right\}$$