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