Theorem lkr0f2

Description: The kernel of the zero functional is the set of all vectors. (Contributed by NM, 4-Feb-2015)

	Ref	Expression
Hypotheses	lkr0f2.v	$$⊢V={\mathrm{Base}}_W$$
	lkr0f2.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
	lkr0f2.k	$$⊢K=\mathrm{LKer}\left(W\right)$$
	lkr0f2.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
	lkr0f2.o	$$⊢\underset{\dot{}}{0}=0_D$$
	lkr0f2.w	$$⊢\phi \to W\in \mathrm{LMod}$$
	lkr0f2.g	$$⊢\phi \to G\in F$$
Assertion	lkr0f2	$$⊢\phi \to \left(K\left(G\right)=V\leftrightarrow G=\underset{\dot{}}{0}\right)$$

Proof

Step	Hyp	Ref	Expression
1		lkr0f2.v	$$⊢V={\mathrm{Base}}_W$$
2		lkr0f2.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
3		lkr0f2.k	$$⊢K=\mathrm{LKer}\left(W\right)$$
4		lkr0f2.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
5		lkr0f2.o	$$⊢\underset{\dot{}}{0}=0_D$$
6		lkr0f2.w	$$⊢\phi \to W\in \mathrm{LMod}$$
7		lkr0f2.g	$$⊢\phi \to G\in F$$
8		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
9		eqid	$$⊢0_{\mathrm{Scalar}\left(W\right)}=0_{\mathrm{Scalar}\left(W\right)}$$
10	8 9 1 2 3	lkr0f	$$⊢\left(W\in \mathrm{LMod}\wedge G\in F\right)\to \left(K\left(G\right)=V\leftrightarrow G=V\times \left\{0_{\mathrm{Scalar}\left(W\right)}\right\}\right)$$
11	6 7 10	syl2anc	$$⊢\phi \to \left(K\left(G\right)=V\leftrightarrow G=V\times \left\{0_{\mathrm{Scalar}\left(W\right)}\right\}\right)$$
12	1 8 9 4 5 6	ldual0v	$$⊢\phi \to \underset{\dot{}}{0}=V\times \left\{0_{\mathrm{Scalar}\left(W\right)}\right\}$$
13	12	eqeq2d	$$⊢\phi \to \left(G=\underset{\dot{}}{0}\leftrightarrow G=V\times \left\{0_{\mathrm{Scalar}\left(W\right)}\right\}\right)$$
14	11 13	bitr4d	$$⊢\phi \to \left(K\left(G\right)=V\leftrightarrow G=\underset{\dot{}}{0}\right)$$