Metamath Proof Explorer


Theorem lkrf0

Description: The value of a functional at a member of its kernel is zero. (Contributed by NM, 16-Apr-2014)

Ref Expression
Hypotheses lkrf0.d 𝐷 = ( Scalar ‘ 𝑊 )
lkrf0.o 0 = ( 0g𝐷 )
lkrf0.f 𝐹 = ( LFnl ‘ 𝑊 )
lkrf0.k 𝐾 = ( LKer ‘ 𝑊 )
Assertion lkrf0 ( ( 𝑊𝑌𝐺𝐹𝑋 ∈ ( 𝐾𝐺 ) ) → ( 𝐺𝑋 ) = 0 )

Proof

Step Hyp Ref Expression
1 lkrf0.d 𝐷 = ( Scalar ‘ 𝑊 )
2 lkrf0.o 0 = ( 0g𝐷 )
3 lkrf0.f 𝐹 = ( LFnl ‘ 𝑊 )
4 lkrf0.k 𝐾 = ( LKer ‘ 𝑊 )
5 eqid ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
6 5 1 2 3 4 ellkr ( ( 𝑊𝑌𝐺𝐹 ) → ( 𝑋 ∈ ( 𝐾𝐺 ) ↔ ( 𝑋 ∈ ( Base ‘ 𝑊 ) ∧ ( 𝐺𝑋 ) = 0 ) ) )
7 6 simplbda ( ( ( 𝑊𝑌𝐺𝐹 ) ∧ 𝑋 ∈ ( 𝐾𝐺 ) ) → ( 𝐺𝑋 ) = 0 )
8 7 3impa ( ( 𝑊𝑌𝐺𝐹𝑋 ∈ ( 𝐾𝐺 ) ) → ( 𝐺𝑋 ) = 0 )