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

Metamath Proof Explorer

Theorem lspsnsubn0

Description: Unequal singleton spans imply nonzero vector subtraction. (Contributed by NM, 19-Mar-2015)

Ref Expression
Hypotheses lspsnsubn0.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lspsnsubn0.o ⊢ 0 = ( 0g ‘ 𝑊 )
lspsnsubn0.m ⊢ − = ( -g ‘ 𝑊 )
lspsnsubn0.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
lspsnsubn0.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
lspsnsubn0.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
lspsnsubn0.e ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
Assertion lspsnsubn0 ( 𝜑 → ( 𝑋 − 𝑌 ) ≠ 0 )

Proof

Step Hyp Ref Expression
1 lspsnsubn0.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lspsnsubn0.o ⊢ 0 = ( 0g ‘ 𝑊 )
3 lspsnsubn0.m ⊢ − = ( -g ‘ 𝑊 )
4 lspsnsubn0.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
5 lspsnsubn0.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
6 lspsnsubn0.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
7 lspsnsubn0.e ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
8 1 2 3 lmodsubeq0 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( 𝑋 − 𝑌 ) = 0 ↔ 𝑋 = 𝑌 ) )
9 4 5 6 8 syl3anc ⊢ ( 𝜑 → ( ( 𝑋 − 𝑌 ) = 0 ↔ 𝑋 = 𝑌 ) )
10 sneq ⊢ ( 𝑋 = 𝑌 → { 𝑋 } = { 𝑌 } )
11 10 fveq2d ⊢ ( 𝑋 = 𝑌 → ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) )
12 9 11 biimtrdi ⊢ ( 𝜑 → ( ( 𝑋 − 𝑌 ) = 0 → ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) )
13 12 necon3d ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) → ( 𝑋 − 𝑌 ) ≠ 0 ) )
14 7 13 mpd ⊢ ( 𝜑 → ( 𝑋 − 𝑌 ) ≠ 0 )