Theorem lcfrlem21

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)$$
Assertion	lcfrlem21	$$⊢\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	9	adantr	$$⊢\left(\phi \wedge \neg X\in \underset{\dot{}}{\perp }\left(\left\{X\underset{\dot{}}{+}Y\right\}\right)\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
14	10	adantr	$$⊢\left(\phi \wedge \neg X\in \underset{\dot{}}{\perp }\left(\left\{X\underset{\dot{}}{+}Y\right\}\right)\right)\to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
15	11	adantr	$$⊢\left(\phi \wedge \neg X\in \underset{\dot{}}{\perp }\left(\left\{X\underset{\dot{}}{+}Y\right\}\right)\right)\to Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
16	12	adantr	$$⊢\left(\phi \wedge \neg X\in \underset{\dot{}}{\perp }\left(\left\{X\underset{\dot{}}{+}Y\right\}\right)\right)\to N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)$$
17		simpr	$$⊢\left(\phi \wedge \neg X\in \underset{\dot{}}{\perp }\left(\left\{X\underset{\dot{}}{+}Y\right\}\right)\right)\to \neg X\in \underset{\dot{}}{\perp }\left(\left\{X\underset{\dot{}}{+}Y\right\}\right)$$
18	1 2 3 4 5 6 7 8 13 14 15 16 17	lcfrlem20	$$⊢\left(\phi \wedge \neg X\in \underset{\dot{}}{\perp }\left(\left\{X\underset{\dot{}}{+}Y\right\}\right)\right)\to N\left(\left\{X,Y\right\}\right)\cap \underset{\dot{}}{\perp }\left(\left\{X\underset{\dot{}}{+}Y\right\}\right)\in A$$
19	1 3 9	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
20	10	eldifad	$$⊢\phi \to X\in V$$
21	11	eldifad	$$⊢\phi \to Y\in V$$
22	4 5	lmodcom	$$⊢\left(U\in \mathrm{LMod}\wedge X\in V\wedge Y\in V\right)\to X\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}X$$
23	19 20 21 22	syl3anc	$$⊢\phi \to X\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}X$$
24	23	sneqd	$$⊢\phi \to \left\{X\underset{\dot{}}{+}Y\right\}=\left\{Y\underset{\dot{}}{+}X\right\}$$
25	24	fveq2d	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\left\{X\underset{\dot{}}{+}Y\right\}\right)=\underset{\dot{}}{\perp }\left(\left\{Y\underset{\dot{}}{+}X\right\}\right)$$
26	25	eleq2d	$$⊢\phi \to \left(Y\in \underset{\dot{}}{\perp }\left(\left\{X\underset{\dot{}}{+}Y\right\}\right)\leftrightarrow Y\in \underset{\dot{}}{\perp }\left(\left\{Y\underset{\dot{}}{+}X\right\}\right)\right)$$
27	26	biimprd	$$⊢\phi \to \left(Y\in \underset{\dot{}}{\perp }\left(\left\{Y\underset{\dot{}}{+}X\right\}\right)\to Y\in \underset{\dot{}}{\perp }\left(\left\{X\underset{\dot{}}{+}Y\right\}\right)\right)$$
28	27	con3dimp	$$⊢\left(\phi \wedge \neg Y\in \underset{\dot{}}{\perp }\left(\left\{X\underset{\dot{}}{+}Y\right\}\right)\right)\to \neg Y\in \underset{\dot{}}{\perp }\left(\left\{Y\underset{\dot{}}{+}X\right\}\right)$$
29		prcom	$$⊢\left\{X,Y\right\}=\left\{Y,X\right\}$$
30	29	fveq2i	$$⊢N\left(\left\{X,Y\right\}\right)=N\left(\left\{Y,X\right\}\right)$$
31	30	a1i	$$⊢\phi \to N\left(\left\{X,Y\right\}\right)=N\left(\left\{Y,X\right\}\right)$$
32	31 25	ineq12d	$$⊢\phi \to N\left(\left\{X,Y\right\}\right)\cap \underset{\dot{}}{\perp }\left(\left\{X\underset{\dot{}}{+}Y\right\}\right)=N\left(\left\{Y,X\right\}\right)\cap \underset{\dot{}}{\perp }\left(\left\{Y\underset{\dot{}}{+}X\right\}\right)$$
33	32	adantr	$$⊢\left(\phi \wedge \neg Y\in \underset{\dot{}}{\perp }\left(\left\{Y\underset{\dot{}}{+}X\right\}\right)\right)\to N\left(\left\{X,Y\right\}\right)\cap \underset{\dot{}}{\perp }\left(\left\{X\underset{\dot{}}{+}Y\right\}\right)=N\left(\left\{Y,X\right\}\right)\cap \underset{\dot{}}{\perp }\left(\left\{Y\underset{\dot{}}{+}X\right\}\right)$$
34	9	adantr	$$⊢\left(\phi \wedge \neg Y\in \underset{\dot{}}{\perp }\left(\left\{Y\underset{\dot{}}{+}X\right\}\right)\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
35	11	adantr	$$⊢\left(\phi \wedge \neg Y\in \underset{\dot{}}{\perp }\left(\left\{Y\underset{\dot{}}{+}X\right\}\right)\right)\to Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
36	10	adantr	$$⊢\left(\phi \wedge \neg Y\in \underset{\dot{}}{\perp }\left(\left\{Y\underset{\dot{}}{+}X\right\}\right)\right)\to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
37	12	necomd	$$⊢\phi \to N\left(\left\{Y\right\}\right)\ne N\left(\left\{X\right\}\right)$$
38	37	adantr	$$⊢\left(\phi \wedge \neg Y\in \underset{\dot{}}{\perp }\left(\left\{Y\underset{\dot{}}{+}X\right\}\right)\right)\to N\left(\left\{Y\right\}\right)\ne N\left(\left\{X\right\}\right)$$
39		simpr	$$⊢\left(\phi \wedge \neg Y\in \underset{\dot{}}{\perp }\left(\left\{Y\underset{\dot{}}{+}X\right\}\right)\right)\to \neg Y\in \underset{\dot{}}{\perp }\left(\left\{Y\underset{\dot{}}{+}X\right\}\right)$$
40	1 2 3 4 5 6 7 8 34 35 36 38 39	lcfrlem20	$$⊢\left(\phi \wedge \neg Y\in \underset{\dot{}}{\perp }\left(\left\{Y\underset{\dot{}}{+}X\right\}\right)\right)\to N\left(\left\{Y,X\right\}\right)\cap \underset{\dot{}}{\perp }\left(\left\{Y\underset{\dot{}}{+}X\right\}\right)\in A$$
41	33 40	eqeltrd	$$⊢\left(\phi \wedge \neg Y\in \underset{\dot{}}{\perp }\left(\left\{Y\underset{\dot{}}{+}X\right\}\right)\right)\to N\left(\left\{X,Y\right\}\right)\cap \underset{\dot{}}{\perp }\left(\left\{X\underset{\dot{}}{+}Y\right\}\right)\in A$$
42	28 41	syldan	$$⊢\left(\phi \wedge \neg Y\in \underset{\dot{}}{\perp }\left(\left\{X\underset{\dot{}}{+}Y\right\}\right)\right)\to N\left(\left\{X,Y\right\}\right)\cap \underset{\dot{}}{\perp }\left(\left\{X\underset{\dot{}}{+}Y\right\}\right)\in A$$
43	1 2 3 4 5 6 7 8 9 10 11 12	lcfrlem19	$$⊢\phi \to \left(\neg X\in \underset{\dot{}}{\perp }\left(\left\{X\underset{\dot{}}{+}Y\right\}\right)\vee \neg Y\in \underset{\dot{}}{\perp }\left(\left\{X\underset{\dot{}}{+}Y\right\}\right)\right)$$
44	18 42 43	mpjaodan	$$⊢\phi \to N\left(\left\{X,Y\right\}\right)\cap \underset{\dot{}}{\perp }\left(\left\{X\underset{\dot{}}{+}Y\right\}\right)\in A$$