Theorem dochsnkr2cl

Description: The X determining functional G belongs to the atom formed by the orthocomplement of the kernel. (Contributed by NM, 4-Jan-2015)

	Ref	Expression
Hypotheses	dochsnkr2.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dochsnkr2.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
	dochsnkr2.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	dochsnkr2.v	$$⊢V={\mathrm{Base}}_U$$
	dochsnkr2.z	$$⊢\underset{\dot{}}{0}=0_U$$
	dochsnkr2.a	$$⊢\underset{\dot{}}{+}={+}_U$$
	dochsnkr2.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
	dochsnkr2.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
	dochsnkr2.d	$$⊢D=\mathrm{Scalar}\left(U\right)$$
	dochsnkr2.r	$$⊢R={\mathrm{Base}}_D$$
	dochsnkr2.g	$$⊢G=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}X\right)\right)\right)$$
	dochsnkr2.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	dochsnkr2.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
Assertion	dochsnkr2cl	$$⊢\phi \to X\in \left(\underset{\dot{}}{\perp }\left(L\left(G\right)\right)\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		dochsnkr2.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		dochsnkr2.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
3		dochsnkr2.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
4		dochsnkr2.v	$$⊢V={\mathrm{Base}}_U$$
5		dochsnkr2.z	$$⊢\underset{\dot{}}{0}=0_U$$
6		dochsnkr2.a	$$⊢\underset{\dot{}}{+}={+}_U$$
7		dochsnkr2.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
8		dochsnkr2.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
9		dochsnkr2.d	$$⊢D=\mathrm{Scalar}\left(U\right)$$
10		dochsnkr2.r	$$⊢R={\mathrm{Base}}_D$$
11		dochsnkr2.g	$$⊢G=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}X\right)\right)\right)$$
12		dochsnkr2.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
13		dochsnkr2.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
14	1 3 12	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
15	13	eldifad	$$⊢\phi \to X\in V$$
16		eqid	$$⊢\mathrm{LSpan}\left(U\right)=\mathrm{LSpan}\left(U\right)$$
17	4 16	lspsnid	$$⊢\left(U\in \mathrm{LMod}\wedge X\in V\right)\to X\in \mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)$$
18	14 15 17	syl2anc	$$⊢\phi \to X\in \mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)$$
19	1 2 3 4 5 6 7 8 9 10 11 12 13	dochsnkr2	$$⊢\phi \to L\left(G\right)=\underset{\dot{}}{\perp }\left(\left\{X\right\}\right)$$
20	15	snssd	$$⊢\phi \to \left\{X\right\}\subseteq V$$
21	1 3 2 4 16 12 20	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)$$
22	19 21	eqtr4d	$$⊢\phi \to L\left(G\right)=\underset{\dot{}}{\perp }\left(\mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)\right)$$
23	22	fveq2d	$$⊢\phi \to \underset{\dot{}}{\perp }\left(L\left(G\right)\right)=\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(\mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)\right)\right)$$
24		eqid	$$⊢\mathrm{DIsoH}\left(K\right)\left(W\right)=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
25	1 3 4 16 24	dihlsprn	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge X\in V\right)\to \mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)\in \mathrm{ran}\mathrm{DIsoH}\left(K\right)\left(W\right)$$
26	12 15 25	syl2anc	$$⊢\phi \to \mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)\in \mathrm{ran}\mathrm{DIsoH}\left(K\right)\left(W\right)$$
27	1 24 2	dochoc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)\in \mathrm{ran}\mathrm{DIsoH}\left(K\right)\left(W\right)\right)\to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(\mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)\right)\right)=\mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)$$
28	12 26 27	syl2anc	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(\mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)\right)\right)=\mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)$$
29	23 28	eqtr2d	$$⊢\phi \to \mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)=\underset{\dot{}}{\perp }\left(L\left(G\right)\right)$$
30	18 29	eleqtrd	$$⊢\phi \to X\in \underset{\dot{}}{\perp }\left(L\left(G\right)\right)$$
31		eldifsni	$$⊢X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\to X\ne \underset{\dot{}}{0}$$
32	13 31	syl	$$⊢\phi \to X\ne \underset{\dot{}}{0}$$
33		eldifsn	$$⊢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 X\ne \underset{\dot{}}{0}\right)$$
34	30 32 33	sylanbrc	$$⊢\phi \to X\in \left(\underset{\dot{}}{\perp }\left(L\left(G\right)\right)\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$