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	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	lcfrlem7.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
	lcfrlem7.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	lcfrlem7.p	⊢ + = ( +g ‘ 𝑈 )
	lcfrlem7.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
	lcfrlem7.d	⊢ 𝐷 = ( LDual ‘ 𝑈 )
	lcfrlem7.q	⊢ 𝑄 = ( LSubSp ‘ 𝐷 )
	lcfrlem7.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	lcfrlem7.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑄 )
	lcfrlem7.e	⊢ 𝐸 = ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) )
	lcfrlem7.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐸 )
	lcfrlem7.z	⊢ 0 = ( 0g ‘ 𝑈 )
	lcfrlem7.y	⊢ ( 𝜑 → 𝑌 = 0 )
Assertion	lcfrlem7	⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ 𝐸 )

Proof

Step	Hyp	Ref	Expression
1		lcfrlem7.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		lcfrlem7.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3		lcfrlem7.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4		lcfrlem7.p	⊢ + = ( +g ‘ 𝑈 )
5		lcfrlem7.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
6		lcfrlem7.d	⊢ 𝐷 = ( LDual ‘ 𝑈 )
7		lcfrlem7.q	⊢ 𝑄 = ( LSubSp ‘ 𝐷 )
8		lcfrlem7.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9		lcfrlem7.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑄 )
10		lcfrlem7.e	⊢ 𝐸 = ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) )
11		lcfrlem7.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐸 )
12		lcfrlem7.z	⊢ 0 = ( 0g ‘ 𝑈 )
13		lcfrlem7.y	⊢ ( 𝜑 → 𝑌 = 0 )
14	13	oveq2d	⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) = ( 𝑋 + 0 ) )
15	1 3 8	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
16		eqid	⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
17	1 2 3 16 5 6 7 10 8 9 11	lcfrlem4	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝑈 ) )
18	16 4 12	lmod0vrid	⊢ ( ( 𝑈 ∈ LMod ∧ 𝑋 ∈ ( Base ‘ 𝑈 ) ) → ( 𝑋 + 0 ) = 𝑋 )
19	15 17 18	syl2anc	⊢ ( 𝜑 → ( 𝑋 + 0 ) = 𝑋 )
20	14 19	eqtrd	⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) = 𝑋 )
21	20 11	eqeltrd	⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ 𝐸 )