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

Metamath Proof Explorer

Theorem lkrval

Description: Value of the kernel of a functional. (Contributed by NM, 15-Apr-2014)

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

Proof

Step Hyp Ref Expression
1 lkrfval.d ⊢ 𝐷 = ( Scalar ‘ 𝑊 )
2 lkrfval.o ⊢ 0 = ( 0g ‘ 𝐷 )
3 lkrfval.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
4 lkrfval.k ⊢ 𝐾 = ( LKer ‘ 𝑊 )
5 1 2 3 4 lkrfval ⊢ ( 𝑊 ∈ 𝑋 → 𝐾 = ( 𝑓 ∈ 𝐹 ↦ ( ◡ 𝑓 “ { 0 } ) ) )
6 5 fveq1d ⊢ ( 𝑊 ∈ 𝑋 → ( 𝐾 ‘ 𝐺 ) = ( ( 𝑓 ∈ 𝐹 ↦ ( ◡ 𝑓 “ { 0 } ) ) ‘ 𝐺 ) )
7 cnvexg ⊢ ( 𝐺 ∈ 𝐹 → ◡ 𝐺 ∈ V )
8 imaexg ⊢ ( ◡ 𝐺 ∈ V → ( ◡ 𝐺 “ { 0 } ) ∈ V )
9 7 8 syl ⊢ ( 𝐺 ∈ 𝐹 → ( ◡ 𝐺 “ { 0 } ) ∈ V )
10 cnveq ⊢ ( 𝑓 = 𝐺 → ◡ 𝑓 = ◡ 𝐺 )
11 10 imaeq1d ⊢ ( 𝑓 = 𝐺 → ( ◡ 𝑓 “ { 0 } ) = ( ◡ 𝐺 “ { 0 } ) )
12 eqid ⊢ ( 𝑓 ∈ 𝐹 ↦ ( ◡ 𝑓 “ { 0 } ) ) = ( 𝑓 ∈ 𝐹 ↦ ( ◡ 𝑓 “ { 0 } ) )
13 11 12 fvmptg ⊢ ( ( 𝐺 ∈ 𝐹 ∧ ( ◡ 𝐺 “ { 0 } ) ∈ V ) → ( ( 𝑓 ∈ 𝐹 ↦ ( ◡ 𝑓 “ { 0 } ) ) ‘ 𝐺 ) = ( ◡ 𝐺 “ { 0 } ) )
14 9 13 mpdan ⊢ ( 𝐺 ∈ 𝐹 → ( ( 𝑓 ∈ 𝐹 ↦ ( ◡ 𝑓 “ { 0 } ) ) ‘ 𝐺 ) = ( ◡ 𝐺 “ { 0 } ) )
15 6 14 sylan9eq ⊢ ( ( 𝑊 ∈ 𝑋 ∧ 𝐺 ∈ 𝐹 ) → ( 𝐾 ‘ 𝐺 ) = ( ◡ 𝐺 “ { 0 } ) )