ellkr2

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

	Ref	Expression
Hypotheses	lkrfval2.v	$⊢ V = {Base}_{W}$
	lkrfval2.d	$⊢ D = Scalar (W)$
	lkrfval2.o	$⊢ \underset{˙}{0} = 0_{D}$
	lkrfval2.f	$⊢ F = LFnl (W)$
	lkrfval2.k	$⊢ K = LKer (W)$
	ellkr2.w	$⊢ φ \to W \in Y$
	ellkr2.g	$⊢ φ \to G \in F$
	ellkr2.x	$⊢ φ \to X \in V$
Assertion	ellkr2	$⊢ φ \to (X \in K (G) \leftrightarrow G (X) = \underset{˙}{0})$

Step	Hyp	Ref	Expression
1		lkrfval2.v	$⊢ V = {Base}_{W}$
2		lkrfval2.d	$⊢ D = Scalar (W)$
3		lkrfval2.o	$⊢ \underset{˙}{0} = 0_{D}$
4		lkrfval2.f	$⊢ F = LFnl (W)$
5		lkrfval2.k	$⊢ K = LKer (W)$
6		ellkr2.w	$⊢ φ \to W \in Y$
7		ellkr2.g	$⊢ φ \to G \in F$
8		ellkr2.x	$⊢ φ \to X \in V$
9	1 2 3 4 5	ellkr	$⊢ (W \in Y \land G \in F) \to (X \in K (G) \leftrightarrow (X \in V \land G (X) = \underset{˙}{0}))$
10	6 7 9	syl2anc	$⊢ φ \to (X \in K (G) \leftrightarrow (X \in V \land G (X) = \underset{˙}{0}))$
11	8	biantrurd	$⊢ φ \to (G (X) = \underset{˙}{0} \leftrightarrow (X \in V \land G (X) = \underset{˙}{0}))$
12	10 11	bitr4d	$⊢ φ \to (X \in K (G) \leftrightarrow G (X) = \underset{˙}{0})$

Metamath Proof Explorer