Theorem lcfrlem22

Description: Lemma for lcfr . (Contributed by NM, 24-Feb-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)$$
	lcfrlem22.b	$$⊢B=N\left(\left\{X,Y\right\}\right)\cap \underset{\dot{}}{\perp }\left(\left\{X\underset{\dot{}}{+}Y\right\}\right)$$
Assertion	lcfrlem22	$$⊢\phi \to B\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		lcfrlem22.b	$$⊢B=N\left(\left\{X,Y\right\}\right)\cap \underset{\dot{}}{\perp }\left(\left\{X\underset{\dot{}}{+}Y\right\}\right)$$
14	1 2 3 4 5 6 7 8 9 10 11 12	lcfrlem21	$$⊢\phi \to N\left(\left\{X,Y\right\}\right)\cap \underset{\dot{}}{\perp }\left(\left\{X\underset{\dot{}}{+}Y\right\}\right)\in A$$
15	13 14	eqeltrid	$$⊢\phi \to B\in A$$