Theorem dochfln0

Description: The value of a functional is nonzero at a nonzero vector in the orthocomplement of its kernel. (Contributed by NM, 2-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		dochfln0.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		dochfln0.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
3		dochfln0.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
4		dochfln0.v	$$⊢V={\mathrm{Base}}_U$$
5		dochfln0.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
6		dochfln0.n	$$⊢N=0_R$$
7		dochfln0.z	$$⊢\underset{\dot{}}{0}=0_U$$
8		dochfln0.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
9		dochfln0.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
10		dochfln0.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
11		dochfln0.g	$$⊢\phi \to G\in F$$
12		dochfln0.x	$$⊢\phi \to X\in \left(\underset{\dot{}}{\perp }\left(L\left(G\right)\right)\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
13	1 3 10	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
14	4 8 9 13 11	lkrssv	$$⊢\phi \to L\left(G\right)\subseteq V$$
15	1 3 4 2	dochssv	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge L\left(G\right)\subseteq V\right)\to \underset{\dot{}}{\perp }\left(L\left(G\right)\right)\subseteq V$$
16	10 14 15	syl2anc	$$⊢\phi \to \underset{\dot{}}{\perp }\left(L\left(G\right)\right)\subseteq V$$
17	16	ssdifd	$$⊢\phi \to \underset{\dot{}}{\perp }\left(L\left(G\right)\right)\setminus \left\{\underset{\dot{}}{0}\right\}\subseteq V\setminus \left\{\underset{\dot{}}{0}\right\}$$
18	17 12	sseldd	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
19	1 2 3 4 7 10 18	dochnel	$$⊢\phi \to \neg X\in \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)$$
20	12	eldifad	$$⊢\phi \to X\in \underset{\dot{}}{\perp }\left(L\left(G\right)\right)$$
21	16 20	sseldd	$$⊢\phi \to X\in V$$
22	21	biantrurd	$$⊢\phi \to \left(G\left(X\right)=N\leftrightarrow \left(X\in V\wedge G\left(X\right)=N\right)\right)$$
23	4 5 6 8 9	ellkr	$$⊢\left(U\in \mathrm{LMod}\wedge G\in F\right)\to \left(X\in L\left(G\right)\leftrightarrow \left(X\in V\wedge G\left(X\right)=N\right)\right)$$
24	13 11 23	syl2anc	$$⊢\phi \to \left(X\in L\left(G\right)\leftrightarrow \left(X\in V\wedge G\left(X\right)=N\right)\right)$$
25	1 2 3 4 7 8 9 10 11 12	dochsnkr	$$⊢\phi \to L\left(G\right)=\underset{\dot{}}{\perp }\left(\left\{X\right\}\right)$$
26	25	eleq2d	$$⊢\phi \to \left(X\in L\left(G\right)\leftrightarrow X\in \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)\right)$$
27	22 24 26	3bitr2rd	$$⊢\phi \to \left(X\in \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)\leftrightarrow G\left(X\right)=N\right)$$
28	27	necon3bbid	$$⊢\phi \to \left(\neg X\in \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)\leftrightarrow G\left(X\right)\ne N\right)$$
29	19 28	mpbid	$$⊢\phi \to G\left(X\right)\ne N$$