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