Theorem lcfrlem20

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

	Ref	Expression
Hypotheses	lcfrlem17.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	lcfrlem17.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
	lcfrlem17.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	lcfrlem17.v	$$⊢V={\mathrm{Base}}_U$$
	lcfrlem17.p	$$⊢\underset{\dot{}}{+}={+}_U$$
	lcfrlem17.z	$$⊢\underset{\dot{}}{0}=0_U$$
	lcfrlem17.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
	lcfrlem17.a	$$⊢A=\mathrm{LSAtoms}\left(U\right)$$
	lcfrlem17.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	lcfrlem17.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	lcfrlem17.y	$$⊢\phi \to Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	lcfrlem17.ne	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)$$
	lcfrlem20.e	$$⊢\phi \to \neg X\in \underset{\dot{}}{\perp }\left(\left\{X\underset{\dot{}}{+}Y\right\}\right)$$
Assertion	lcfrlem20	$$⊢\phi \to N\left(\left\{X,Y\right\}\right)\cap \underset{\dot{}}{\perp }\left(\left\{X\underset{\dot{}}{+}Y\right\}\right)\in A$$

Proof

Step	Hyp	Ref	Expression
1		lcfrlem17.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		lcfrlem17.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
3		lcfrlem17.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
4		lcfrlem17.v	$$⊢V={\mathrm{Base}}_U$$
5		lcfrlem17.p	$$⊢\underset{\dot{}}{+}={+}_U$$
6		lcfrlem17.z	$$⊢\underset{\dot{}}{0}=0_U$$
7		lcfrlem17.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
8		lcfrlem17.a	$$⊢A=\mathrm{LSAtoms}\left(U\right)$$
9		lcfrlem17.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
10		lcfrlem17.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
11		lcfrlem17.y	$$⊢\phi \to Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
12		lcfrlem17.ne	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)$$
13		lcfrlem20.e	$$⊢\phi \to \neg X\in \underset{\dot{}}{\perp }\left(\left\{X\underset{\dot{}}{+}Y\right\}\right)$$
14		eqid	$$⊢\mathrm{LSSum}\left(U\right)=\mathrm{LSSum}\left(U\right)$$
15	1 3 9	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
16	10	eldifad	$$⊢\phi \to X\in V$$
17	11	eldifad	$$⊢\phi \to Y\in V$$
18	4 7 14 15 16 17	lsmpr	$$⊢\phi \to N\left(\left\{X,Y\right\}\right)=N\left(\left\{X\right\}\right)\mathrm{LSSum}\left(U\right)N\left(\left\{Y\right\}\right)$$
19	18	ineq1d	$$⊢\phi \to N\left(\left\{X,Y\right\}\right)\cap \underset{\dot{}}{\perp }\left(\left\{X\underset{\dot{}}{+}Y\right\}\right)=\left(N\left(\left\{X\right\}\right)\mathrm{LSSum}\left(U\right)N\left(\left\{Y\right\}\right)\right)\cap \underset{\dot{}}{\perp }\left(\left\{X\underset{\dot{}}{+}Y\right\}\right)$$
20		eqid	$$⊢\mathrm{LSubSp}\left(U\right)=\mathrm{LSubSp}\left(U\right)$$
21		eqid	$$⊢\mathrm{LSHyp}\left(U\right)=\mathrm{LSHyp}\left(U\right)$$
22	1 3 9	dvhlvec	$$⊢\phi \to U\in \mathrm{LVec}$$
23	1 2 3 4 5 6 7 8 9 10 11 12	lcfrlem17	$$⊢\phi \to X\underset{\dot{}}{+}Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
24	1 2 3 4 6 21 9 23	dochsnshp	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\left\{X\underset{\dot{}}{+}Y\right\}\right)\in \mathrm{LSHyp}\left(U\right)$$
25	4 7 6 8 15 10	lsatlspsn	$$⊢\phi \to N\left(\left\{X\right\}\right)\in A$$
26	4 7 6 8 15 11	lsatlspsn	$$⊢\phi \to N\left(\left\{Y\right\}\right)\in A$$
27	4 5	lmodvacl	$$⊢\left(U\in \mathrm{LMod}\wedge X\in V\wedge Y\in V\right)\to X\underset{\dot{}}{+}Y\in V$$
28	15 16 17 27	syl3anc	$$⊢\phi \to X\underset{\dot{}}{+}Y\in V$$
29	28	snssd	$$⊢\phi \to \left\{X\underset{\dot{}}{+}Y\right\}\subseteq V$$
30	1 3 4 20 2	dochlss	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left\{X\underset{\dot{}}{+}Y\right\}\subseteq V\right)\to \underset{\dot{}}{\perp }\left(\left\{X\underset{\dot{}}{+}Y\right\}\right)\in \mathrm{LSubSp}\left(U\right)$$
31	9 29 30	syl2anc	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\left\{X\underset{\dot{}}{+}Y\right\}\right)\in \mathrm{LSubSp}\left(U\right)$$
32	4 20 7 15 31 16	ellspsn5b	$$⊢\phi \to \left(X\in \underset{\dot{}}{\perp }\left(\left\{X\underset{\dot{}}{+}Y\right\}\right)\leftrightarrow N\left(\left\{X\right\}\right)\subseteq \underset{\dot{}}{\perp }\left(\left\{X\underset{\dot{}}{+}Y\right\}\right)\right)$$
33	13 32	mtbid	$$⊢\phi \to \neg N\left(\left\{X\right\}\right)\subseteq \underset{\dot{}}{\perp }\left(\left\{X\underset{\dot{}}{+}Y\right\}\right)$$
34	20 14 21 8 22 24 25 26 12 33	lshpat	$$⊢\phi \to \left(N\left(\left\{X\right\}\right)\mathrm{LSSum}\left(U\right)N\left(\left\{Y\right\}\right)\right)\cap \underset{\dot{}}{\perp }\left(\left\{X\underset{\dot{}}{+}Y\right\}\right)\in A$$
35	19 34	eqeltrd	$$⊢\phi \to N\left(\left\{X,Y\right\}\right)\cap \underset{\dot{}}{\perp }\left(\left\{X\underset{\dot{}}{+}Y\right\}\right)\in A$$