Theorem lcfrlem14

Description: Lemma for lcfr . (Contributed by NM, 10-Mar-2015)

	Ref	Expression
Hypotheses	lcf1o.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	lcf1o.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
	lcf1o.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	lcf1o.v	$$⊢V={\mathrm{Base}}_U$$
	lcf1o.a	$$⊢\underset{\dot{}}{+}={+}_U$$
	lcf1o.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
	lcf1o.s	$$⊢S=\mathrm{Scalar}\left(U\right)$$
	lcf1o.r	$$⊢R={\mathrm{Base}}_S$$
	lcf1o.z	$$⊢\underset{\dot{}}{0}=0_U$$
	lcf1o.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
	lcf1o.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
	lcf1o.d	$$⊢D=\mathrm{LDual}\left(U\right)$$
	lcf1o.q	$$⊢Q=0_D$$
	lcf1o.c	$$⊢C=\left\{f\in F|\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(f\right)\right)\right)=L\left(f\right)\right\}$$
	lcf1o.j	$$⊢J=\left(x\in \left(V\setminus \left\{\underset{\dot{}}{0}\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)\right)$$
	lcflo.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	lcfrlem10.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	lcfrlem14.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
Assertion	lcfrlem14	$$⊢\phi \to \underset{\dot{}}{\perp }\left(L\left(J\left(X\right)\right)\right)=N\left(\left\{X\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		lcf1o.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		lcf1o.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
3		lcf1o.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
4		lcf1o.v	$$⊢V={\mathrm{Base}}_U$$
5		lcf1o.a	$$⊢\underset{\dot{}}{+}={+}_U$$
6		lcf1o.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
7		lcf1o.s	$$⊢S=\mathrm{Scalar}\left(U\right)$$
8		lcf1o.r	$$⊢R={\mathrm{Base}}_S$$
9		lcf1o.z	$$⊢\underset{\dot{}}{0}=0_U$$
10		lcf1o.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
11		lcf1o.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
12		lcf1o.d	$$⊢D=\mathrm{LDual}\left(U\right)$$
13		lcf1o.q	$$⊢Q=0_D$$
14		lcf1o.c	$$⊢C=\left\{f\in F|\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(f\right)\right)\right)=L\left(f\right)\right\}$$
15		lcf1o.j	$$⊢J=\left(x\in \left(V\setminus \left\{\underset{\dot{}}{0}\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)\right)$$
16		lcflo.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
17		lcfrlem10.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
18		lcfrlem14.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
19	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17	lcfrlem11	$$⊢\phi \to L\left(J\left(X\right)\right)=\underset{\dot{}}{\perp }\left(\left\{X\right\}\right)$$
20	17	eldifad	$$⊢\phi \to X\in V$$
21	20	snssd	$$⊢\phi \to \left\{X\right\}\subseteq V$$
22	1 3 2 4 18 16 21	dochocsp	$$⊢\phi \to \underset{\dot{}}{\perp }\left(N\left(\left\{X\right\}\right)\right)=\underset{\dot{}}{\perp }\left(\left\{X\right\}\right)$$
23	19 22	eqtr4d	$$⊢\phi \to L\left(J\left(X\right)\right)=\underset{\dot{}}{\perp }\left(N\left(\left\{X\right\}\right)\right)$$
24	23	fveq2d	$$⊢\phi \to \underset{\dot{}}{\perp }\left(L\left(J\left(X\right)\right)\right)=\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(N\left(\left\{X\right\}\right)\right)\right)$$
25		eqid	$$⊢\mathrm{DIsoH}\left(K\right)\left(W\right)=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
26	1 3 4 18 25	dihlsprn	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge X\in V\right)\to N\left(\left\{X\right\}\right)\in \mathrm{ran}\mathrm{DIsoH}\left(K\right)\left(W\right)$$
27	16 20 26	syl2anc	$$⊢\phi \to N\left(\left\{X\right\}\right)\in \mathrm{ran}\mathrm{DIsoH}\left(K\right)\left(W\right)$$
28	1 25 2	dochoc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge N\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(N\left(\left\{X\right\}\right)\right)\right)=N\left(\left\{X\right\}\right)$$
29	16 27 28	syl2anc	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(N\left(\left\{X\right\}\right)\right)\right)=N\left(\left\{X\right\}\right)$$
30	24 29	eqtrd	$$⊢\phi \to \underset{\dot{}}{\perp }\left(L\left(J\left(X\right)\right)\right)=N\left(\left\{X\right\}\right)$$