Theorem lclkrlem2n

Description: Lemma for lclkr . (Contributed by NM, 12-Jan-2015)

	Ref	Expression
Hypotheses	lclkrlem2m.v	$$⊢V={\mathrm{Base}}_U$$
	lclkrlem2m.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
	lclkrlem2m.s	$$⊢S=\mathrm{Scalar}\left(U\right)$$
	lclkrlem2m.q	$$⊢\underset{\dot{}}{\times }={\cdot }_S$$
	lclkrlem2m.z	$$⊢\underset{\dot{}}{0}=0_S$$
	lclkrlem2m.i	$$⊢I={inv}_r\left(S\right)$$
	lclkrlem2m.m	$$⊢\underset{\dot{}}{-}={-}_U$$
	lclkrlem2m.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
	lclkrlem2m.d	$$⊢D=\mathrm{LDual}\left(U\right)$$
	lclkrlem2m.p	$$⊢\underset{\dot{}}{+}={+}_D$$
	lclkrlem2m.x	$$⊢\phi \to X\in V$$
	lclkrlem2m.y	$$⊢\phi \to Y\in V$$
	lclkrlem2m.e	$$⊢\phi \to E\in F$$
	lclkrlem2m.g	$$⊢\phi \to G\in F$$
	lclkrlem2n.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
	lclkrlem2n.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
	lclkrlem2n.w	$$⊢\phi \to U\in \mathrm{LVec}$$
	lclkrlem2n.j	$$⊢\phi \to \left(E\underset{\dot{}}{+}G\right)\left(X\right)=\underset{\dot{}}{0}$$
	lclkrlem2n.k	$$⊢\phi \to \left(E\underset{\dot{}}{+}G\right)\left(Y\right)=\underset{\dot{}}{0}$$
Assertion	lclkrlem2n	$$⊢\phi \to N\left(\left\{X,Y\right\}\right)\subseteq L\left(E\underset{\dot{}}{+}G\right)$$

Proof

Step	Hyp	Ref	Expression
1		lclkrlem2m.v	$$⊢V={\mathrm{Base}}_U$$
2		lclkrlem2m.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
3		lclkrlem2m.s	$$⊢S=\mathrm{Scalar}\left(U\right)$$
4		lclkrlem2m.q	$$⊢\underset{\dot{}}{\times }={\cdot }_S$$
5		lclkrlem2m.z	$$⊢\underset{\dot{}}{0}=0_S$$
6		lclkrlem2m.i	$$⊢I={inv}_r\left(S\right)$$
7		lclkrlem2m.m	$$⊢\underset{\dot{}}{-}={-}_U$$
8		lclkrlem2m.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
9		lclkrlem2m.d	$$⊢D=\mathrm{LDual}\left(U\right)$$
10		lclkrlem2m.p	$$⊢\underset{\dot{}}{+}={+}_D$$
11		lclkrlem2m.x	$$⊢\phi \to X\in V$$
12		lclkrlem2m.y	$$⊢\phi \to Y\in V$$
13		lclkrlem2m.e	$$⊢\phi \to E\in F$$
14		lclkrlem2m.g	$$⊢\phi \to G\in F$$
15		lclkrlem2n.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
16		lclkrlem2n.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
17		lclkrlem2n.w	$$⊢\phi \to U\in \mathrm{LVec}$$
18		lclkrlem2n.j	$$⊢\phi \to \left(E\underset{\dot{}}{+}G\right)\left(X\right)=\underset{\dot{}}{0}$$
19		lclkrlem2n.k	$$⊢\phi \to \left(E\underset{\dot{}}{+}G\right)\left(Y\right)=\underset{\dot{}}{0}$$
20		eqid	$$⊢\mathrm{LSubSp}\left(U\right)=\mathrm{LSubSp}\left(U\right)$$
21		lveclmod	$$⊢U\in \mathrm{LVec}\to U\in \mathrm{LMod}$$
22	17 21	syl	$$⊢\phi \to U\in \mathrm{LMod}$$
23	8 9 10 22 13 14	ldualvaddcl	$$⊢\phi \to E\underset{\dot{}}{+}G\in F$$
24	8 16 20	lkrlss	$$⊢\left(U\in \mathrm{LMod}\wedge E\underset{\dot{}}{+}G\in F\right)\to L\left(E\underset{\dot{}}{+}G\right)\in \mathrm{LSubSp}\left(U\right)$$
25	22 23 24	syl2anc	$$⊢\phi \to L\left(E\underset{\dot{}}{+}G\right)\in \mathrm{LSubSp}\left(U\right)$$
26	1 3 5 8 16 17 23 11	ellkr2	$$⊢\phi \to \left(X\in L\left(E\underset{\dot{}}{+}G\right)\leftrightarrow \left(E\underset{\dot{}}{+}G\right)\left(X\right)=\underset{\dot{}}{0}\right)$$
27	18 26	mpbird	$$⊢\phi \to X\in L\left(E\underset{\dot{}}{+}G\right)$$
28	1 3 5 8 16 17 23 12	ellkr2	$$⊢\phi \to \left(Y\in L\left(E\underset{\dot{}}{+}G\right)\leftrightarrow \left(E\underset{\dot{}}{+}G\right)\left(Y\right)=\underset{\dot{}}{0}\right)$$
29	19 28	mpbird	$$⊢\phi \to Y\in L\left(E\underset{\dot{}}{+}G\right)$$
30	20 15 22 25 27 29	lspprss	$$⊢\phi \to N\left(\left\{X,Y\right\}\right)\subseteq L\left(E\underset{\dot{}}{+}G\right)$$