Theorem lcfrlem27

Description: Lemma for lcfr . Special case of lcfrlem37 when ( ( JY )I ) is zero. (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)$$
	lcfrlem22.b	$$⊢B=N\left(\left\{X,Y\right\}\right)\cap \underset{\dot{}}{\perp }\left(\left\{X\underset{\dot{}}{+}Y\right\}\right)$$
	lcfrlem24.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
	lcfrlem24.s	$$⊢S=\mathrm{Scalar}\left(U\right)$$
	lcfrlem24.q	$$⊢Q=0_S$$
	lcfrlem24.r	$$⊢R={\mathrm{Base}}_S$$
	lcfrlem24.j	$$⊢J=\left(x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)⟼\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\right)\right)\right)$$
	lcfrlem24.ib	$$⊢\phi \to I\in B$$
	lcfrlem24.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
	lcfrlem25.d	$$⊢D=\mathrm{LDual}\left(U\right)$$
	lcfrlem25.jz	$$⊢\phi \to J\left(Y\right)\left(I\right)=Q$$
	lcfrlem25.in	$$⊢\phi \to I\ne \underset{\dot{}}{0}$$
	lcfrlem27.g	$$⊢\phi \to G\in \mathrm{LSubSp}\left(D\right)$$
	lcfrlem27.gs	$$⊢\phi \to G\subseteq \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\}$$
	lcfrlem27.e	$$⊢E=\bigcup _{g\in G}\underset{\dot{}}{\perp }\left(L\left(g\right)\right)$$
	lcfrlem27.xe	$$⊢\phi \to X\in E$$
	lcfrlem27.ye	$$⊢\phi \to Y\in E$$
Assertion	lcfrlem27	$$⊢\phi \to X\underset{\dot{}}{+}Y\in E$$

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		lcfrlem24.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
15		lcfrlem24.s	$$⊢S=\mathrm{Scalar}\left(U\right)$$
16		lcfrlem24.q	$$⊢Q=0_S$$
17		lcfrlem24.r	$$⊢R={\mathrm{Base}}_S$$
18		lcfrlem24.j	$$⊢J=\left(x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)⟼\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\right)\right)\right)$$
19		lcfrlem24.ib	$$⊢\phi \to I\in B$$
20		lcfrlem24.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
21		lcfrlem25.d	$$⊢D=\mathrm{LDual}\left(U\right)$$
22		lcfrlem25.jz	$$⊢\phi \to J\left(Y\right)\left(I\right)=Q$$
23		lcfrlem25.in	$$⊢\phi \to I\ne \underset{\dot{}}{0}$$
24		lcfrlem27.g	$$⊢\phi \to G\in \mathrm{LSubSp}\left(D\right)$$
25		lcfrlem27.gs	$$⊢\phi \to G\subseteq \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\}$$
26		lcfrlem27.e	$$⊢E=\bigcup _{g\in G}\underset{\dot{}}{\perp }\left(L\left(g\right)\right)$$
27		lcfrlem27.xe	$$⊢\phi \to X\in E$$
28		lcfrlem27.ye	$$⊢\phi \to Y\in E$$
29		eqid	$$⊢\mathrm{LFnl}\left(U\right)=\mathrm{LFnl}\left(U\right)$$
30		eqid	$$⊢0_D=0_D$$
31		eqid	$$⊢\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\}=\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\}$$
32		eqid	$$⊢\mathrm{LSubSp}\left(D\right)=\mathrm{LSubSp}\left(D\right)$$
33		eldifsni	$$⊢Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\to Y\ne \underset{\dot{}}{0}$$
34	11 33	syl	$$⊢\phi \to Y\ne \underset{\dot{}}{0}$$
35		eldifsn	$$⊢Y\in \left(E\setminus \left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow \left(Y\in E\wedge Y\ne \underset{\dot{}}{0}\right)$$
36	28 34 35	sylanbrc	$$⊢\phi \to Y\in \left(E\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
37	1 2 3 4 5 14 15 17 6 29 20 21 30 31 18 9 32 24 25 26 36	lcfrlem16	$$⊢\phi \to J\left(Y\right)\in G$$
38	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23	lcfrlem26	$$⊢\phi \to X\underset{\dot{}}{+}Y\in \underset{\dot{}}{\perp }\left(L\left(J\left(Y\right)\right)\right)$$
39		2fveq3	$$⊢g=J\left(Y\right)\to \underset{\dot{}}{\perp }\left(L\left(g\right)\right)=\underset{\dot{}}{\perp }\left(L\left(J\left(Y\right)\right)\right)$$
40	39	eleq2d	$$⊢g=J\left(Y\right)\to \left(X\underset{\dot{}}{+}Y\in \underset{\dot{}}{\perp }\left(L\left(g\right)\right)\leftrightarrow X\underset{\dot{}}{+}Y\in \underset{\dot{}}{\perp }\left(L\left(J\left(Y\right)\right)\right)\right)$$
41	40	rspcev	$$⊢\left(J\left(Y\right)\in G\wedge X\underset{\dot{}}{+}Y\in \underset{\dot{}}{\perp }\left(L\left(J\left(Y\right)\right)\right)\right)\to \exists g\in GX\underset{\dot{}}{+}Y\in \underset{\dot{}}{\perp }\left(L\left(g\right)\right)$$
42	37 38 41	syl2anc	$$⊢\phi \to \exists g\in GX\underset{\dot{}}{+}Y\in \underset{\dot{}}{\perp }\left(L\left(g\right)\right)$$
43		eliun	$$⊢X\underset{\dot{}}{+}Y\in \bigcup _{g\in G}\underset{\dot{}}{\perp }\left(L\left(g\right)\right)\leftrightarrow \exists g\in GX\underset{\dot{}}{+}Y\in \underset{\dot{}}{\perp }\left(L\left(g\right)\right)$$
44	42 43	sylibr	$$⊢\phi \to X\underset{\dot{}}{+}Y\in \bigcup _{g\in G}\underset{\dot{}}{\perp }\left(L\left(g\right)\right)$$
45	44 26	eleqtrrdi	$$⊢\phi \to X\underset{\dot{}}{+}Y\in E$$