This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid ⊢ ( 𝑊 ∈ V → 𝐾 = ( 𝑓 ∈ 𝐹 ↦ ( ◡ 𝑓 “ { 0 } ) ) )
18 5 17 syl ⊢ ( 𝑊 ∈ 𝑋 → 𝐾 = ( 𝑓 ∈ 𝐹 ↦ ( ◡ 𝑓 “ { 0 } ) ) )