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	$⊢ D = Scalar (W)$
	lkrf0.o	$⊢ \underset{˙}{0} = 0_{D}$
	lkrf0.f	$⊢ F = LFnl (W)$
	lkrf0.k	$⊢ K = LKer (W)$
Assertion	lkrf0	$⊢ (W \in Y \land G \in F \land X \in K (G)) \to G (X) = \underset{˙}{0}$

Step	Hyp	Ref	Expression
1		lkrf0.d	$⊢ D = Scalar (W)$
2		lkrf0.o	$⊢ \underset{˙}{0} = 0_{D}$
3		lkrf0.f	$⊢ F = LFnl (W)$
4		lkrf0.k	$⊢ K = LKer (W)$
5		eqid	$⊢ {Base}_{W} = {Base}_{W}$
6	5 1 2 3 4	ellkr	$⊢ (W \in Y \land G \in F) \to (X \in K (G) \leftrightarrow (X \in {Base}_{W} \land G (X) = \underset{˙}{0}))$
7	6	simplbda	$⊢ ((W \in Y \land G \in F) \land X \in K (G)) \to G (X) = \underset{˙}{0}$
8	7	3impa	$⊢ (W \in Y \land G \in F \land X \in K (G)) \to G (X) = \underset{˙}{0}$

Metamath Proof Explorer