Theorem lspfval

Description: The span function for a left vector space (or a left module). ( df-span 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	lspfval	⊢ ( 𝑊 ∈ 𝑋 → 𝑁 = ( 𝑠 ∈ 𝒫 𝑉 ↦ ∩ { 𝑡 ∈ 𝑆 ∣ 𝑠 ⊆ 𝑡 } ) )

Proof

Step	Hyp	Ref	Expression
1		lspval.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lspval.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3		lspval.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
4		elex	⊢ ( 𝑊 ∈ 𝑋 → 𝑊 ∈ V )
5		fveq2	⊢ ( 𝑤 = 𝑊 → ( Base ‘ 𝑤 ) = ( Base ‘ 𝑊 ) )
6	5 1	eqtr4di	⊢ ( 𝑤 = 𝑊 → ( Base ‘ 𝑤 ) = 𝑉 )
7	6	pweqd	⊢ ( 𝑤 = 𝑊 → 𝒫 ( Base ‘ 𝑤 ) = 𝒫 𝑉 )
8		fveq2	⊢ ( 𝑤 = 𝑊 → ( LSubSp ‘ 𝑤 ) = ( LSubSp ‘ 𝑊 ) )
9	8 2	eqtr4di	⊢ ( 𝑤 = 𝑊 → ( LSubSp ‘ 𝑤 ) = 𝑆 )
10	9	rabeqdv	⊢ ( 𝑤 = 𝑊 → { 𝑡 ∈ ( LSubSp ‘ 𝑤 ) ∣ 𝑠 ⊆ 𝑡 } = { 𝑡 ∈ 𝑆 ∣ 𝑠 ⊆ 𝑡 } )
11	10	inteqd	⊢ ( 𝑤 = 𝑊 → ∩ { 𝑡 ∈ ( LSubSp ‘ 𝑤 ) ∣ 𝑠 ⊆ 𝑡 } = ∩ { 𝑡 ∈ 𝑆 ∣ 𝑠 ⊆ 𝑡 } )
12	7 11	mpteq12dv	⊢ ( 𝑤 = 𝑊 → ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑤 ) ↦ ∩ { 𝑡 ∈ ( LSubSp ‘ 𝑤 ) ∣ 𝑠 ⊆ 𝑡 } ) = ( 𝑠 ∈ 𝒫 𝑉 ↦ ∩ { 𝑡 ∈ 𝑆 ∣ 𝑠 ⊆ 𝑡 } ) )
13		df-lsp	⊢ LSpan = ( 𝑤 ∈ V ↦ ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑤 ) ↦ ∩ { 𝑡 ∈ ( LSubSp ‘ 𝑤 ) ∣ 𝑠 ⊆ 𝑡 } ) )
14	1	fvexi	⊢ 𝑉 ∈ V
15	14	pwex	⊢ 𝒫 𝑉 ∈ V
16	15	mptex	⊢ ( 𝑠 ∈ 𝒫 𝑉 ↦ ∩ { 𝑡 ∈ 𝑆 ∣ 𝑠 ⊆ 𝑡 } ) ∈ V
17	12 13 16	fvmpt	⊢ ( 𝑊 ∈ V → ( LSpan ‘ 𝑊 ) = ( 𝑠 ∈ 𝒫 𝑉 ↦ ∩ { 𝑡 ∈ 𝑆 ∣ 𝑠 ⊆ 𝑡 } ) )
18	4 17	syl	⊢ ( 𝑊 ∈ 𝑋 → ( LSpan ‘ 𝑊 ) = ( 𝑠 ∈ 𝒫 𝑉 ↦ ∩ { 𝑡 ∈ 𝑆 ∣ 𝑠 ⊆ 𝑡 } ) )
19	3 18	syl5eq	⊢ ( 𝑊 ∈ 𝑋 → 𝑁 = ( 𝑠 ∈ 𝒫 𝑉 ↦ ∩ { 𝑡 ∈ 𝑆 ∣ 𝑠 ⊆ 𝑡 } ) )