This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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