Metamath Proof Explorer

Theorem lsppr

Description: Span of a pair of vectors. (Contributed by NM, 22-Aug-2014)

Ref Expression
Hypotheses lsppr.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lsppr.a ⊢ + = ( +g ‘ 𝑊 )
lsppr.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
lsppr.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
lsppr.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
lsppr.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
lsppr.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
lsppr.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
lsppr.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
Assertion lsppr ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) = { 𝑣 ∣ ∃ 𝑘 ∈ 𝐾 ∃ 𝑙 ∈ 𝐾 𝑣 = ( ( 𝑘 · 𝑋 ) + ( 𝑙 · 𝑌 ) ) } )

Proof

Step Hyp Ref Expression
1 lsppr.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lsppr.a ⊢ + = ( +g ‘ 𝑊 )
3 lsppr.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
4 lsppr.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
5 lsppr.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
6 lsppr.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
7 lsppr.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
8 lsppr.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
9 lsppr.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
10 df-pr ⊢ { 𝑋 , 𝑌 } = ( { 𝑋 } ∪ { 𝑌 } )
11 10 fveq2i ⊢ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) = ( 𝑁 ‘ ( { 𝑋 } ∪ { 𝑌 } ) )
12 8 snssd ⊢ ( 𝜑 → { 𝑋 } ⊆ 𝑉 )
13 9 snssd ⊢ ( 𝜑 → { 𝑌 } ⊆ 𝑉 )
14 1 6 lspun ⊢ ( ( 𝑊 ∈ LMod ∧ { 𝑋 } ⊆ 𝑉 ∧ { 𝑌 } ⊆ 𝑉 ) → ( 𝑁 ‘ ( { 𝑋 } ∪ { 𝑌 } ) ) = ( 𝑁 ‘ ( ( 𝑁 ‘ { 𝑋 } ) ∪ ( 𝑁 ‘ { 𝑌 } ) ) ) )
15 7 12 13 14 syl3anc ⊢ ( 𝜑 → ( 𝑁 ‘ ( { 𝑋 } ∪ { 𝑌 } ) ) = ( 𝑁 ‘ ( ( 𝑁 ‘ { 𝑋 } ) ∪ ( 𝑁 ‘ { 𝑌 } ) ) ) )
16 eqid ⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
17 1 16 6 lspsncl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑊 ) )
18 7 8 17 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑊 ) )
19 1 16 6 lspsncl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑊 ) )
20 7 9 19 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑊 ) )
21 eqid ⊢ ( LSSum ‘ 𝑊 ) = ( LSSum ‘ 𝑊 )
22 16 6 21 lsmsp ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑊 ) ∧ ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑊 ) ) → ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑌 } ) ) = ( 𝑁 ‘ ( ( 𝑁 ‘ { 𝑋 } ) ∪ ( 𝑁 ‘ { 𝑌 } ) ) ) )
23 7 18 20 22 syl3anc ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑌 } ) ) = ( 𝑁 ‘ ( ( 𝑁 ‘ { 𝑋 } ) ∪ ( 𝑁 ‘ { 𝑌 } ) ) ) )
24 1 2 3 4 5 21 6 7 8 9 lsmspsn ⊢ ( 𝜑 → ( 𝑣 ∈ ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑌 } ) ) ↔ ∃ 𝑘 ∈ 𝐾 ∃ 𝑙 ∈ 𝐾 𝑣 = ( ( 𝑘 · 𝑋 ) + ( 𝑙 · 𝑌 ) ) ) )
25 24 abbi2dv ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑌 } ) ) = { 𝑣 ∣ ∃ 𝑘 ∈ 𝐾 ∃ 𝑙 ∈ 𝐾 𝑣 = ( ( 𝑘 · 𝑋 ) + ( 𝑙 · 𝑌 ) ) } )
26 15 23 25 3eqtr2d ⊢ ( 𝜑 → ( 𝑁 ‘ ( { 𝑋 } ∪ { 𝑌 } ) ) = { 𝑣 ∣ ∃ 𝑘 ∈ 𝐾 ∃ 𝑙 ∈ 𝐾 𝑣 = ( ( 𝑘 · 𝑋 ) + ( 𝑙 · 𝑌 ) ) } )
27 11 26 eqtrid ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) = { 𝑣 ∣ ∃ 𝑘 ∈ 𝐾 ∃ 𝑙 ∈ 𝐾 𝑣 = ( ( 𝑘 · 𝑋 ) + ( 𝑙 · 𝑌 ) ) } )