lduallkr3

Description: The kernels of nonzero functionals are hyperplanes. (Contributed by NM, 22-Feb-2015)

	Ref	Expression
Hypotheses	lduallkr3.h	$⊢ H = LSHyp (W)$
	lduallkr3.f	$⊢ F = LFnl (W)$
	lduallkr3.k	$⊢ K = LKer (W)$
	lduallkr3.d	$⊢ D = LDual (W)$
	lduallkr3.o	$⊢ \underset{˙}{0} = 0_{D}$
	lduallkr3.w	$⊢ φ \to W \in LVec$
	lduallkr3.g	$⊢ φ \to G \in F$
Assertion	lduallkr3	$⊢ φ \to (K (G) \in H \leftrightarrow G \neq \underset{˙}{0})$

Step	Hyp	Ref	Expression
1		lduallkr3.h	$⊢ H = LSHyp (W)$
2		lduallkr3.f	$⊢ F = LFnl (W)$
3		lduallkr3.k	$⊢ K = LKer (W)$
4		lduallkr3.d	$⊢ D = LDual (W)$
5		lduallkr3.o	$⊢ \underset{˙}{0} = 0_{D}$
6		lduallkr3.w	$⊢ φ \to W \in LVec$
7		lduallkr3.g	$⊢ φ \to G \in F$
8		eqid	$⊢ {Base}_{W} = {Base}_{W}$
9		eqid	$⊢ Scalar (W) = Scalar (W)$
10		eqid	$⊢ 0_{Scalar (W)} = 0_{Scalar (W)}$
11	8 9 10 1 2 3 6 7	lkrshp3	$⊢ φ \to (K (G) \in H \leftrightarrow G \neq {Base}_{W} \times \{0_{Scalar (W)}\})$
12		lveclmod	$⊢ W \in LVec \to W \in LMod$
13	6 12	syl	$⊢ φ \to W \in LMod$
14	8 9 10 4 5 13	ldual0v	$⊢ φ \to \underset{˙}{0} = {Base}_{W} \times \{0_{Scalar (W)}\}$
15	14	neeq2d	$⊢ φ \to (G \neq \underset{˙}{0} \leftrightarrow G \neq {Base}_{W} \times \{0_{Scalar (W)}\})$
16	11 15	bitr4d	$⊢ φ \to (K (G) \in H \leftrightarrow G \neq \underset{˙}{0})$

Metamath Proof Explorer