Theorem lcfl6lem

Description: Lemma for lcfl6 . A functional G (whose kernel is closed by dochsnkr ) is completely determined by a vector X in the orthocomplement in its kernel at which the functional value is 1. Note that the \ { .0. } in the X hypothesis is redundant by the last hypothesis but allows easier use of other theorems. (Contributed by NM, 3-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		lcfl6lem.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		lcfl6lem.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
3		lcfl6lem.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
4		lcfl6lem.v	$$⊢V={\mathrm{Base}}_U$$
5		lcfl6lem.a	$$⊢\underset{\dot{}}{+}={+}_U$$
6		lcfl6lem.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
7		lcfl6lem.s	$$⊢S=\mathrm{Scalar}\left(U\right)$$
8		lcfl6lem.i	$$⊢\underset{\dot{}}{1}=1_S$$
9		lcfl6lem.r	$$⊢R={\mathrm{Base}}_S$$
10		lcfl6lem.z	$$⊢\underset{\dot{}}{0}=0_U$$
11		lcfl6lem.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
12		lcfl6lem.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
13		lcfl6lem.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
14		lcfl6lem.g	$$⊢\phi \to G\in F$$
15		lcfl6lem.x	$$⊢\phi \to X\in \left(\underset{\dot{}}{\perp }\left(L\left(G\right)\right)\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
16		lcfl6lem.y	$$⊢\phi \to G\left(X\right)=\underset{\dot{}}{1}$$
17		eqid	$$⊢0_S=0_S$$
18	1 3 13	dvhlvec	$$⊢\phi \to U\in \mathrm{LVec}$$
19	1 3 13	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
20	4 11 12 19 14	lkrssv	$$⊢\phi \to L\left(G\right)\subseteq V$$
21	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$$
22	13 20 21	syl2anc	$$⊢\phi \to \underset{\dot{}}{\perp }\left(L\left(G\right)\right)\subseteq V$$
23	15	eldifad	$$⊢\phi \to X\in \underset{\dot{}}{\perp }\left(L\left(G\right)\right)$$
24	22 23	sseldd	$$⊢\phi \to X\in V$$
25		eqid	$$⊢\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)=\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)$$
26		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}$$
27	15 26	syl	$$⊢\phi \to X\ne \underset{\dot{}}{0}$$
28		eldifsn	$$⊢X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow \left(X\in V\wedge X\ne \underset{\dot{}}{0}\right)$$
29	24 27 28	sylanbrc	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
30	1 2 3 4 10 5 6 11 7 9 25 13 29	dochflcl	$$⊢\phi \to \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)\in F$$
31	1 2 3 4 10 11 12 13 14 15	dochsnkr	$$⊢\phi \to L\left(G\right)=\underset{\dot{}}{\perp }\left(\left\{X\right\}\right)$$
32	1 2 3 4 10 5 6 12 7 9 25 13 29	dochsnkr2	$$⊢\phi \to L\left(\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)\right)=\underset{\dot{}}{\perp }\left(\left\{X\right\}\right)$$
33	31 32	eqtr4d	$$⊢\phi \to L\left(G\right)=L\left(\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)\right)$$
34	1 2 3 4 5 6 10 7 9 8 13 29 25	dochfl1	$$⊢\phi \to \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)\left(X\right)=\underset{\dot{}}{1}$$
35	16 34	eqtr4d	$$⊢\phi \to G\left(X\right)=\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)\left(X\right)$$
36	1 2 3 4 7 17 10 11 12 13 14 15	dochfln0	$$⊢\phi \to G\left(X\right)\ne 0_S$$
37	4 7 9 17 11 12 18 24 14 30 33 35 36	eqlkr3	$$⊢\phi \to 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)$$