Metamath Proof Explorer


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 abbi2dv ( ( 𝑊 ∈ V ∧ 𝐺𝐹 ) → ( 𝐾𝐺 ) = { 𝑥 ∣ ( 𝑥𝑉 ∧ ( 𝐺𝑥 ) = 0 ) } )
9 df-rab { 𝑥𝑉 ∣ ( 𝐺𝑥 ) = 0 } = { 𝑥 ∣ ( 𝑥𝑉 ∧ ( 𝐺𝑥 ) = 0 ) }
10 8 9 eqtr4di ( ( 𝑊 ∈ V ∧ 𝐺𝐹 ) → ( 𝐾𝐺 ) = { 𝑥𝑉 ∣ ( 𝐺𝑥 ) = 0 } )
11 6 10 sylan ( ( 𝑊𝑋𝐺𝐹 ) → ( 𝐾𝐺 ) = { 𝑥𝑉 ∣ ( 𝐺𝑥 ) = 0 } )