Theorem lcfrlem39

Description: Lemma for lcfr . Eliminate J . (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}$$
	lcfrlem38.sp	$$⊢N=\mathrm{LSpan}\left(U\right)$$
	lcfrlem38.ne	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)$$
	lcfrlem38.b	$$⊢B=N\left(\left\{X,Y\right\}\right)\cap \underset{\dot{}}{\perp }\left(\left\{X\underset{\dot{}}{+}Y\right\}\right)$$
	lcfrlem38.i	$$⊢\phi \to I\in B$$
	lcfrlem38.n	$$⊢\phi \to I\ne \underset{\dot{}}{0}$$
Assertion	lcfrlem39	$$⊢\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		lcfrlem38.sp	$$⊢N=\mathrm{LSpan}\left(U\right)$$
20		lcfrlem38.ne	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)$$
21		lcfrlem38.b	$$⊢B=N\left(\left\{X,Y\right\}\right)\cap \underset{\dot{}}{\perp }\left(\left\{X\underset{\dot{}}{+}Y\right\}\right)$$
22		lcfrlem38.i	$$⊢\phi \to I\in B$$
23		lcfrlem38.n	$$⊢\phi \to I\ne \underset{\dot{}}{0}$$
24		eqid	$$⊢{\mathrm{Base}}_U={\mathrm{Base}}_U$$
25		eqid	$$⊢{\cdot }_U={\cdot }_U$$
26		eqid	$$⊢\mathrm{Scalar}\left(U\right)=\mathrm{Scalar}\left(U\right)$$
27		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(U\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(U\right)}$$
28		oveq1	$$⊢j=k\to j{\cdot }_{U}x=k{\cdot }_{U}x$$
29	28	oveq2d	$$⊢j=k\to w\underset{\dot{}}{+}\left(j{\cdot }_{U}x\right)=w\underset{\dot{}}{+}\left(k{\cdot }_{U}x\right)$$
30	29	eqeq2d	$$⊢j=k\to \left(v=w\underset{\dot{}}{+}\left(j{\cdot }_{U}x\right)\leftrightarrow v=w\underset{\dot{}}{+}\left(k{\cdot }_{U}x\right)\right)$$
31	30	rexbidv	$$⊢j=k\to \left(\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(j{\cdot }_{U}x\right)\leftrightarrow \exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k{\cdot }_{U}x\right)\right)$$
32	31	cbvriotavw	$$⊢\left(\iota j\in {\mathrm{Base}}_{\mathrm{Scalar}\left(U\right)}|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(j{\cdot }_{U}x\right)\right)=\left(\iota k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(U\right)}|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k{\cdot }_{U}x\right)\right)$$
33	32	mpteq2i	$$⊢\left(v\in {\mathrm{Base}}_U⟼\left(\iota j\in {\mathrm{Base}}_{\mathrm{Scalar}\left(U\right)}|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(j{\cdot }_{U}x\right)\right)\right)=\left(v\in {\mathrm{Base}}_U⟼\left(\iota k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(U\right)}|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k{\cdot }_{U}x\right)\right)\right)$$
34	33	mpteq2i	$$⊢\left(x\in \left({\mathrm{Base}}_U\setminus \left\{\underset{\dot{}}{0}\right\}\right)⟼\left(v\in {\mathrm{Base}}_U⟼\left(\iota j\in {\mathrm{Base}}_{\mathrm{Scalar}\left(U\right)}|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(j{\cdot }_{U}x\right)\right)\right)\right)=\left(x\in \left({\mathrm{Base}}_U\setminus \left\{\underset{\dot{}}{0}\right\}\right)⟼\left(v\in {\mathrm{Base}}_U⟼\left(\iota k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(U\right)}|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k{\cdot }_{U}x\right)\right)\right)\right)$$
35	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 34	lcfrlem38	$$⊢\phi \to X\underset{\dot{}}{+}Y\in E$$