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

Metamath Proof Explorer

Theorem lspsnne2

Description: Two ways to express that vectors have different spans. (Contributed by NM, 20-May-2015)

Ref Expression
Hypotheses lspsnne2.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lspsnne2.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
lspsnne2.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
lspsnne2.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
lspsnne2.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
lspsnne2.e ⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) )
Assertion lspsnne2 ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )

Proof

Step Hyp Ref Expression
1 lspsnne2.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lspsnne2.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
3 lspsnne2.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
4 lspsnne2.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
5 lspsnne2.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
6 lspsnne2.e ⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) )
7 eqimss ⊢ ( ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) → ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑁 ‘ { 𝑌 } ) )
8 eqid ⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
9 1 8 2 lspsncl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑊 ) )
10 3 5 9 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑊 ) )
11 1 8 2 3 10 4 ellspsn5b ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) ↔ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑁 ‘ { 𝑌 } ) ) )
12 7 11 imbitrrid ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) → 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) ) )
13 12 necon3bd ⊢ ( 𝜑 → ( ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) ) )
14 6 13 mpd ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )