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

Metamath Proof Explorer

Theorem lspvadd

Description: The span of a vector sum is included in the span of its arguments. (Contributed by NM, 22-Feb-2014) (Proof shortened by Mario Carneiro, 21-Jun-2014)

Ref Expression
Hypotheses lspvadd.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lspvadd.a ⊢ + = ( +g ‘ 𝑊 )
lspvadd.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
Assertion lspvadd ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ⊆ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )

Proof

Step Hyp Ref Expression
1 lspvadd.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lspvadd.a ⊢ + = ( +g ‘ 𝑊 )
3 lspvadd.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
4 eqid ⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
5 simp1 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → 𝑊 ∈ LMod )
6 prssi ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → { 𝑋 , 𝑌 } ⊆ 𝑉 )
7 6 3adant1 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → { 𝑋 , 𝑌 } ⊆ 𝑉 )
8 1 4 3 lspcl ⊢ ( ( 𝑊 ∈ LMod ∧ { 𝑋 , 𝑌 } ⊆ 𝑉 ) → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∈ ( LSubSp ‘ 𝑊 ) )
9 5 7 8 syl2anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∈ ( LSubSp ‘ 𝑊 ) )
10 1 3 lspssid ⊢ ( ( 𝑊 ∈ LMod ∧ { 𝑋 , 𝑌 } ⊆ 𝑉 ) → { 𝑋 , 𝑌 } ⊆ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
11 5 7 10 syl2anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → { 𝑋 , 𝑌 } ⊆ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
12 prssg ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( 𝑋 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ↔ { 𝑋 , 𝑌 } ⊆ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) )
13 12 3adant1 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( 𝑋 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ↔ { 𝑋 , 𝑌 } ⊆ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) )
14 11 13 mpbird ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) )
15 2 4 lssvacl ⊢ ( ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∈ ( LSubSp ‘ 𝑊 ) ) ∧ ( 𝑋 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ) → ( 𝑋 + 𝑌 ) ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
16 5 9 14 15 syl21anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 + 𝑌 ) ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
17 4 3 5 9 16 ellspsn5 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ⊆ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )