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

Proof

Step	Hyp	Ref	Expression
1		lspsntri.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lspsntri.a	⊢ + = ( +g ‘ 𝑊 )
3		lspsntri.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
4		lspsntri.p	⊢ ⊕ = ( LSSum ‘ 𝑊 )
5	1 2 3	lspvadd	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ⊆ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
6		df-pr	⊢ { 𝑋 , 𝑌 } = ( { 𝑋 } ∪ { 𝑌 } )
7	6	fveq2i	⊢ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) = ( 𝑁 ‘ ( { 𝑋 } ∪ { 𝑌 } ) )
8	5 7	sseqtrdi	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ⊆ ( 𝑁 ‘ ( { 𝑋 } ∪ { 𝑌 } ) ) )
9		simp1	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → 𝑊 ∈ LMod )
10		simp2	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → 𝑋 ∈ 𝑉 )
11	10	snssd	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → { 𝑋 } ⊆ 𝑉 )
12		simp3	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → 𝑌 ∈ 𝑉 )
13	12	snssd	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → { 𝑌 } ⊆ 𝑉 )
14	1 3 4	lsmsp2	⊢ ( ( 𝑊 ∈ LMod ∧ { 𝑋 } ⊆ 𝑉 ∧ { 𝑌 } ⊆ 𝑉 ) → ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) = ( 𝑁 ‘ ( { 𝑋 } ∪ { 𝑌 } ) ) )
15	9 11 13 14	syl3anc	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) = ( 𝑁 ‘ ( { 𝑋 } ∪ { 𝑌 } ) ) )
16	8 15	sseqtrrd	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ⊆ ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) )