Metamath Proof Explorer

Theorem lsmpr

Description: The span of a pair of vectors equals the sum of the spans of their singletons. (Contributed by NM, 13-Jan-2015)

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

Proof

Step Hyp Ref Expression
1 lsmpr.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lsmpr.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
3 lsmpr.p ⊢ ⊕ = ( LSSum ‘ 𝑊 )
4 lsmpr.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
5 lsmpr.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
6 lsmpr.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
7 5 snssd ⊢ ( 𝜑 → { 𝑋 } ⊆ 𝑉 )
8 6 snssd ⊢ ( 𝜑 → { 𝑌 } ⊆ 𝑉 )
9 1 2 lspun ⊢ ( ( 𝑊 ∈ LMod ∧ { 𝑋 } ⊆ 𝑉 ∧ { 𝑌 } ⊆ 𝑉 ) → ( 𝑁 ‘ ( { 𝑋 } ∪ { 𝑌 } ) ) = ( 𝑁 ‘ ( ( 𝑁 ‘ { 𝑋 } ) ∪ ( 𝑁 ‘ { 𝑌 } ) ) ) )
10 4 7 8 9 syl3anc ⊢ ( 𝜑 → ( 𝑁 ‘ ( { 𝑋 } ∪ { 𝑌 } ) ) = ( 𝑁 ‘ ( ( 𝑁 ‘ { 𝑋 } ) ∪ ( 𝑁 ‘ { 𝑌 } ) ) ) )
11 df-pr ⊢ { 𝑋 , 𝑌 } = ( { 𝑋 } ∪ { 𝑌 } )
12 11 fveq2i ⊢ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) = ( 𝑁 ‘ ( { 𝑋 } ∪ { 𝑌 } ) )
13 12 a1i ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) = ( 𝑁 ‘ ( { 𝑋 } ∪ { 𝑌 } ) ) )
14 eqid ⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
15 1 14 2 lspsncl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑊 ) )
16 4 5 15 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑊 ) )
17 1 14 2 lspsncl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑊 ) )
18 4 6 17 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑊 ) )
19 14 2 3 lsmsp ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑊 ) ∧ ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑊 ) ) → ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) = ( 𝑁 ‘ ( ( 𝑁 ‘ { 𝑋 } ) ∪ ( 𝑁 ‘ { 𝑌 } ) ) ) )
20 4 16 18 19 syl3anc ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) = ( 𝑁 ‘ ( ( 𝑁 ‘ { 𝑋 } ) ∪ ( 𝑁 ‘ { 𝑌 } ) ) ) )
21 10 13 20 3eqtr4d ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) = ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) )