Theorem dochsnkr

Description: A (closed) kernel expressed in terms of a nonzero vector in its orthocomplement. TODO: consolidate lemmas unless they're needed for something else (in which case break out as theorems). (Contributed by NM, 2-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	dochsnkr	$$⊢\phi \to L\left(G\right)=\underset{\dot{}}{\perp }\left(\left\{X\right\}\right)$$

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		eqid	$$⊢\mathrm{LSpan}\left(U\right)=\mathrm{LSpan}\left(U\right)$$
12		eqid	$$⊢\mathrm{LSAtoms}\left(U\right)=\mathrm{LSAtoms}\left(U\right)$$
13	1 3 8	dvhlvec	$$⊢\phi \to U\in \mathrm{LVec}$$
14	1 2 3 4 5 6 7 8 9 10 12	dochsnkrlem2	$$⊢\phi \to \underset{\dot{}}{\perp }\left(L\left(G\right)\right)\in \mathrm{LSAtoms}\left(U\right)$$
15	10	eldifad	$$⊢\phi \to X\in \underset{\dot{}}{\perp }\left(L\left(G\right)\right)$$
16		eldifsni	$$⊢X\in \left(\underset{\dot{}}{\perp }\left(L\left(G\right)\right)\setminus \left\{\underset{\dot{}}{0}\right\}\right)\to X\ne \underset{\dot{}}{0}$$
17	10 16	syl	$$⊢\phi \to X\ne \underset{\dot{}}{0}$$
18	5 11 12 13 14 15 17	lsatel	$$⊢\phi \to \underset{\dot{}}{\perp }\left(L\left(G\right)\right)=\mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)$$
19	18	fveq2d	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(G\right)\right)\right)=\underset{\dot{}}{\perp }\left(\mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)\right)$$
20	1 2 3 4 5 6 7 8 9 10	dochsnkrlem3	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(G\right)\right)\right)=L\left(G\right)$$
21	1 3 8	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
22	4 6 7 21 9	lkrssv	$$⊢\phi \to L\left(G\right)\subseteq V$$
23	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$$
24	8 22 23	syl2anc	$$⊢\phi \to \underset{\dot{}}{\perp }\left(L\left(G\right)\right)\subseteq V$$
25	24	ssdifssd	$$⊢\phi \to \underset{\dot{}}{\perp }\left(L\left(G\right)\right)\setminus \left\{\underset{\dot{}}{0}\right\}\subseteq V$$
26	25 10	sseldd	$$⊢\phi \to X\in V$$
27	26	snssd	$$⊢\phi \to \left\{X\right\}\subseteq V$$
28	1 3 2 4 11 8 27	dochocsp	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)\right)=\underset{\dot{}}{\perp }\left(\left\{X\right\}\right)$$
29	19 20 28	3eqtr3d	$$⊢\phi \to L\left(G\right)=\underset{\dot{}}{\perp }\left(\left\{X\right\}\right)$$