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

Metamath Proof Explorer

Theorem lssvancl1

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. TODO: notice similarity to lspindp3 . Can it be used along with lspsnne1 , lspsnne2 to shorten this proof? (Contributed by NM, 14-May-2015)

Ref Expression
Hypotheses lssvancl.v ⊢ V = Base W
lssvancl.p ⊢ + ˙ = + W
lssvancl.s ⊢ S = LSubSp ⁡ W
lssvancl.w ⊢ φ → W ∈ LMod
lssvancl.u ⊢ φ → U ∈ S
lssvancl.x ⊢ φ → X ∈ U
lssvancl.y ⊢ φ → Y ∈ V
lssvancl.n ⊢ φ → ¬ Y ∈ U
Assertion lssvancl1 ⊢ φ → ¬ X + ˙ Y ∈ U

Proof

Step Hyp Ref Expression
1 lssvancl.v ⊢ V = Base W
2 lssvancl.p ⊢ + ˙ = + W
3 lssvancl.s ⊢ S = LSubSp ⁡ W
4 lssvancl.w ⊢ φ → W ∈ LMod
5 lssvancl.u ⊢ φ → U ∈ S
6 lssvancl.x ⊢ φ → X ∈ U
7 lssvancl.y ⊢ φ → Y ∈ V
8 lssvancl.n ⊢ φ → ¬ Y ∈ U
9 lmodabl ⊢ W ∈ LMod → W ∈ Abel
10 4 9 syl ⊢ φ → W ∈ Abel
11 1 3 lssel ⊢ U ∈ S ∧ X ∈ U → X ∈ V
12 5 6 11 syl2anc ⊢ φ → X ∈ V
13 eqid ⊢ - W = - W
14 1 2 13 ablpncan2 ⊢ W ∈ Abel ∧ X ∈ V ∧ Y ∈ V → X + ˙ Y - W X = Y
15 10 12 7 14 syl3anc ⊢ φ → X + ˙ Y - W X = Y
16 15 adantr ⊢ φ ∧ X + ˙ Y ∈ U → X + ˙ Y - W X = Y
17 4 adantr ⊢ φ ∧ X + ˙ Y ∈ U → W ∈ LMod
18 5 adantr ⊢ φ ∧ X + ˙ Y ∈ U → U ∈ S
19 simpr ⊢ φ ∧ X + ˙ Y ∈ U → X + ˙ Y ∈ U
20 6 adantr ⊢ φ ∧ X + ˙ Y ∈ U → X ∈ U
21 13 3 lssvsubcl ⊢ W ∈ LMod ∧ U ∈ S ∧ X + ˙ Y ∈ U ∧ X ∈ U → X + ˙ Y - W X ∈ U
22 17 18 19 20 21 syl22anc ⊢ φ ∧ X + ˙ Y ∈ U → X + ˙ Y - W X ∈ U
23 16 22 eqeltrrd ⊢ φ ∧ X + ˙ Y ∈ U → Y ∈ U
24 8 23 mtand ⊢ φ → ¬ X + ˙ Y ∈ U