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

Metamath Proof Explorer

Theorem ellkr2

Description: Membership in the kernel of a functional. (Contributed by NM, 12-Jan-2015)

Ref Expression
Hypotheses lkrfval2.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lkrfval2.d ⊢ 𝐷 = ( Scalar ‘ 𝑊 )
lkrfval2.o ⊢ 0 = ( 0g ‘ 𝐷 )
lkrfval2.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
lkrfval2.k ⊢ 𝐾 = ( LKer ‘ 𝑊 )
ellkr2.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑌 )
ellkr2.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
ellkr2.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
Assertion ellkr2 ( 𝜑 → ( 𝑋 ∈ ( 𝐾 ‘ 𝐺 ) ↔ ( 𝐺 ‘ 𝑋 ) = 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 ellkr2.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑌 )
7 ellkr2.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
8 ellkr2.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
9 1 2 3 4 5 ellkr ⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐺 ∈ 𝐹 ) → ( 𝑋 ∈ ( 𝐾 ‘ 𝐺 ) ↔ ( 𝑋 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑋 ) = 0 ) ) )
10 6 7 9 syl2anc ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐾 ‘ 𝐺 ) ↔ ( 𝑋 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑋 ) = 0 ) ) )
11 8 biantrurd ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑋 ) = 0 ↔ ( 𝑋 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑋 ) = 0 ) ) )
12 10 11 bitr4d ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐾 ‘ 𝐺 ) ↔ ( 𝐺 ‘ 𝑋 ) = 0 ) )