ellkr

Description: Membership in the kernel of a functional. ( elnlfn analog.) (Contributed by NM, 16-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	ellkr	$⊢ (W \in Y \land G \in F) \to (X \in K (G) \leftrightarrow (X \in V \land 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	2 3 4 5	lkrval	$⊢ (W \in Y \land G \in F) \to K (G) = G^{-1} [\{\underset{˙}{0}\}]$
7	6	eleq2d	$⊢ (W \in Y \land G \in F) \to (X \in K (G) \leftrightarrow X \in G^{-1} [\{\underset{˙}{0}\}])$
8		eqid	$⊢ {Base}_{D} = {Base}_{D}$
9	2 8 1 4	lflf	$⊢ (W \in Y \land G \in F) \to G : V ⟶ {Base}_{D}$
10		ffn	$⊢ G : V ⟶ {Base}_{D} \to G Fn V$
11		elpreima	$⊢ G Fn V \to (X \in G^{-1} [\{\underset{˙}{0}\}] \leftrightarrow (X \in V \land G (X) \in \{\underset{˙}{0}\}))$
12	9 10 11	3syl	$⊢ (W \in Y \land G \in F) \to (X \in G^{-1} [\{\underset{˙}{0}\}] \leftrightarrow (X \in V \land G (X) \in \{\underset{˙}{0}\}))$
13		fvex	$⊢ G (X) \in V$
14	13	elsn	$⊢ G (X) \in \{\underset{˙}{0}\} \leftrightarrow G (X) = \underset{˙}{0}$
15	14	anbi2i	$⊢ (X \in V \land G (X) \in \{\underset{˙}{0}\}) \leftrightarrow (X \in V \land G (X) = \underset{˙}{0})$
16	12 15	bitrdi	$⊢ (W \in Y \land G \in F) \to (X \in G^{-1} [\{\underset{˙}{0}\}] \leftrightarrow (X \in V \land G (X) = \underset{˙}{0}))$
17	7 16	bitrd	$⊢ (W \in Y \land G \in F) \to (X \in K (G) \leftrightarrow (X \in V \land G (X) = \underset{˙}{0}))$

Metamath Proof Explorer