Theorem lkrfval

Description: The kernel of a functional. (Contributed by NM, 15-Apr-2014) (Revised by Mario Carneiro, 24-Jun-2014)

	Ref	Expression
Hypotheses	lkrfval.d	⊢ 𝐷 = ( Scalar ‘ 𝑊 )
	lkrfval.o	⊢ 0 = ( 0g ‘ 𝐷 )
	lkrfval.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
	lkrfval.k	⊢ 𝐾 = ( LKer ‘ 𝑊 )
Assertion	lkrfval	⊢ ( 𝑊 ∈ 𝑋 → 𝐾 = ( 𝑓 ∈ 𝐹 ↦ ( ◡ 𝑓 “ { 0 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		lkrfval.d	⊢ 𝐷 = ( Scalar ‘ 𝑊 )
2		lkrfval.o	⊢ 0 = ( 0g ‘ 𝐷 )
3		lkrfval.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
4		lkrfval.k	⊢ 𝐾 = ( LKer ‘ 𝑊 )
5		elex	⊢ ( 𝑊 ∈ 𝑋 → 𝑊 ∈ V )
6		fveq2	⊢ ( 𝑤 = 𝑊 → ( LFnl ‘ 𝑤 ) = ( LFnl ‘ 𝑊 ) )
7	6 3	eqtr4di	⊢ ( 𝑤 = 𝑊 → ( LFnl ‘ 𝑤 ) = 𝐹 )
8		fveq2	⊢ ( 𝑤 = 𝑊 → ( Scalar ‘ 𝑤 ) = ( Scalar ‘ 𝑊 ) )
9	8 1	eqtr4di	⊢ ( 𝑤 = 𝑊 → ( Scalar ‘ 𝑤 ) = 𝐷 )
10	9	fveq2d	⊢ ( 𝑤 = 𝑊 → ( 0g ‘ ( Scalar ‘ 𝑤 ) ) = ( 0g ‘ 𝐷 ) )
11	10 2	eqtr4di	⊢ ( 𝑤 = 𝑊 → ( 0g ‘ ( Scalar ‘ 𝑤 ) ) = 0 )
12	11	sneqd	⊢ ( 𝑤 = 𝑊 → { ( 0g ‘ ( Scalar ‘ 𝑤 ) ) } = { 0 } )
13	12	imaeq2d	⊢ ( 𝑤 = 𝑊 → ( ◡ 𝑓 “ { ( 0g ‘ ( Scalar ‘ 𝑤 ) ) } ) = ( ◡ 𝑓 “ { 0 } ) )
14	7 13	mpteq12dv	⊢ ( 𝑤 = 𝑊 → ( 𝑓 ∈ ( LFnl ‘ 𝑤 ) ↦ ( ◡ 𝑓 “ { ( 0g ‘ ( Scalar ‘ 𝑤 ) ) } ) ) = ( 𝑓 ∈ 𝐹 ↦ ( ◡ 𝑓 “ { 0 } ) ) )
15		df-lkr	⊢ LKer = ( 𝑤 ∈ V ↦ ( 𝑓 ∈ ( LFnl ‘ 𝑤 ) ↦ ( ◡ 𝑓 “ { ( 0g ‘ ( Scalar ‘ 𝑤 ) ) } ) ) )
16	14 15 3	mptfvmpt	⊢ ( 𝑊 ∈ V → ( LKer ‘ 𝑊 ) = ( 𝑓 ∈ 𝐹 ↦ ( ◡ 𝑓 “ { 0 } ) ) )
17	4 16	syl5eq	⊢ ( 𝑊 ∈ V → 𝐾 = ( 𝑓 ∈ 𝐹 ↦ ( ◡ 𝑓 “ { 0 } ) ) )
18	5 17	syl	⊢ ( 𝑊 ∈ 𝑋 → 𝐾 = ( 𝑓 ∈ 𝐹 ↦ ( ◡ 𝑓 “ { 0 } ) ) )