lkrval

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

	Ref	Expression
Hypotheses	lkrfval.d	$⊢ D = Scalar (W)$
	lkrfval.o	$⊢ \underset{˙}{0} = 0_{D}$
	lkrfval.f	$⊢ F = LFnl (W)$
	lkrfval.k	$⊢ K = LKer (W)$
Assertion	lkrval	$⊢ (W \in X \land G \in F) \to K (G) = G^{-1} [\{\underset{˙}{0}\}]$

Step	Hyp	Ref	Expression
1		lkrfval.d	$⊢ D = Scalar (W)$
2		lkrfval.o	$⊢ \underset{˙}{0} = 0_{D}$
3		lkrfval.f	$⊢ F = LFnl (W)$
4		lkrfval.k	$⊢ K = LKer (W)$
5	1 2 3 4	lkrfval	$⊢ W \in X \to K = (f \in F ⟼ f^{-1} [\{\underset{˙}{0}\}])$
6	5	fveq1d	$⊢ W \in X \to K (G) = (f \in F ⟼ f^{-1} [\{\underset{˙}{0}\}]) (G)$
7		cnvexg	$⊢ G \in F \to G^{-1} \in V$
8		imaexg	$⊢ G^{-1} \in V \to G^{-1} [\{\underset{˙}{0}\}] \in V$
9	7 8	syl	$⊢ G \in F \to G^{-1} [\{\underset{˙}{0}\}] \in V$
10		cnveq	$⊢ f = G \to f^{-1} = G^{-1}$
11	10	imaeq1d	$⊢ f = G \to f^{-1} [\{\underset{˙}{0}\}] = G^{-1} [\{\underset{˙}{0}\}]$
12		eqid	$⊢ (f \in F ⟼ f^{-1} [\{\underset{˙}{0}\}]) = (f \in F ⟼ f^{-1} [\{\underset{˙}{0}\}])$
13	11 12	fvmptg	$⊢ (G \in F \land G^{-1} [\{\underset{˙}{0}\}] \in V) \to (f \in F ⟼ f^{-1} [\{\underset{˙}{0}\}]) (G) = G^{-1} [\{\underset{˙}{0}\}]$
14	9 13	mpdan	$⊢ G \in F \to (f \in F ⟼ f^{-1} [\{\underset{˙}{0}\}]) (G) = G^{-1} [\{\underset{˙}{0}\}]$
15	6 14	sylan9eq	$⊢ (W \in X \land G \in F) \to K (G) = G^{-1} [\{\underset{˙}{0}\}]$

Metamath Proof Explorer