Theorem lcfrlem41

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

	Ref	Expression
Hypotheses	lcfrlem38.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	lcfrlem38.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
	lcfrlem38.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	lcfrlem38.p	$$⊢\underset{\dot{}}{+}={+}_U$$
	lcfrlem38.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
	lcfrlem38.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
	lcfrlem38.d	$$⊢D=\mathrm{LDual}\left(U\right)$$
	lcfrlem38.q	$$⊢Q=\mathrm{LSubSp}\left(D\right)$$
	lcfrlem38.c	$$⊢C=\left\{f\in \mathrm{LFnl}\left(U\right)|\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(f\right)\right)\right)=L\left(f\right)\right\}$$
	lcfrlem38.e	$$⊢E=\bigcup _{g\in G}\underset{\dot{}}{\perp }\left(L\left(g\right)\right)$$
	lcfrlem38.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	lcfrlem38.g	$$⊢\phi \to G\in Q$$
	lcfrlem38.gs	$$⊢\phi \to G\subseteq C$$
	lcfrlem38.xe	$$⊢\phi \to X\in E$$
	lcfrlem38.ye	$$⊢\phi \to Y\in E$$
	lcfrlem38.z	$$⊢\underset{\dot{}}{0}=0_U$$
	lcfrlem38.x	$$⊢\phi \to X\ne \underset{\dot{}}{0}$$
	lcfrlem38.y	$$⊢\phi \to Y\ne \underset{\dot{}}{0}$$
Assertion	lcfrlem41	$$⊢\phi \to X\underset{\dot{}}{+}Y\in E$$

Proof

Step	Hyp	Ref	Expression
1		lcfrlem38.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		lcfrlem38.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
3		lcfrlem38.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
4		lcfrlem38.p	$$⊢\underset{\dot{}}{+}={+}_U$$
5		lcfrlem38.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
6		lcfrlem38.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
7		lcfrlem38.d	$$⊢D=\mathrm{LDual}\left(U\right)$$
8		lcfrlem38.q	$$⊢Q=\mathrm{LSubSp}\left(D\right)$$
9		lcfrlem38.c	$$⊢C=\left\{f\in \mathrm{LFnl}\left(U\right)|\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(f\right)\right)\right)=L\left(f\right)\right\}$$
10		lcfrlem38.e	$$⊢E=\bigcup _{g\in G}\underset{\dot{}}{\perp }\left(L\left(g\right)\right)$$
11		lcfrlem38.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
12		lcfrlem38.g	$$⊢\phi \to G\in Q$$
13		lcfrlem38.gs	$$⊢\phi \to G\subseteq C$$
14		lcfrlem38.xe	$$⊢\phi \to X\in E$$
15		lcfrlem38.ye	$$⊢\phi \to Y\in E$$
16		lcfrlem38.z	$$⊢\underset{\dot{}}{0}=0_U$$
17		lcfrlem38.x	$$⊢\phi \to X\ne \underset{\dot{}}{0}$$
18		lcfrlem38.y	$$⊢\phi \to Y\ne \underset{\dot{}}{0}$$
19		eqid	$$⊢\mathrm{LSpan}\left(U\right)=\mathrm{LSpan}\left(U\right)$$
20	11	adantr	$$⊢\left(\phi \wedge \mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)=\mathrm{LSpan}\left(U\right)\left(\left\{Y\right\}\right)\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
21	12	adantr	$$⊢\left(\phi \wedge \mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)=\mathrm{LSpan}\left(U\right)\left(\left\{Y\right\}\right)\right)\to G\in Q$$
22	14	adantr	$$⊢\left(\phi \wedge \mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)=\mathrm{LSpan}\left(U\right)\left(\left\{Y\right\}\right)\right)\to X\in E$$
23	15	adantr	$$⊢\left(\phi \wedge \mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)=\mathrm{LSpan}\left(U\right)\left(\left\{Y\right\}\right)\right)\to Y\in E$$
24		simpr	$$⊢\left(\phi \wedge \mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)=\mathrm{LSpan}\left(U\right)\left(\left\{Y\right\}\right)\right)\to \mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)=\mathrm{LSpan}\left(U\right)\left(\left\{Y\right\}\right)$$
25	1 2 3 4 19 6 7 8 20 21 10 22 23 24	lcfrlem6	$$⊢\left(\phi \wedge \mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)=\mathrm{LSpan}\left(U\right)\left(\left\{Y\right\}\right)\right)\to X\underset{\dot{}}{+}Y\in E$$
26	11	adantr	$$⊢\left(\phi \wedge \mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)\ne \mathrm{LSpan}\left(U\right)\left(\left\{Y\right\}\right)\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
27	12	adantr	$$⊢\left(\phi \wedge \mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)\ne \mathrm{LSpan}\left(U\right)\left(\left\{Y\right\}\right)\right)\to G\in Q$$
28	13	adantr	$$⊢\left(\phi \wedge \mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)\ne \mathrm{LSpan}\left(U\right)\left(\left\{Y\right\}\right)\right)\to G\subseteq C$$
29	14	adantr	$$⊢\left(\phi \wedge \mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)\ne \mathrm{LSpan}\left(U\right)\left(\left\{Y\right\}\right)\right)\to X\in E$$
30	15	adantr	$$⊢\left(\phi \wedge \mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)\ne \mathrm{LSpan}\left(U\right)\left(\left\{Y\right\}\right)\right)\to Y\in E$$
31	17	adantr	$$⊢\left(\phi \wedge \mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)\ne \mathrm{LSpan}\left(U\right)\left(\left\{Y\right\}\right)\right)\to X\ne \underset{\dot{}}{0}$$
32	18	adantr	$$⊢\left(\phi \wedge \mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)\ne \mathrm{LSpan}\left(U\right)\left(\left\{Y\right\}\right)\right)\to Y\ne \underset{\dot{}}{0}$$
33		simpr	$$⊢\left(\phi \wedge \mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)\ne \mathrm{LSpan}\left(U\right)\left(\left\{Y\right\}\right)\right)\to \mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)\ne \mathrm{LSpan}\left(U\right)\left(\left\{Y\right\}\right)$$
34	1 2 3 4 5 6 7 8 9 10 26 27 28 29 30 16 31 32 19 33	lcfrlem40	$$⊢\left(\phi \wedge \mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)\ne \mathrm{LSpan}\left(U\right)\left(\left\{Y\right\}\right)\right)\to X\underset{\dot{}}{+}Y\in E$$
35	25 34	pm2.61dane	$$⊢\phi \to X\underset{\dot{}}{+}Y\in E$$