Metamath Proof Explorer


Theorem lspval

Description: The span of a set of vectors (in a left module). ( spanval analog.) (Contributed by NM, 8-Dec-2013) (Revised by Mario Carneiro, 19-Jun-2014)

Ref Expression
Hypotheses lspval.v 𝑉 = ( Base ‘ 𝑊 )
lspval.s 𝑆 = ( LSubSp ‘ 𝑊 )
lspval.n 𝑁 = ( LSpan ‘ 𝑊 )
Assertion lspval ( ( 𝑊 ∈ LMod ∧ 𝑈𝑉 ) → ( 𝑁𝑈 ) = { 𝑡𝑆𝑈𝑡 } )

Proof

Step Hyp Ref Expression
1 lspval.v 𝑉 = ( Base ‘ 𝑊 )
2 lspval.s 𝑆 = ( LSubSp ‘ 𝑊 )
3 lspval.n 𝑁 = ( LSpan ‘ 𝑊 )
4 1 2 3 lspfval ( 𝑊 ∈ LMod → 𝑁 = ( 𝑠 ∈ 𝒫 𝑉 { 𝑡𝑆𝑠𝑡 } ) )
5 4 fveq1d ( 𝑊 ∈ LMod → ( 𝑁𝑈 ) = ( ( 𝑠 ∈ 𝒫 𝑉 { 𝑡𝑆𝑠𝑡 } ) ‘ 𝑈 ) )
6 5 adantr ( ( 𝑊 ∈ LMod ∧ 𝑈𝑉 ) → ( 𝑁𝑈 ) = ( ( 𝑠 ∈ 𝒫 𝑉 { 𝑡𝑆𝑠𝑡 } ) ‘ 𝑈 ) )
7 eqid ( 𝑠 ∈ 𝒫 𝑉 { 𝑡𝑆𝑠𝑡 } ) = ( 𝑠 ∈ 𝒫 𝑉 { 𝑡𝑆𝑠𝑡 } )
8 sseq1 ( 𝑠 = 𝑈 → ( 𝑠𝑡𝑈𝑡 ) )
9 8 rabbidv ( 𝑠 = 𝑈 → { 𝑡𝑆𝑠𝑡 } = { 𝑡𝑆𝑈𝑡 } )
10 9 inteqd ( 𝑠 = 𝑈 { 𝑡𝑆𝑠𝑡 } = { 𝑡𝑆𝑈𝑡 } )
11 simpr ( ( 𝑊 ∈ LMod ∧ 𝑈𝑉 ) → 𝑈𝑉 )
12 1 fvexi 𝑉 ∈ V
13 12 elpw2 ( 𝑈 ∈ 𝒫 𝑉𝑈𝑉 )
14 11 13 sylibr ( ( 𝑊 ∈ LMod ∧ 𝑈𝑉 ) → 𝑈 ∈ 𝒫 𝑉 )
15 1 2 lss1 ( 𝑊 ∈ LMod → 𝑉𝑆 )
16 sseq2 ( 𝑡 = 𝑉 → ( 𝑈𝑡𝑈𝑉 ) )
17 16 rspcev ( ( 𝑉𝑆𝑈𝑉 ) → ∃ 𝑡𝑆 𝑈𝑡 )
18 15 17 sylan ( ( 𝑊 ∈ LMod ∧ 𝑈𝑉 ) → ∃ 𝑡𝑆 𝑈𝑡 )
19 intexrab ( ∃ 𝑡𝑆 𝑈𝑡 { 𝑡𝑆𝑈𝑡 } ∈ V )
20 18 19 sylib ( ( 𝑊 ∈ LMod ∧ 𝑈𝑉 ) → { 𝑡𝑆𝑈𝑡 } ∈ V )
21 7 10 14 20 fvmptd3 ( ( 𝑊 ∈ LMod ∧ 𝑈𝑉 ) → ( ( 𝑠 ∈ 𝒫 𝑉 { 𝑡𝑆𝑠𝑡 } ) ‘ 𝑈 ) = { 𝑡𝑆𝑈𝑡 } )
22 6 21 eqtrd ( ( 𝑊 ∈ LMod ∧ 𝑈𝑉 ) → ( 𝑁𝑈 ) = { 𝑡𝑆𝑈𝑡 } )