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

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