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 
|- V = ( Base ` W )
lspsnsubn0.o 
|- .0. = ( 0g ` W )
lspsnsubn0.m 
|- .- = ( -g ` W )
lspsnsubn0.w 
|- ( ph -> W e. LMod )
lspsnsubn0.x 
|- ( ph -> X e. V )
lspsnsubn0.y 
|- ( ph -> Y e. V )
lspsnsubn0.e 
|- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )
Assertion lspsnsubn0 
|- ( ph -> ( X .- Y ) =/= .0. )

Proof

Step Hyp Ref Expression
1 lspsnsubn0.v 
 |-  V = ( Base ` W )
2 lspsnsubn0.o 
 |-  .0. = ( 0g ` W )
3 lspsnsubn0.m 
 |-  .- = ( -g ` W )
4 lspsnsubn0.w 
 |-  ( ph -> W e. LMod )
5 lspsnsubn0.x 
 |-  ( ph -> X e. V )
6 lspsnsubn0.y 
 |-  ( ph -> Y e. V )
7 lspsnsubn0.e 
 |-  ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )
8 1 2 3 lmodsubeq0 
 |-  ( ( W e. LMod /\ X e. V /\ Y e. V ) -> ( ( X .- Y ) = .0. <-> X = Y ) )
9 4 5 6 8 syl3anc 
 |-  ( ph -> ( ( X .- Y ) = .0. <-> X = Y ) )
10 sneq 
 |-  ( X = Y -> { X } = { Y } )
11 10 fveq2d 
 |-  ( X = Y -> ( N ` { X } ) = ( N ` { Y } ) )
12 9 11 biimtrdi 
 |-  ( ph -> ( ( X .- Y ) = .0. -> ( N ` { X } ) = ( N ` { Y } ) ) )
13 12 necon3d 
 |-  ( ph -> ( ( N ` { X } ) =/= ( N ` { Y } ) -> ( X .- Y ) =/= .0. ) )
14 7 13 mpd 
 |-  ( ph -> ( X .- Y ) =/= .0. )