lkrshp3

Description: The kernels of nonzero functionals are hyperplanes. (Contributed by NM, 17-Jul-2014)

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

Proof

Step	Hyp	Ref	Expression
1		lkrshp3.v	$⊢ V = {Base}_{W}$
2		lkrshp3.d	$⊢ D = Scalar (W)$
3		lkrshp3.o	$⊢ \underset{˙}{0} = 0_{D}$
4		lkrshp3.h	$⊢ H = LSHyp (W)$
5		lkrshp3.f	$⊢ F = LFnl (W)$
6		lkrshp3.k	$⊢ K = LKer (W)$
7		lkrshp3.w	$⊢ φ \to W \in LVec$
8		lkrshp3.g	$⊢ φ \to G \in F$
9		lveclmod	$⊢ W \in LVec \to W \in LMod$
10	7 9	syl	$⊢ φ \to W \in LMod$
11	10	adantr	$⊢ (φ \land K (G) \in H) \to W \in LMod$
12		simpr	$⊢ (φ \land K (G) \in H) \to K (G) \in H$
13	1 4 11 12	lshpne	$⊢ (φ \land K (G) \in H) \to K (G) \neq V$
14	2 3 1 5 6	lkr0f	$⊢ (W \in LMod \land G \in F) \to (K (G) = V \leftrightarrow G = V \times \{\underset{˙}{0}\})$
15	10 8 14	syl2anc	$⊢ φ \to (K (G) = V \leftrightarrow G = V \times \{\underset{˙}{0}\})$
16	15	adantr	$⊢ (φ \land K (G) \in H) \to (K (G) = V \leftrightarrow G = V \times \{\underset{˙}{0}\})$
17	16	necon3bid	$⊢ (φ \land K (G) \in H) \to (K (G) \neq V \leftrightarrow G \neq V \times \{\underset{˙}{0}\})$
18	13 17	mpbid	$⊢ (φ \land K (G) \in H) \to G \neq V \times \{\underset{˙}{0}\}$
19	7	adantr	$⊢ (φ \land G \neq V \times \{\underset{˙}{0}\}) \to W \in LVec$
20	8	adantr	$⊢ (φ \land G \neq V \times \{\underset{˙}{0}\}) \to G \in F$
21		simpr	$⊢ (φ \land G \neq V \times \{\underset{˙}{0}\}) \to G \neq V \times \{\underset{˙}{0}\}$
22	1 2 3 4 5 6	lkrshp	$⊢ (W \in LVec \land G \in F \land G \neq V \times \{\underset{˙}{0}\}) \to K (G) \in H$
23	19 20 21 22	syl3anc	$⊢ (φ \land G \neq V \times \{\underset{˙}{0}\}) \to K (G) \in H$
24	18 23	impbida	$⊢ φ \to (K (G) \in H \leftrightarrow G \neq V \times \{\underset{˙}{0}\})$

Metamath Proof Explorer

Theorem lkrshp3

Proof