Theorem lclkrlem2j

Description: Lemma for lclkr . Kernel closure when Y is zero. (Contributed by NM, 18-Jan-2015)

	Ref	Expression
Hypotheses	lclkrlem2f.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	lclkrlem2f.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
	lclkrlem2f.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	lclkrlem2f.v	$$⊢V={\mathrm{Base}}_U$$
	lclkrlem2f.s	$$⊢S=\mathrm{Scalar}\left(U\right)$$
	lclkrlem2f.q	$$⊢Q=0_S$$
	lclkrlem2f.z	$$⊢\underset{\dot{}}{0}=0_U$$
	lclkrlem2f.a	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(U\right)$$
	lclkrlem2f.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
	lclkrlem2f.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
	lclkrlem2f.j	$$⊢J=\mathrm{LSHyp}\left(U\right)$$
	lclkrlem2f.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
	lclkrlem2f.d	$$⊢D=\mathrm{LDual}\left(U\right)$$
	lclkrlem2f.p	$$⊢\underset{\dot{}}{+}={+}_D$$
	lclkrlem2f.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	lclkrlem2f.b	$$⊢\phi \to B\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	lclkrlem2f.e	$$⊢\phi \to E\in F$$
	lclkrlem2f.g	$$⊢\phi \to G\in F$$
	lclkrlem2f.le	$$⊢\phi \to L\left(E\right)=\underset{\dot{}}{\perp }\left(\left\{X\right\}\right)$$
	lclkrlem2f.lg	$$⊢\phi \to L\left(G\right)=\underset{\dot{}}{\perp }\left(\left\{Y\right\}\right)$$
	lclkrlem2f.kb	$$⊢\phi \to \left(E\underset{\dot{}}{+}G\right)\left(B\right)=Q$$
	lclkrlem2f.nx	$$⊢\phi \to \left(\neg X\in \underset{\dot{}}{\perp }\left(\left\{B\right\}\right)\vee \neg Y\in \underset{\dot{}}{\perp }\left(\left\{B\right\}\right)\right)$$
	lclkrlem2j.x	$$⊢\phi \to X\in V$$
	lclkrlem2j.y	$$⊢\phi \to Y=\underset{\dot{}}{0}$$
Assertion	lclkrlem2j	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(E\underset{\dot{}}{+}G\right)\right)\right)=L\left(E\underset{\dot{}}{+}G\right)$$

Proof

