Metamath Proof Explorer

Theorem lcfrlem17

Description: Lemma for lcfr . Condition needed more than once. (Contributed by NM, 11-Mar-2015)

Ref Expression
Hypotheses lcfrlem17.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
lcfrlem17.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
lcfrlem17.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
lcfrlem17.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
lcfrlem17.p ⊢ + = ( +g ‘ 𝑈 )
lcfrlem17.z ⊢ 0 = ( 0g ‘ 𝑈 )
lcfrlem17.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
lcfrlem17.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
lcfrlem17.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
lcfrlem17.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
lcfrlem17.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
lcfrlem17.ne ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
Assertion lcfrlem17 ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ ( 𝑉 ∖ { 0 } ) )

Proof

Step Hyp Ref Expression
1 lcfrlem17.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 lcfrlem17.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3 lcfrlem17.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 lcfrlem17.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
5 lcfrlem17.p ⊢ + = ( +g ‘ 𝑈 )
6 lcfrlem17.z ⊢ 0 = ( 0g ‘ 𝑈 )
7 lcfrlem17.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
8 lcfrlem17.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
9 lcfrlem17.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
10 lcfrlem17.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
11 lcfrlem17.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
12 lcfrlem17.ne ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
13 1 3 9 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
14 10 eldifad ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
15 11 eldifad ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
16 4 5 lmodvacl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 + 𝑌 ) ∈ 𝑉 )
17 13 14 15 16 syl3anc ⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ 𝑉 )
18 4 5 6 7 13 14 15 12 lmodindp1 ⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) ≠ 0 )
19 eldifsn ⊢ ( ( 𝑋 + 𝑌 ) ∈ ( 𝑉 ∖ { 0 } ) ↔ ( ( 𝑋 + 𝑌 ) ∈ 𝑉 ∧ ( 𝑋 + 𝑌 ) ≠ 0 ) )
20 17 18 19 sylanbrc ⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ ( 𝑉 ∖ { 0 } ) )