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	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lspsntrim.s	⊢ − = ( -g ‘ 𝑊 )
	lspsntrim.p	⊢ ⊕ = ( LSSum ‘ 𝑊 )
	lspsntrim.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
Assertion	lspsntrim	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ⊆ ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		lspsntrim.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lspsntrim.s	⊢ − = ( -g ‘ 𝑊 )
3		lspsntrim.p	⊢ ⊕ = ( LSSum ‘ 𝑊 )
4		lspsntrim.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
5		eqid	⊢ ( invg ‘ 𝑊 ) = ( invg ‘ 𝑊 )
6	1 5	lmodvnegcl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) → ( ( invg ‘ 𝑊 ) ‘ 𝑌 ) ∈ 𝑉 )
7	6	3adant2	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( invg ‘ 𝑊 ) ‘ 𝑌 ) ∈ 𝑉 )
8		eqid	⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
9	1 8 4 3	lspsntri	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑌 ) ∈ 𝑉 ) → ( 𝑁 ‘ { ( 𝑋 ( +g ‘ 𝑊 ) ( ( invg ‘ 𝑊 ) ‘ 𝑌 ) ) } ) ⊆ ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { ( ( invg ‘ 𝑊 ) ‘ 𝑌 ) } ) ) )
10	7 9	syld3an3	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ { ( 𝑋 ( +g ‘ 𝑊 ) ( ( invg ‘ 𝑊 ) ‘ 𝑌 ) ) } ) ⊆ ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { ( ( invg ‘ 𝑊 ) ‘ 𝑌 ) } ) ) )
11	1 8 5 2	grpsubval	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 − 𝑌 ) = ( 𝑋 ( +g ‘ 𝑊 ) ( ( invg ‘ 𝑊 ) ‘ 𝑌 ) ) )
12	11	sneqd	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → { ( 𝑋 − 𝑌 ) } = { ( 𝑋 ( +g ‘ 𝑊 ) ( ( invg ‘ 𝑊 ) ‘ 𝑌 ) ) } )
13	12	fveq2d	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) = ( 𝑁 ‘ { ( 𝑋 ( +g ‘ 𝑊 ) ( ( invg ‘ 𝑊 ) ‘ 𝑌 ) ) } ) )
14	13	3adant1	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) = ( 𝑁 ‘ { ( 𝑋 ( +g ‘ 𝑊 ) ( ( invg ‘ 𝑊 ) ‘ 𝑌 ) ) } ) )
15	1 5 4	lspsnneg	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ { ( ( invg ‘ 𝑊 ) ‘ 𝑌 ) } ) = ( 𝑁 ‘ { 𝑌 } ) )
16	15	3adant2	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ { ( ( invg ‘ 𝑊 ) ‘ 𝑌 ) } ) = ( 𝑁 ‘ { 𝑌 } ) )
17	16	eqcomd	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑌 } ) = ( 𝑁 ‘ { ( ( invg ‘ 𝑊 ) ‘ 𝑌 ) } ) )
18	17	oveq2d	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) = ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { ( ( invg ‘ 𝑊 ) ‘ 𝑌 ) } ) ) )
19	10 14 18	3sstr4d	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ⊆ ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) )