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