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