lkr0f2

Description: The kernel of the zero functional is the set of all vectors. (Contributed by NM, 4-Feb-2015)

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

Step	Hyp	Ref	Expression
1		lkr0f2.v	$⊢ V = {Base}_{W}$
2		lkr0f2.f	$⊢ F = LFnl (W)$
3		lkr0f2.k	$⊢ K = LKer (W)$
4		lkr0f2.d	$⊢ D = LDual (W)$
5		lkr0f2.o	$⊢ \underset{˙}{0} = 0_{D}$
6		lkr0f2.w	$⊢ φ \to W \in LMod$
7		lkr0f2.g	$⊢ φ \to G \in F$
8		eqid	$⊢ Scalar (W) = Scalar (W)$
9		eqid	$⊢ 0_{Scalar (W)} = 0_{Scalar (W)}$
10	8 9 1 2 3	lkr0f	$⊢ (W \in LMod \land G \in F) \to (K (G) = V \leftrightarrow G = V \times \{0_{Scalar (W)}\})$
11	6 7 10	syl2anc	$⊢ φ \to (K (G) = V \leftrightarrow G = V \times \{0_{Scalar (W)}\})$
12	1 8 9 4 5 6	ldual0v	$⊢ φ \to \underset{˙}{0} = V \times \{0_{Scalar (W)}\}$
13	12	eqeq2d	$⊢ φ \to (G = \underset{˙}{0} \leftrightarrow G = V \times \{0_{Scalar (W)}\})$
14	11 13	bitr4d	$⊢ φ \to (K (G) = V \leftrightarrow G = \underset{˙}{0})$

Metamath Proof Explorer