Theorem dochsnkrlem1

Description: Lemma for dochsnkr . (Contributed by NM, 1-Jan-2015)

	Ref	Expression
Hypotheses	dochsnkr.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dochsnkr.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
	dochsnkr.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	dochsnkr.v	$$⊢V={\mathrm{Base}}_U$$
	dochsnkr.z	$$⊢\underset{\dot{}}{0}=0_U$$
	dochsnkr.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
	dochsnkr.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
	dochsnkr.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	dochsnkr.g	$$⊢\phi \to G\in F$$
	dochsnkr.x	$$⊢\phi \to X\in \left(\underset{\dot{}}{\perp }\left(L\left(G\right)\right)\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
Assertion	dochsnkrlem1	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(G\right)\right)\right)\ne V$$

Proof

Step	Hyp	Ref	Expression
1		dochsnkr.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		dochsnkr.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
3		dochsnkr.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
4		dochsnkr.v	$$⊢V={\mathrm{Base}}_U$$
5		dochsnkr.z	$$⊢\underset{\dot{}}{0}=0_U$$
6		dochsnkr.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
7		dochsnkr.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
8		dochsnkr.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
9		dochsnkr.g	$$⊢\phi \to G\in F$$
10		dochsnkr.x	$$⊢\phi \to X\in \left(\underset{\dot{}}{\perp }\left(L\left(G\right)\right)\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
11		eldif	$$⊢X\in \left(\underset{\dot{}}{\perp }\left(L\left(G\right)\right)\setminus \left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow \left(X\in \underset{\dot{}}{\perp }\left(L\left(G\right)\right)\wedge \neg X\in \left\{\underset{\dot{}}{0}\right\}\right)$$
12		nelne1	$$⊢\left(X\in \underset{\dot{}}{\perp }\left(L\left(G\right)\right)\wedge \neg X\in \left\{\underset{\dot{}}{0}\right\}\right)\to \underset{\dot{}}{\perp }\left(L\left(G\right)\right)\ne \left\{\underset{\dot{}}{0}\right\}$$
13	11 12	sylbi	$$⊢X\in \left(\underset{\dot{}}{\perp }\left(L\left(G\right)\right)\setminus \left\{\underset{\dot{}}{0}\right\}\right)\to \underset{\dot{}}{\perp }\left(L\left(G\right)\right)\ne \left\{\underset{\dot{}}{0}\right\}$$
14	10 13	syl	$$⊢\phi \to \underset{\dot{}}{\perp }\left(L\left(G\right)\right)\ne \left\{\underset{\dot{}}{0}\right\}$$
15	1 3 8	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
16	4 6 7 15 9	lkrssv	$$⊢\phi \to L\left(G\right)\subseteq V$$
17	1 2 3 4 5 8 16	dochn0nv	$$⊢\phi \to \left(\underset{\dot{}}{\perp }\left(L\left(G\right)\right)\ne \left\{\underset{\dot{}}{0}\right\}\leftrightarrow \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(G\right)\right)\right)\ne V\right)$$
18	14 17	mpbid	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(G\right)\right)\right)\ne V$$