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

Metamath Proof Explorer

Theorem lspsnne1

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

Ref Expression
Hypotheses lspsnne1.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lspsnne1.o ⊢ 0 = ( 0g ‘ 𝑊 )
lspsnne1.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
lspsnne1.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
lspsnne1.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
lspsnne1.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
lspsnne1.e ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
Assertion lspsnne1 ( 𝜑 → ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) )

Proof

Step Hyp Ref Expression
1 lspsnne1.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lspsnne1.o ⊢ 0 = ( 0g ‘ 𝑊 )
3 lspsnne1.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
4 lspsnne1.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
5 lspsnne1.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
6 lspsnne1.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
7 lspsnne1.e ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
8 eqid ⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
9 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
10 4 9 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
11 1 8 3 lspsncl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑊 ) )
12 10 6 11 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑊 ) )
13 5 eldifad ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
14 1 8 3 10 12 13 ellspsn5b ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) ↔ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑁 ‘ { 𝑌 } ) ) )
15 14 notbid ⊢ ( 𝜑 → ( ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) ↔ ¬ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑁 ‘ { 𝑌 } ) ) )
16 1 2 3 4 5 6 lspsncmp ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑁 ‘ { 𝑌 } ) ↔ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) )
17 16 necon3bbid ⊢ ( 𝜑 → ( ¬ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑁 ‘ { 𝑌 } ) ↔ ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) ) )
18 15 17 bitrd ⊢ ( 𝜑 → ( ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) ↔ ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) ) )
19 7 18 mpbird ⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) )