Theorem lclkrlem2d

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

	Ref	Expression
Hypotheses	lclkrlem2a.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	lclkrlem2a.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
	lclkrlem2a.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	lclkrlem2a.v	$$⊢V={\mathrm{Base}}_U$$
	lclkrlem2a.z	$$⊢\underset{\dot{}}{0}=0_U$$
	lclkrlem2a.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(U\right)$$
	lclkrlem2a.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
	lclkrlem2a.a	$$⊢A=\mathrm{LSAtoms}\left(U\right)$$
	lclkrlem2a.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	lclkrlem2a.b	$$⊢\phi \to B\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	lclkrlem2a.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	lclkrlem2a.y	$$⊢\phi \to Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	lclkrlem2a.e	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)\ne \underset{\dot{}}{\perp }\left(\left\{Y\right\}\right)$$
	lclkrlem2b.da	$$⊢\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)$$
	lclkrlem2d.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
Assertion	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}I$$

Proof

Step	Hyp	Ref	Expression
1		lclkrlem2a.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		lclkrlem2a.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
3		lclkrlem2a.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
4		lclkrlem2a.v	$$⊢V={\mathrm{Base}}_U$$
5		lclkrlem2a.z	$$⊢\underset{\dot{}}{0}=0_U$$
6		lclkrlem2a.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(U\right)$$
7		lclkrlem2a.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
8		lclkrlem2a.a	$$⊢A=\mathrm{LSAtoms}\left(U\right)$$
9		lclkrlem2a.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
10		lclkrlem2a.b	$$⊢\phi \to B\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
11		lclkrlem2a.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
12		lclkrlem2a.y	$$⊢\phi \to Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
13		lclkrlem2a.e	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)\ne \underset{\dot{}}{\perp }\left(\left\{Y\right\}\right)$$
14		lclkrlem2b.da	$$⊢\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)$$
15		lclkrlem2d.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
16	11	eldifad	$$⊢\phi \to X\in V$$
17	16	snssd	$$⊢\phi \to \left\{X\right\}\subseteq V$$
18	1 15 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}I$$
19	9 17 18	syl2anc	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)\in \mathrm{ran}I$$
20	12	eldifad	$$⊢\phi \to Y\in V$$
21	20	snssd	$$⊢\phi \to \left\{Y\right\}\subseteq V$$
22	1 15 3 4 2	dochcl	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left\{Y\right\}\subseteq V\right)\to \underset{\dot{}}{\perp }\left(\left\{Y\right\}\right)\in \mathrm{ran}I$$
23	9 21 22	syl2anc	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\left\{Y\right\}\right)\in \mathrm{ran}I$$
24	1 15	dihmeetcl	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\underset{\dot{}}{\perp }\left(\left\{X\right\}\right)\in \mathrm{ran}I\wedge \underset{\dot{}}{\perp }\left(\left\{Y\right\}\right)\in \mathrm{ran}I\right)\right)\to \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)\cap \underset{\dot{}}{\perp }\left(\left\{Y\right\}\right)\in \mathrm{ran}I$$
25	9 19 23 24	syl12anc	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)\cap \underset{\dot{}}{\perp }\left(\left\{Y\right\}\right)\in \mathrm{ran}I$$
26	10	eldifad	$$⊢\phi \to B\in V$$
27	1 3 4 6 7 15 9 25 26	dihsmsprn	$$⊢\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}I$$