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 ‘ 𝑤 ) ) } ) ) )