Metamath Proof Explorer


Theorem ellkr

Description: Membership in the kernel of a functional. ( elnlfn analog.) (Contributed by NM, 16-Apr-2014)

Ref Expression
Hypotheses lkrfval2.v 𝑉 = ( Base ‘ 𝑊 )
lkrfval2.d 𝐷 = ( Scalar ‘ 𝑊 )
lkrfval2.o 0 = ( 0g𝐷 )
lkrfval2.f 𝐹 = ( LFnl ‘ 𝑊 )
lkrfval2.k 𝐾 = ( LKer ‘ 𝑊 )
Assertion ellkr ( ( 𝑊𝑌𝐺𝐹 ) → ( 𝑋 ∈ ( 𝐾𝐺 ) ↔ ( 𝑋𝑉 ∧ ( 𝐺𝑋 ) = 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 2 3 4 5 lkrval ( ( 𝑊𝑌𝐺𝐹 ) → ( 𝐾𝐺 ) = ( 𝐺 “ { 0 } ) )
7 6 eleq2d ( ( 𝑊𝑌𝐺𝐹 ) → ( 𝑋 ∈ ( 𝐾𝐺 ) ↔ 𝑋 ∈ ( 𝐺 “ { 0 } ) ) )
8 eqid ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
9 2 8 1 4 lflf ( ( 𝑊𝑌𝐺𝐹 ) → 𝐺 : 𝑉 ⟶ ( Base ‘ 𝐷 ) )
10 ffn ( 𝐺 : 𝑉 ⟶ ( Base ‘ 𝐷 ) → 𝐺 Fn 𝑉 )
11 elpreima ( 𝐺 Fn 𝑉 → ( 𝑋 ∈ ( 𝐺 “ { 0 } ) ↔ ( 𝑋𝑉 ∧ ( 𝐺𝑋 ) ∈ { 0 } ) ) )
12 9 10 11 3syl ( ( 𝑊𝑌𝐺𝐹 ) → ( 𝑋 ∈ ( 𝐺 “ { 0 } ) ↔ ( 𝑋𝑉 ∧ ( 𝐺𝑋 ) ∈ { 0 } ) ) )
13 fvex ( 𝐺𝑋 ) ∈ V
14 13 elsn ( ( 𝐺𝑋 ) ∈ { 0 } ↔ ( 𝐺𝑋 ) = 0 )
15 14 anbi2i ( ( 𝑋𝑉 ∧ ( 𝐺𝑋 ) ∈ { 0 } ) ↔ ( 𝑋𝑉 ∧ ( 𝐺𝑋 ) = 0 ) )
16 12 15 bitrdi ( ( 𝑊𝑌𝐺𝐹 ) → ( 𝑋 ∈ ( 𝐺 “ { 0 } ) ↔ ( 𝑋𝑉 ∧ ( 𝐺𝑋 ) = 0 ) ) )
17 7 16 bitrd ( ( 𝑊𝑌𝐺𝐹 ) → ( 𝑋 ∈ ( 𝐾𝐺 ) ↔ ( 𝑋𝑉 ∧ ( 𝐺𝑋 ) = 0 ) ) )