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

Metamath Proof Explorer

Theorem lspindp4

Description: (Partial) independence of 3 vectors is preserved by vector sum. (Contributed by NM, 26-Apr-2015)

Ref Expression
Hypotheses lspindp3.v ⊢ V = Base W
lspindp3.p ⊢ + ˙ = + W
lspindp4.n ⊢ N = LSpan ⁡ W
lspindp4.w ⊢ φ → W ∈ LMod
lspindp4.x ⊢ φ → X ∈ V
lspindp4.y ⊢ φ → Y ∈ V
lspindp4.z ⊢ φ → Z ∈ V
lspindp4.e ⊢ φ → ¬ Z ∈ N ⁡ X Y
Assertion lspindp4 ⊢ φ → ¬ Z ∈ N ⁡ X X + ˙ Y

Proof

Step Hyp Ref Expression
1 lspindp3.v ⊢ V = Base W
2 lspindp3.p ⊢ + ˙ = + W
3 lspindp4.n ⊢ N = LSpan ⁡ W
4 lspindp4.w ⊢ φ → W ∈ LMod
5 lspindp4.x ⊢ φ → X ∈ V
6 lspindp4.y ⊢ φ → Y ∈ V
7 lspindp4.z ⊢ φ → Z ∈ V
8 lspindp4.e ⊢ φ → ¬ Z ∈ N ⁡ X Y
9 1 2 3 4 5 6 lspprabs ⊢ φ → N ⁡ X X + ˙ Y = N ⁡ X Y
10 8 9 neleqtrrd ⊢ φ → ¬ Z ∈ N ⁡ X X + ˙ Y