Metamath Proof Explorer


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