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 } ) ) )