Metamath Proof Explorer


Theorem lkrcl

Description: A member of the kernel of a functional is a vector. (Contributed by NM, 16-Apr-2014)

Ref Expression
Hypotheses lkrcl.v 𝑉 = ( Base ‘ 𝑊 )
lkrcl.f 𝐹 = ( LFnl ‘ 𝑊 )
lkrcl.k 𝐾 = ( LKer ‘ 𝑊 )
Assertion lkrcl ( ( 𝑊𝑌𝐺𝐹𝑋 ∈ ( 𝐾𝐺 ) ) → 𝑋𝑉 )

Proof

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