Theorem lspprvacl

Description: The sum of two vectors belongs to their span. (Contributed by NM, 20-May-2015)

	Ref	Expression
Hypotheses	lspprvacl.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lspprvacl.p	⊢ + = ( +g ‘ 𝑊 )
	lspprvacl.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
	lspprvacl.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
	lspprvacl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	lspprvacl.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
Assertion	lspprvacl	⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )

Proof

Step	Hyp	Ref	Expression
1		lspprvacl.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lspprvacl.p	⊢ + = ( +g ‘ 𝑊 )
3		lspprvacl.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
4		lspprvacl.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
5		lspprvacl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
6		lspprvacl.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
7		eqid	⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
8	1 7 3 4 5 6	lspprcl	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∈ ( LSubSp ‘ 𝑊 ) )
9	1 3 4 5 6	lspprid1	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
10	1 3 4 5 6	lspprid2	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
11	2 7	lssvacl	⊢ ( ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∈ ( LSubSp ‘ 𝑊 ) ) ∧ ( 𝑋 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ) → ( 𝑋 + 𝑌 ) ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
12	4 8 9 10 11	syl22anc	⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )