This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lssvancl2

Description: Non-closure: if one vector belongs to a subspace but another does not, their sum does not belong. Useful for obtaining a new vector not in a subspace. (Contributed by NM, 20-May-2015)

Ref Expression
Hypotheses lssvancl.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lssvancl.p ⊢ + = ( +g ‘ 𝑊 )
lssvancl.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
lssvancl.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
lssvancl.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
lssvancl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
lssvancl.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
lssvancl.n ⊢ ( 𝜑 → ¬ 𝑌 ∈ 𝑈 )
Assertion lssvancl2 ( 𝜑 → ¬ ( 𝑌 + 𝑋 ) ∈ 𝑈 )

Proof

Step Hyp Ref Expression
1 lssvancl.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lssvancl.p ⊢ + = ( +g ‘ 𝑊 )
3 lssvancl.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
4 lssvancl.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
5 lssvancl.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
6 lssvancl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
7 lssvancl.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
8 lssvancl.n ⊢ ( 𝜑 → ¬ 𝑌 ∈ 𝑈 )
9 1 3 lssel ⊢ ( ( 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑈 ) → 𝑋 ∈ 𝑉 )
10 5 6 9 syl2anc ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
11 1 2 lmodcom ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) )
12 4 10 7 11 syl3anc ⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) )
13 1 2 3 4 5 6 7 8 lssvancl1 ⊢ ( 𝜑 → ¬ ( 𝑋 + 𝑌 ) ∈ 𝑈 )
14 12 13 eqneltrrd ⊢ ( 𝜑 → ¬ ( 𝑌 + 𝑋 ) ∈ 𝑈 )