Theorem lcfrlem7

Description: Lemma for lcfr . Closure of vector sum when one vector is zero. TODO: share hypotheses with others. (Contributed by NM, 11-Mar-2015)

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

Proof

Step	Hyp	Ref	Expression
1		lcfrlem7.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		lcfrlem7.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
3		lcfrlem7.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
4		lcfrlem7.p	$$⊢\underset{\dot{}}{+}={+}_U$$
5		lcfrlem7.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
6		lcfrlem7.d	$$⊢D=\mathrm{LDual}\left(U\right)$$
7		lcfrlem7.q	$$⊢Q=\mathrm{LSubSp}\left(D\right)$$
8		lcfrlem7.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
9		lcfrlem7.g	$$⊢\phi \to G\in Q$$
10		lcfrlem7.e	$$⊢E=\bigcup _{g\in G}\underset{\dot{}}{\perp }\left(L\left(g\right)\right)$$
11		lcfrlem7.x	$$⊢\phi \to X\in E$$
12		lcfrlem7.z	$$⊢\underset{\dot{}}{0}=0_U$$
13		lcfrlem7.y	$$⊢\phi \to Y=\underset{\dot{}}{0}$$
14	13	oveq2d	$$⊢\phi \to X\underset{\dot{}}{+}Y=X\underset{\dot{}}{+}\underset{\dot{}}{0}$$
15	1 3 8	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
16		eqid	$$⊢{\mathrm{Base}}_U={\mathrm{Base}}_U$$
17	1 2 3 16 5 6 7 10 8 9 11	lcfrlem4	$$⊢\phi \to X\in {\mathrm{Base}}_U$$
18	16 4 12	lmod0vrid	$$⊢\left(U\in \mathrm{LMod}\wedge X\in {\mathrm{Base}}_U\right)\to X\underset{\dot{}}{+}\underset{\dot{}}{0}=X$$
19	15 17 18	syl2anc	$$⊢\phi \to X\underset{\dot{}}{+}\underset{\dot{}}{0}=X$$
20	14 19	eqtrd	$$⊢\phi \to X\underset{\dot{}}{+}Y=X$$
21	20 11	eqeltrd	$$⊢\phi \to X\underset{\dot{}}{+}Y\in E$$