Step	Hyp	Ref	Expression
1		lclkrlem2f.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		lclkrlem2f.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
3		lclkrlem2f.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
4		lclkrlem2f.v	$$⊢V={\mathrm{Base}}_U$$
5		lclkrlem2f.s	$$⊢S=\mathrm{Scalar}\left(U\right)$$
6		lclkrlem2f.q	$$⊢Q=0_S$$
7		lclkrlem2f.z	$$⊢\underset{\dot{}}{0}=0_U$$
8		lclkrlem2f.a	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(U\right)$$
9		lclkrlem2f.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
10		lclkrlem2f.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
11		lclkrlem2f.j	$$⊢J=\mathrm{LSHyp}\left(U\right)$$
12		lclkrlem2f.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
13		lclkrlem2f.d	$$⊢D=\mathrm{LDual}\left(U\right)$$
14		lclkrlem2f.p	$$⊢\underset{\dot{}}{+}={+}_D$$
15		lclkrlem2f.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
16		lclkrlem2f.b	$$⊢\phi \to B\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
17		lclkrlem2f.e	$$⊢\phi \to E\in F$$
18		lclkrlem2f.g	$$⊢\phi \to G\in F$$
19		lclkrlem2f.le	$$⊢\phi \to L\left(E\right)=\underset{\dot{}}{\perp }\left(\left\{X\right\}\right)$$
20		lclkrlem2f.lg	$$⊢\phi \to L\left(G\right)=\underset{\dot{}}{\perp }\left(\left\{Y\right\}\right)$$
21		lclkrlem2f.kb	$$⊢\phi \to \left(E\underset{\dot{}}{+}G\right)\left(B\right)=Q$$
22		lclkrlem2f.nx	$$⊢\phi \to \left(\neg X\in \underset{\dot{}}{\perp }\left(\left\{B\right\}\right)\vee \neg Y\in \underset{\dot{}}{\perp }\left(\left\{B\right\}\right)\right)$$
23		lclkrlem2j.x	$$⊢\phi \to X\in V$$
24		lclkrlem2j.y	$$⊢\phi \to Y=\underset{\dot{}}{0}$$
25	23	snssd	$$⊢\phi \to \left\{X\right\}\subseteq V$$
26		eqid	$$⊢\mathrm{DIsoH}\left(K\right)\left(W\right)=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
27	1 26 3 4 2	dochcl	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left\{X\right\}\subseteq V\right)\to \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)\in \mathrm{ran}\mathrm{DIsoH}\left(K\right)\left(W\right)$$
28	15 25 27	syl2anc	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)\in \mathrm{ran}\mathrm{DIsoH}\left(K\right)\left(W\right)$$
29	1 26 2	dochoc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \underset{\dot{}}{\perp }\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(\underset{\dot{}}{\perp }\left(\left\{X\right\}\right)\right)\right)=\underset{\dot{}}{\perp }\left(\left\{X\right\}\right)$$
30	15 28 29	syl2anc	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(\left\{X\right\}\right)\right)\right)=\underset{\dot{}}{\perp }\left(\left\{X\right\}\right)$$
31	24	sneqd	$$⊢\phi \to \left\{Y\right\}=\left\{\underset{\dot{}}{0}\right\}$$
32	31	fveq2d	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\left\{Y\right\}\right)=\underset{\dot{}}{\perp }\left(\left\{\underset{\dot{}}{0}\right\}\right)$$
33		eqid	$$⊢{\mathrm{Base}}_U={\mathrm{Base}}_U$$
34	1 3 2 33 7	doch0	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to \underset{\dot{}}{\perp }\left(\left\{\underset{\dot{}}{0}\right\}\right)={\mathrm{Base}}_U$$
35	15 34	syl	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\left\{\underset{\dot{}}{0}\right\}\right)={\mathrm{Base}}_U$$
36	20 32 35	3eqtrd	$$⊢\phi \to L\left(G\right)={\mathrm{Base}}_U$$
37	1 3 15	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
38	5 6 33 10 12	lkr0f	$$⊢\left(U\in \mathrm{LMod}\wedge G\in F\right)\to \left(L\left(G\right)={\mathrm{Base}}_U\leftrightarrow G={\mathrm{Base}}_U\times \left\{Q\right\}\right)$$
39	37 18 38	syl2anc	$$⊢\phi \to \left(L\left(G\right)={\mathrm{Base}}_U\leftrightarrow G={\mathrm{Base}}_U\times \left\{Q\right\}\right)$$
40	36 39	mpbid	$$⊢\phi \to G={\mathrm{Base}}_U\times \left\{Q\right\}$$
41		eqid	$$⊢0_D=0_D$$
42	33 5 6 13 41 37	ldual0v	$$⊢\phi \to 0_D={\mathrm{Base}}_U\times \left\{Q\right\}$$
43	40 42	eqtr4d	$$⊢\phi \to G=0_D$$
44	43	oveq2d	$$⊢\phi \to E\underset{\dot{}}{+}G=E\underset{\dot{}}{+}{0}_D$$
45	13 37	lduallmod	$$⊢\phi \to D\in \mathrm{LMod}$$
46		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
47	10 13 46 37 17	ldualelvbase	$$⊢\phi \to E\in {\mathrm{Base}}_D$$
48	46 14 41	lmod0vrid	$$⊢\left(D\in \mathrm{LMod}\wedge E\in {\mathrm{Base}}_D\right)\to E\underset{\dot{}}{+}{0}_D=E$$
49	45 47 48	syl2anc	$$⊢\phi \to E\underset{\dot{}}{+}{0}_D=E$$
50	44 49	eqtrd	$$⊢\phi \to E\underset{\dot{}}{+}G=E$$
51	50	fveq2d	$$⊢\phi \to L\left(E\underset{\dot{}}{+}G\right)=L\left(E\right)$$
52	51 19	eqtr2d	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)=L\left(E\underset{\dot{}}{+}G\right)$$
53	52	fveq2d	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(\left\{X\right\}\right)\right)=\underset{\dot{}}{\perp }\left(L\left(E\underset{\dot{}}{+}G\right)\right)$$
54	53	fveq2d	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(\left\{X\right\}\right)\right)\right)=\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(E\underset{\dot{}}{+}G\right)\right)\right)$$
55	30 54 52	3eqtr3d	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(E\underset{\dot{}}{+}G\right)\right)\right)=L\left(E\underset{\dot{}}{+}G\right)$$