Theorem lclkrlem2g

Description: Lemma for lclkr . Comparable hyperplanes are equal, so the kernel of the sum is closed. (Contributed by NM, 16-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)$$
	lclkrlem2f.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	lclkrlem2f.y	$$⊢\phi \to Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	lclkrlem2f.ne	$$⊢\phi \to L\left(E\right)\ne L\left(G\right)$$
	lclkrlem2f.lp	$$⊢\phi \to L\left(E\underset{\dot{}}{+}G\right)\in J$$
Assertion	lclkrlem2g	$$⊢\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		lclkrlem2f.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
24		lclkrlem2f.y	$$⊢\phi \to Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
25		lclkrlem2f.ne	$$⊢\phi \to L\left(E\right)\ne L\left(G\right)$$
26		lclkrlem2f.lp	$$⊢\phi \to L\left(E\underset{\dot{}}{+}G\right)\in J$$
27	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26	lclkrlem2f	$$⊢\phi \to \left(L\left(E\right)\cap L\left(G\right)\right)\underset{\dot{}}{\oplus }N\left(\left\{B\right\}\right)\subseteq L\left(E\underset{\dot{}}{+}G\right)$$
28	1 3 15	dvhlvec	$$⊢\phi \to U\in \mathrm{LVec}$$
29	19 20	ineq12d	$$⊢\phi \to L\left(E\right)\cap L\left(G\right)=\underset{\dot{}}{\perp }\left(\left\{X\right\}\right)\cap \underset{\dot{}}{\perp }\left(\left\{Y\right\}\right)$$
30	29	oveq1d	$$⊢\phi \to \left(L\left(E\right)\cap L\left(G\right)\right)\underset{\dot{}}{\oplus }N\left(\left\{B\right\}\right)=\left(\underset{\dot{}}{\perp }\left(\left\{X\right\}\right)\cap \underset{\dot{}}{\perp }\left(\left\{Y\right\}\right)\right)\underset{\dot{}}{\oplus }N\left(\left\{B\right\}\right)$$
31		eqid	$$⊢\mathrm{LSAtoms}\left(U\right)=\mathrm{LSAtoms}\left(U\right)$$
32	25 19 20	3netr3d	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)\ne \underset{\dot{}}{\perp }\left(\left\{Y\right\}\right)$$
33	1 2 3 4 7 8 9 31 15 16 23 24 32 22 11	lclkrlem2c	$$⊢\phi \to \left(\underset{\dot{}}{\perp }\left(\left\{X\right\}\right)\cap \underset{\dot{}}{\perp }\left(\left\{Y\right\}\right)\right)\underset{\dot{}}{\oplus }N\left(\left\{B\right\}\right)\in J$$
34	30 33	eqeltrd	$$⊢\phi \to \left(L\left(E\right)\cap L\left(G\right)\right)\underset{\dot{}}{\oplus }N\left(\left\{B\right\}\right)\in J$$
35	11 28 34 26	lshpcmp	$$⊢\phi \to \left(\left(L\left(E\right)\cap L\left(G\right)\right)\underset{\dot{}}{\oplus }N\left(\left\{B\right\}\right)\subseteq L\left(E\underset{\dot{}}{+}G\right)\leftrightarrow \left(L\left(E\right)\cap L\left(G\right)\right)\underset{\dot{}}{\oplus }N\left(\left\{B\right\}\right)=L\left(E\underset{\dot{}}{+}G\right)\right)$$
36	27 35	mpbid	$$⊢\phi \to \left(L\left(E\right)\cap L\left(G\right)\right)\underset{\dot{}}{\oplus }N\left(\left\{B\right\}\right)=L\left(E\underset{\dot{}}{+}G\right)$$
37		eqid	$$⊢\mathrm{DIsoH}\left(K\right)\left(W\right)=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
38	1 2 3 4 7 8 9 31 15 16 23 24 32 22 37	lclkrlem2d	$$⊢\phi \to \left(\underset{\dot{}}{\perp }\left(\left\{X\right\}\right)\cap \underset{\dot{}}{\perp }\left(\left\{Y\right\}\right)\right)\underset{\dot{}}{\oplus }N\left(\left\{B\right\}\right)\in \mathrm{ran}\mathrm{DIsoH}\left(K\right)\left(W\right)$$
39	30 38	eqeltrd	$$⊢\phi \to \left(L\left(E\right)\cap L\left(G\right)\right)\underset{\dot{}}{\oplus }N\left(\left\{B\right\}\right)\in \mathrm{ran}\mathrm{DIsoH}\left(K\right)\left(W\right)$$
40	36 39	eqeltrrd	$$⊢\phi \to L\left(E\underset{\dot{}}{+}G\right)\in \mathrm{ran}\mathrm{DIsoH}\left(K\right)\left(W\right)$$
41	1 3 37 4	dihrnss	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge L\left(E\underset{\dot{}}{+}G\right)\in \mathrm{ran}\mathrm{DIsoH}\left(K\right)\left(W\right)\right)\to L\left(E\underset{\dot{}}{+}G\right)\subseteq V$$
42	15 40 41	syl2anc	$$⊢\phi \to L\left(E\underset{\dot{}}{+}G\right)\subseteq V$$
43	1 37 3 4 2 15 42	dochoccl	$$⊢\phi \to \left(L\left(E\underset{\dot{}}{+}G\right)\in \mathrm{ran}\mathrm{DIsoH}\left(K\right)\left(W\right)\leftrightarrow \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(E\underset{\dot{}}{+}G\right)\right)\right)=L\left(E\underset{\dot{}}{+}G\right)\right)$$
44	40 43	mpbid	$$⊢\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)$$