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

Metamath Proof Explorer

Theorem lspsnsub

Description: Swapping subtraction order does not change the span of a singleton. (Contributed by NM, 4-Apr-2015)

Ref Expression
Hypotheses lspsnsub.v 
|- V = ( Base ` W )
lspsnsub.s 
|- .- = ( -g ` W )
lspsnsub.n 
|- N = ( LSpan ` W )
lspsnsub.w 
|- ( ph -> W e. LMod )
lspsnsub.x 
|- ( ph -> X e. V )
lspsnsub.y 
|- ( ph -> Y e. V )
Assertion lspsnsub 
|- ( ph -> ( N ` { ( X .- Y ) } ) = ( N ` { ( Y .- X ) } ) )

Proof

Step Hyp Ref Expression
1 lspsnsub.v 
 |-  V = ( Base ` W )
2 lspsnsub.s 
 |-  .- = ( -g ` W )
3 lspsnsub.n 
 |-  N = ( LSpan ` W )
4 lspsnsub.w 
 |-  ( ph -> W e. LMod )
5 lspsnsub.x 
 |-  ( ph -> X e. V )
6 lspsnsub.y 
 |-  ( ph -> Y e. V )
7 1 2 lmodvsubcl 
 |-  ( ( W e. LMod /\ X e. V /\ Y e. V ) -> ( X .- Y ) e. V )
8 4 5 6 7 syl3anc 
 |-  ( ph -> ( X .- Y ) e. V )
9 eqid 
 |-  ( invg ` W ) = ( invg ` W )
10 1 9 3 lspsnneg 
 |-  ( ( W e. LMod /\ ( X .- Y ) e. V ) -> ( N ` { ( ( invg ` W ) ` ( X .- Y ) ) } ) = ( N ` { ( X .- Y ) } ) )
11 4 8 10 syl2anc 
 |-  ( ph -> ( N ` { ( ( invg ` W ) ` ( X .- Y ) ) } ) = ( N ` { ( X .- Y ) } ) )
12 lmodgrp 
 |-  ( W e. LMod -> W e. Grp )
13 4 12 syl 
 |-  ( ph -> W e. Grp )
14 1 2 9 grpinvsub 
 |-  ( ( W e. Grp /\ X e. V /\ Y e. V ) -> ( ( invg ` W ) ` ( X .- Y ) ) = ( Y .- X ) )
15 13 5 6 14 syl3anc 
 |-  ( ph -> ( ( invg ` W ) ` ( X .- Y ) ) = ( Y .- X ) )
16 15 sneqd 
 |-  ( ph -> { ( ( invg ` W ) ` ( X .- Y ) ) } = { ( Y .- X ) } )
17 16 fveq2d 
 |-  ( ph -> ( N ` { ( ( invg ` W ) ` ( X .- Y ) ) } ) = ( N ` { ( Y .- X ) } ) )
18 11 17 eqtr3d 
 |-  ( ph -> ( N ` { ( X .- Y ) } ) = ( N ` { ( Y .- X ) } ) )