This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ) )