Theorem dochflcl

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

	Ref	Expression
Hypotheses	dochflcl.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dochflcl.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
	dochflcl.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	dochflcl.v	$$⊢V={\mathrm{Base}}_U$$
	dochflcl.z	$$⊢\underset{\dot{}}{0}=0_U$$
	dochflcl.a	$$⊢\underset{\dot{}}{+}={+}_U$$
	dochflcl.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
	dochflcl.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
	dochflcl.d	$$⊢D=\mathrm{Scalar}\left(U\right)$$
	dochflcl.r	$$⊢R={\mathrm{Base}}_D$$
	dochflcl.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)$$
	dochflcl.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	dochflcl.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
Assertion	dochflcl	$$⊢\phi \to G\in F$$

Proof

Step	Hyp	Ref	Expression
1		dochflcl.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		dochflcl.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
3		dochflcl.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
4		dochflcl.v	$$⊢V={\mathrm{Base}}_U$$
5		dochflcl.z	$$⊢\underset{\dot{}}{0}=0_U$$
6		dochflcl.a	$$⊢\underset{\dot{}}{+}={+}_U$$
7		dochflcl.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
8		dochflcl.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
9		dochflcl.d	$$⊢D=\mathrm{Scalar}\left(U\right)$$
10		dochflcl.r	$$⊢R={\mathrm{Base}}_D$$
11		dochflcl.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		dochflcl.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
13		dochflcl.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	lshpkrcl	$$⊢\phi \to G\in F$$