lkrshp

Description: The kernel of a nonzero functional is a hyperplane. (Contributed by NM, 29-Jun-2014)

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

Proof

Step	Hyp	Ref	Expression
1		lkrshp.v	$⊢ V = {Base}_{W}$
2		lkrshp.d	$⊢ D = Scalar (W)$
3		lkrshp.z	$⊢ \underset{˙}{0} = 0_{D}$
4		lkrshp.h	$⊢ H = LSHyp (W)$
5		lkrshp.f	$⊢ F = LFnl (W)$
6		lkrshp.k	$⊢ K = LKer (W)$
7		lveclmod	$⊢ W \in LVec \to W \in LMod$
8	7	3ad2ant1	$⊢ (W \in LVec \land G \in F \land G \neq V \times \{\underset{˙}{0}\}) \to W \in LMod$
9		simp2	$⊢ (W \in LVec \land G \in F \land G \neq V \times \{\underset{˙}{0}\}) \to G \in F$
10		eqid	$⊢ LSubSp (W) = LSubSp (W)$
11	5 6 10	lkrlss	$⊢ (W \in LMod \land G \in F) \to K (G) \in LSubSp (W)$
12	8 9 11	syl2anc	$⊢ (W \in LVec \land G \in F \land G \neq V \times \{\underset{˙}{0}\}) \to K (G) \in LSubSp (W)$
13		simp3	$⊢ (W \in LVec \land G \in F \land G \neq V \times \{\underset{˙}{0}\}) \to G \neq V \times \{\underset{˙}{0}\}$
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	8 9 14	syl2anc	$⊢ (W \in LVec \land G \in F \land G \neq V \times \{\underset{˙}{0}\}) \to (K (G) = V \leftrightarrow G = V \times \{\underset{˙}{0}\})$
16	15	necon3bid	$⊢ (W \in LVec \land G \in F \land G \neq V \times \{\underset{˙}{0}\}) \to (K (G) \neq V \leftrightarrow G \neq V \times \{\underset{˙}{0}\})$
17	13 16	mpbird	$⊢ (W \in LVec \land G \in F \land G \neq V \times \{\underset{˙}{0}\}) \to K (G) \neq V$
18		eqid	$⊢ 1_{D} = 1_{D}$
19	2 3 18 1 5	lfl1	$⊢ (W \in LVec \land G \in F \land G \neq V \times \{\underset{˙}{0}\}) \to \exists v \in V G (v) = 1_{D}$
20		simp11	$⊢ ((W \in LVec \land G \in F \land G \neq V \times \{\underset{˙}{0}\}) \land v \in V \land G (v) = 1_{D}) \to W \in LVec$
21		simp2	$⊢ ((W \in LVec \land G \in F \land G \neq V \times \{\underset{˙}{0}\}) \land v \in V \land G (v) = 1_{D}) \to v \in V$
22		simp12	$⊢ ((W \in LVec \land G \in F \land G \neq V \times \{\underset{˙}{0}\}) \land v \in V \land G (v) = 1_{D}) \to G \in F$
23		simp3	$⊢ ((W \in LVec \land G \in F \land G \neq V \times \{\underset{˙}{0}\}) \land v \in V \land G (v) = 1_{D}) \to G (v) = 1_{D}$
24	2	lvecdrng	$⊢ W \in LVec \to D \in DivRing$
25	3 18	drngunz	$⊢ D \in DivRing \to 1_{D} \neq \underset{˙}{0}$
26	20 24 25	3syl	$⊢ ((W \in LVec \land G \in F \land G \neq V \times \{\underset{˙}{0}\}) \land v \in V \land G (v) = 1_{D}) \to 1_{D} \neq \underset{˙}{0}$
27	23 26	eqnetrd	$⊢ ((W \in LVec \land G \in F \land G \neq V \times \{\underset{˙}{0}\}) \land v \in V \land G (v) = 1_{D}) \to G (v) \neq \underset{˙}{0}$
28		simpl11	$⊢ (((W \in LVec \land G \in F \land G \neq V \times \{\underset{˙}{0}\}) \land v \in V \land G (v) = 1_{D}) \land v \in K (G)) \to W \in LVec$
29		simpl12	$⊢ (((W \in LVec \land G \in F \land G \neq V \times \{\underset{˙}{0}\}) \land v \in V \land G (v) = 1_{D}) \land v \in K (G)) \to G \in F$
30		simpr	$⊢ (((W \in LVec \land G \in F \land G \neq V \times \{\underset{˙}{0}\}) \land v \in V \land G (v) = 1_{D}) \land v \in K (G)) \to v \in K (G)$
31	2 3 5 6	lkrf0	$⊢ (W \in LVec \land G \in F \land v \in K (G)) \to G (v) = \underset{˙}{0}$
32	28 29 30 31	syl3anc	$⊢ (((W \in LVec \land G \in F \land G \neq V \times \{\underset{˙}{0}\}) \land v \in V \land G (v) = 1_{D}) \land v \in K (G)) \to G (v) = \underset{˙}{0}$
33	32	ex	$⊢ ((W \in LVec \land G \in F \land G \neq V \times \{\underset{˙}{0}\}) \land v \in V \land G (v) = 1_{D}) \to (v \in K (G) \to G (v) = \underset{˙}{0})$
34	33	necon3ad	$⊢ ((W \in LVec \land G \in F \land G \neq V \times \{\underset{˙}{0}\}) \land v \in V \land G (v) = 1_{D}) \to (G (v) \neq \underset{˙}{0} \to \neg v \in K (G))$
35	27 34	mpd	$⊢ ((W \in LVec \land G \in F \land G \neq V \times \{\underset{˙}{0}\}) \land v \in V \land G (v) = 1_{D}) \to \neg v \in K (G)$
36		eqid	$⊢ LSpan (W) = LSpan (W)$
37	1 36 5 6	lkrlsp3	$⊢ (W \in LVec \land (v \in V \land G \in F) \land \neg v \in K (G)) \to LSpan (W) (K (G) \cup \{v\}) = V$
38	20 21 22 35 37	syl121anc	$⊢ ((W \in LVec \land G \in F \land G \neq V \times \{\underset{˙}{0}\}) \land v \in V \land G (v) = 1_{D}) \to LSpan (W) (K (G) \cup \{v\}) = V$
39	38	3expia	$⊢ ((W \in LVec \land G \in F \land G \neq V \times \{\underset{˙}{0}\}) \land v \in V) \to (G (v) = 1_{D} \to LSpan (W) (K (G) \cup \{v\}) = V)$
40	39	reximdva	$⊢ (W \in LVec \land G \in F \land G \neq V \times \{\underset{˙}{0}\}) \to (\exists v \in V G (v) = 1_{D} \to \exists v \in V LSpan (W) (K (G) \cup \{v\}) = V)$
41	19 40	mpd	$⊢ (W \in LVec \land G \in F \land G \neq V \times \{\underset{˙}{0}\}) \to \exists v \in V LSpan (W) (K (G) \cup \{v\}) = V$
42	1 36 10 4	islshp	$⊢ W \in LVec \to (K (G) \in H \leftrightarrow (K (G) \in LSubSp (W) \land K (G) \neq V \land \exists v \in V LSpan (W) (K (G) \cup \{v\}) = V))$
43	42	3ad2ant1	$⊢ (W \in LVec \land G \in F \land G \neq V \times \{\underset{˙}{0}\}) \to (K (G) \in H \leftrightarrow (K (G) \in LSubSp (W) \land K (G) \neq V \land \exists v \in V LSpan (W) (K (G) \cup \{v\}) = V))$
44	12 17 41 43	mpbir3and	$⊢ (W \in LVec \land G \in F \land G \neq V \times \{\underset{˙}{0}\}) \to K (G) \in H$

Metamath Proof Explorer

Theorem lkrshp

Proof