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

Metamath Proof Explorer

Theorem lspsnnecom

Description: Swap two vectors with different spans. (Contributed by NM, 20-May-2015)

Ref Expression
Hypotheses lspsnnecom.v ⊢ V = Base W
lspsnnecom.o ⊢ 0 ˙ = 0 W
lspsnnecom.n ⊢ N = LSpan ⁡ W
lspsnnecom.w ⊢ φ → W ∈ LVec
lspsnnecom.x ⊢ φ → X ∈ V
lspsnnecom.y ⊢ φ → Y ∈ V ∖ 0 ˙
lspsnnecom.e ⊢ φ → ¬ X ∈ N ⁡ Y
Assertion lspsnnecom ⊢ φ → ¬ Y ∈ N ⁡ X

Proof

Step Hyp Ref Expression
1 lspsnnecom.v ⊢ V = Base W
2 lspsnnecom.o ⊢ 0 ˙ = 0 W
3 lspsnnecom.n ⊢ N = LSpan ⁡ W
4 lspsnnecom.w ⊢ φ → W ∈ LVec
5 lspsnnecom.x ⊢ φ → X ∈ V
6 lspsnnecom.y ⊢ φ → Y ∈ V ∖ 0 ˙
7 lspsnnecom.e ⊢ φ → ¬ X ∈ N ⁡ Y
8 lveclmod ⊢ W ∈ LVec → W ∈ LMod
9 4 8 syl ⊢ φ → W ∈ LMod
10 6 eldifad ⊢ φ → Y ∈ V
11 1 3 9 5 10 7 lspsnne2 ⊢ φ → N ⁡ X ≠ N ⁡ Y
12 11 necomd ⊢ φ → N ⁡ Y ≠ N ⁡ X
13 1 2 3 4 6 5 12 lspsnne1 ⊢ φ → ¬ Y ∈ N ⁡ X