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

Metamath Proof Explorer

Theorem lspsntrim

Description: Triangle-type inequality for span of a singleton of vector difference. (Contributed by NM, 25-Apr-2014) (Revised by Mario Carneiro, 21-Jun-2014)

Ref Expression
Hypotheses lspsntrim.v 
|- V = ( Base ` W )
lspsntrim.s 
|- .- = ( -g ` W )
lspsntrim.p 
|- .(+) = ( LSSum ` W )
lspsntrim.n 
|- N = ( LSpan ` W )
Assertion lspsntrim 
|- ( ( W e. LMod /\ X e. V /\ Y e. V ) -> ( N ` { ( X .- Y ) } ) C_ ( ( N ` { X } ) .(+) ( N ` { Y } ) ) )

Proof

Step Hyp Ref Expression
1 lspsntrim.v 
 |-  V = ( Base ` W )
2 lspsntrim.s 
 |-  .- = ( -g ` W )
3 lspsntrim.p 
 |-  .(+) = ( LSSum ` W )
4 lspsntrim.n 
 |-  N = ( LSpan ` W )
5 eqid 
 |-  ( invg ` W ) = ( invg ` W )
6 1 5 lmodvnegcl 
 |-  ( ( W e. LMod /\ Y e. V ) -> ( ( invg ` W ) ` Y ) e. V )
7 6 3adant2 
 |-  ( ( W e. LMod /\ X e. V /\ Y e. V ) -> ( ( invg ` W ) ` Y ) e. V )
8 eqid 
 |-  ( +g ` W ) = ( +g ` W )
9 1 8 4 3 lspsntri 
 |-  ( ( W e. LMod /\ X e. V /\ ( ( invg ` W ) ` Y ) e. V ) -> ( N ` { ( X ( +g ` W ) ( ( invg ` W ) ` Y ) ) } ) C_ ( ( N ` { X } ) .(+) ( N ` { ( ( invg ` W ) ` Y ) } ) ) )
10 7 9 syld3an3 
 |-  ( ( W e. LMod /\ X e. V /\ Y e. V ) -> ( N ` { ( X ( +g ` W ) ( ( invg ` W ) ` Y ) ) } ) C_ ( ( N ` { X } ) .(+) ( N ` { ( ( invg ` W ) ` Y ) } ) ) )
11 1 8 5 2 grpsubval 
 |-  ( ( X e. V /\ Y e. V ) -> ( X .- Y ) = ( X ( +g ` W ) ( ( invg ` W ) ` Y ) ) )
12 11 sneqd 
 |-  ( ( X e. V /\ Y e. V ) -> { ( X .- Y ) } = { ( X ( +g ` W ) ( ( invg ` W ) ` Y ) ) } )
13 12 fveq2d 
 |-  ( ( X e. V /\ Y e. V ) -> ( N ` { ( X .- Y ) } ) = ( N ` { ( X ( +g ` W ) ( ( invg ` W ) ` Y ) ) } ) )
14 13 3adant1 
 |-  ( ( W e. LMod /\ X e. V /\ Y e. V ) -> ( N ` { ( X .- Y ) } ) = ( N ` { ( X ( +g ` W ) ( ( invg ` W ) ` Y ) ) } ) )
15 1 5 4 lspsnneg 
 |-  ( ( W e. LMod /\ Y e. V ) -> ( N ` { ( ( invg ` W ) ` Y ) } ) = ( N ` { Y } ) )
16 15 3adant2 
 |-  ( ( W e. LMod /\ X e. V /\ Y e. V ) -> ( N ` { ( ( invg ` W ) ` Y ) } ) = ( N ` { Y } ) )
17 16 eqcomd 
 |-  ( ( W e. LMod /\ X e. V /\ Y e. V ) -> ( N ` { Y } ) = ( N ` { ( ( invg ` W ) ` Y ) } ) )
18 17 oveq2d 
 |-  ( ( W e. LMod /\ X e. V /\ Y e. V ) -> ( ( N ` { X } ) .(+) ( N ` { Y } ) ) = ( ( N ` { X } ) .(+) ( N ` { ( ( invg ` W ) ` Y ) } ) ) )
19 10 14 18 3sstr4d 
 |-  ( ( W e. LMod /\ X e. V /\ Y e. V ) -> ( N ` { ( X .- Y ) } ) C_ ( ( N ` { X } ) .(+) ( N ` { Y } ) ) )