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

Metamath Proof Explorer

Definition df-lkr

Description: Define the kernel of a functional (set of vectors whose functional value is zero) on a left module or left vector space. (Contributed by NM, 15-Apr-2014)

Ref Expression
Assertion df-lkr LKer = ( 𝑤 ∈ V ↦ ( 𝑓 ∈ ( LFnl ‘ 𝑤 ) ↦ ( ◡ 𝑓 “ { ( 0g ‘ ( Scalar ‘ 𝑤 ) ) } ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 clk ⊢ LKer
1 vw ⊢ 𝑤
2 cvv ⊢ V
3 vf ⊢ 𝑓
4 clfn ⊢ LFnl
5 1 cv ⊢ 𝑤
6 5 4 cfv ⊢ ( LFnl ‘ 𝑤 )
7 3 cv ⊢ 𝑓
8 7 ccnv ⊢ ◡ 𝑓
9 c0g ⊢ 0g
10 csca ⊢ Scalar
11 5 10 cfv ⊢ ( Scalar ‘ 𝑤 )
12 11 9 cfv ⊢ ( 0g ‘ ( Scalar ‘ 𝑤 ) )
13 12 csn ⊢ { ( 0g ‘ ( Scalar ‘ 𝑤 ) ) }
14 8 13 cima ⊢ ( ◡ 𝑓 “ { ( 0g ‘ ( Scalar ‘ 𝑤 ) ) } )
15 3 6 14 cmpt ⊢ ( 𝑓 ∈ ( LFnl ‘ 𝑤 ) ↦ ( ◡ 𝑓 “ { ( 0g ‘ ( Scalar ‘ 𝑤 ) ) } ) )
16 1 2 15 cmpt ⊢ ( 𝑤 ∈ V ↦ ( 𝑓 ∈ ( LFnl ‘ 𝑤 ) ↦ ( ◡ 𝑓 “ { ( 0g ‘ ( Scalar ‘ 𝑤 ) ) } ) ) )
17 0 16 wceq ⊢ LKer = ( 𝑤 ∈ V ↦ ( 𝑓 ∈ ( LFnl ‘ 𝑤 ) ↦ ( ◡ 𝑓 “ { ( 0g ‘ ( Scalar ‘ 𝑤 ) ) } ) ) )