Theorem dochsnkr2

Description: Kernel of the explicit functional G determined by a nonzero vector X . Compare the more general lshpkr . (Contributed by NM, 27-Oct-2014)

	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	dochsnkr2	$$⊢\phi \to L\left(G\right)=\underset{\dot{}}{\perp }\left(\left\{X\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		eqid	$$⊢\mathrm{LSpan}\left(U\right)=\mathrm{LSpan}\left(U\right)$$
15		eqid	$$⊢\mathrm{LSSum}\left(U\right)=\mathrm{LSSum}\left(U\right)$$
16		eqid	$$⊢\mathrm{LSHyp}\left(U\right)=\mathrm{LSHyp}\left(U\right)$$
17	1 3 12	dvhlvec	$$⊢\phi \to U\in \mathrm{LVec}$$
18	1 2 3 4 5 16 12 13	dochsnshp	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)\in \mathrm{LSHyp}\left(U\right)$$
19	13	eldifad	$$⊢\phi \to X\in V$$
20	1 2 3 4 5 14 15 12 13	dochexmidat	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)\mathrm{LSSum}\left(U\right)\mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)=V$$
21	4 6 14 15 16 17 18 19 20 9 10 7 11 8	lshpkr	$$⊢\phi \to L\left(G\right)=\underset{\dot{}}{\perp }\left(\left\{X\right\}\right)$$