Theorem lkrf0

Description: The value of a functional at a member of its kernel is zero. (Contributed by NM, 16-Apr-2014)

	Ref	Expression
Hypotheses	lkrf0.d	⊢ 𝐷 = ( Scalar ‘ 𝑊 )
	lkrf0.o	⊢ 0 = ( 0g ‘ 𝐷 )
	lkrf0.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
	lkrf0.k	⊢ 𝐾 = ( LKer ‘ 𝑊 )
Assertion	lkrf0	⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐺 ∈ 𝐹 ∧ 𝑋 ∈ ( 𝐾 ‘ 𝐺 ) ) → ( 𝐺 ‘ 𝑋 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		lkrf0.d	⊢ 𝐷 = ( Scalar ‘ 𝑊 )
2		lkrf0.o	⊢ 0 = ( 0g ‘ 𝐷 )
3		lkrf0.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
4		lkrf0.k	⊢ 𝐾 = ( LKer ‘ 𝑊 )
5		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
6	5 1 2 3 4	ellkr	⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐺 ∈ 𝐹 ) → ( 𝑋 ∈ ( 𝐾 ‘ 𝐺 ) ↔ ( 𝑋 ∈ ( Base ‘ 𝑊 ) ∧ ( 𝐺 ‘ 𝑋 ) = 0 ) ) )
7	6	simplbda	⊢ ( ( ( 𝑊 ∈ 𝑌 ∧ 𝐺 ∈ 𝐹 ) ∧ 𝑋 ∈ ( 𝐾 ‘ 𝐺 ) ) → ( 𝐺 ‘ 𝑋 ) = 0 )
8	7	3impa	⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐺 ∈ 𝐹 ∧ 𝑋 ∈ ( 𝐾 ‘ 𝐺 ) ) → ( 𝐺 ‘ 𝑋 ) = 0 )