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

Metamath Proof Explorer

Theorem lspsntri

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

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

Proof

Step Hyp Ref Expression
1 lspsntri.v 
 |-  V = ( Base ` W )
2 lspsntri.a 
 |-  .+ = ( +g ` W )
3 lspsntri.n 
 |-  N = ( LSpan ` W )
4 lspsntri.p 
 |-  .(+) = ( LSSum ` W )
5 1 2 3 lspvadd 
 |-  ( ( W e. LMod /\ X e. V /\ Y e. V ) -> ( N ` { ( X .+ Y ) } ) C_ ( N ` { X , Y } ) )
6 df-pr 
 |-  { X , Y } = ( { X } u. { Y } )
7 6 fveq2i 
 |-  ( N ` { X , Y } ) = ( N ` ( { X } u. { Y } ) )
8 5 7 sseqtrdi 
 |-  ( ( W e. LMod /\ X e. V /\ Y e. V ) -> ( N ` { ( X .+ Y ) } ) C_ ( N ` ( { X } u. { Y } ) ) )
9 simp1 
 |-  ( ( W e. LMod /\ X e. V /\ Y e. V ) -> W e. LMod )
10 simp2 
 |-  ( ( W e. LMod /\ X e. V /\ Y e. V ) -> X e. V )
11 10 snssd 
 |-  ( ( W e. LMod /\ X e. V /\ Y e. V ) -> { X } C_ V )
12 simp3 
 |-  ( ( W e. LMod /\ X e. V /\ Y e. V ) -> Y e. V )
13 12 snssd 
 |-  ( ( W e. LMod /\ X e. V /\ Y e. V ) -> { Y } C_ V )
14 1 3 4 lsmsp2 
 |-  ( ( W e. LMod /\ { X } C_ V /\ { Y } C_ V ) -> ( ( N ` { X } ) .(+) ( N ` { Y } ) ) = ( N ` ( { X } u. { Y } ) ) )
15 9 11 13 14 syl3anc 
 |-  ( ( W e. LMod /\ X e. V /\ Y e. V ) -> ( ( N ` { X } ) .(+) ( N ` { Y } ) ) = ( N ` ( { X } u. { Y } ) ) )
16 8 15 sseqtrrd 
 |-  ( ( W e. LMod /\ X e. V /\ Y e. V ) -> ( N ` { ( X .+ Y ) } ) C_ ( ( N ` { X } ) .(+) ( N ` { Y } ) ) )