lkrval2

Description: Value of the kernel of a functional. (Contributed by NM, 15-Apr-2014)

	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)$
Assertion	lkrval2	$⊢ (W \in X \land G \in F) \to K (G) = \{x \in V \| 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		elex	$⊢ W \in X \to W \in V$
7	1 2 3 4 5	ellkr	$⊢ (W \in V \land G \in F) \to (x \in K (G) \leftrightarrow (x \in V \land G (x) = \underset{˙}{0}))$
8	7	eqabdv	$⊢ (W \in V \land G \in F) \to K (G) = \{x \| (x \in V \land G (x) = \underset{˙}{0})\}$
9		df-rab	$⊢ \{x \in V \| G (x) = \underset{˙}{0}\} = \{x \| (x \in V \land G (x) = \underset{˙}{0})\}$
10	8 9	eqtr4di	$⊢ (W \in V \land G \in F) \to K (G) = \{x \in V \| G (x) = \underset{˙}{0}\}$
11	6 10	sylan	$⊢ (W \in X \land G \in F) \to K (G) = \{x \in V \| G (x) = \underset{˙}{0}\}$

Metamath Proof Explorer