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 ⊢ 𝑉 = ( Base ‘ 𝑊 )
lspsnnecom.o ⊢ 0 = ( 0g ‘ 𝑊 )
lspsnnecom.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
lspsnnecom.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
lspsnnecom.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
lspsnnecom.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
lspsnnecom.e ⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) )
Assertion lspsnnecom ( 𝜑 → ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑋 } ) )

Proof

Step Hyp Ref Expression
1 lspsnnecom.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lspsnnecom.o ⊢ 0 = ( 0g ‘ 𝑊 )
3 lspsnnecom.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
4 lspsnnecom.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
5 lspsnnecom.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
6 lspsnnecom.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
7 lspsnnecom.e ⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) )
8 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
9 4 8 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
10 6 eldifad ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
11 1 3 9 5 10 7 lspsnne2 ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
12 11 necomd ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ≠ ( 𝑁 ‘ { 𝑋 } ) )
13 1 2 3 4 6 5 12 lspsnne1 ⊢ ( 𝜑 → ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑋 } ) )