Theorem lkrval2

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

	Ref	Expression
Hypotheses	lkrfval2.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lkrfval2.d	⊢ 𝐷 = ( Scalar ‘ 𝑊 )
	lkrfval2.o	⊢ 0 = ( 0g ‘ 𝐷 )
	lkrfval2.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
	lkrfval2.k	⊢ 𝐾 = ( LKer ‘ 𝑊 )
Assertion	lkrval2	⊢ ( ( 𝑊 ∈ 𝑋 ∧ 𝐺 ∈ 𝐹 ) → ( 𝐾 ‘ 𝐺 ) = { 𝑥 ∈ 𝑉 ∣ ( 𝐺 ‘ 𝑥 ) = 0 } )

Proof

Step	Hyp	Ref	Expression
1		lkrfval2.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lkrfval2.d	⊢ 𝐷 = ( Scalar ‘ 𝑊 )
3		lkrfval2.o	⊢ 0 = ( 0g ‘ 𝐷 )
4		lkrfval2.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
5		lkrfval2.k	⊢ 𝐾 = ( LKer ‘ 𝑊 )
6		elex	⊢ ( 𝑊 ∈ 𝑋 → 𝑊 ∈ V )
7	1 2 3 4 5	ellkr	⊢ ( ( 𝑊 ∈ V ∧ 𝐺 ∈ 𝐹 ) → ( 𝑥 ∈ ( 𝐾 ‘ 𝐺 ) ↔ ( 𝑥 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑥 ) = 0 ) ) )
8	7	eqabdv	⊢ ( ( 𝑊 ∈ V ∧ 𝐺 ∈ 𝐹 ) → ( 𝐾 ‘ 𝐺 ) = { 𝑥 ∣ ( 𝑥 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑥 ) = 0 ) } )
9		df-rab	⊢ { 𝑥 ∈ 𝑉 ∣ ( 𝐺 ‘ 𝑥 ) = 0 } = { 𝑥 ∣ ( 𝑥 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑥 ) = 0 ) }
10	8 9	eqtr4di	⊢ ( ( 𝑊 ∈ V ∧ 𝐺 ∈ 𝐹 ) → ( 𝐾 ‘ 𝐺 ) = { 𝑥 ∈ 𝑉 ∣ ( 𝐺 ‘ 𝑥 ) = 0 } )
11	6 10	sylan	⊢ ( ( 𝑊 ∈ 𝑋 ∧ 𝐺 ∈ 𝐹 ) → ( 𝐾 ‘ 𝐺 ) = { 𝑥 ∈ 𝑉 ∣ ( 𝐺 ‘ 𝑥 ) = 0 } )