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 ⊢ 𝑉 = ( 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 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ⊆ ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) )