lshpset2N

Description: The set of all hyperplanes of a left module or left vector space equals the set of all kernels of nonzero functionals. (Contributed by NM, 17-Jul-2014) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		lshpset2.v	$⊢ V = {Base}_{W}$
2		lshpset2.d	$⊢ D = Scalar (W)$
3		lshpset2.z	$⊢ \underset{˙}{0} = 0_{D}$
4		lshpset2.h	$⊢ H = LSHyp (W)$
5		lshpset2.f	$⊢ F = LFnl (W)$
6		lshpset2.k	$⊢ K = LKer (W)$
7	4 5 6	lshpkrex	$⊢ (W \in LVec \land s \in H) \to \exists g \in F K (g) = s$
8		eleq1	$⊢ K (g) = s \to (K (g) \in H \leftrightarrow s \in H)$
9	8	biimparc	$⊢ (s \in H \land K (g) = s) \to K (g) \in H$
10	9	adantll	$⊢ ((W \in LVec \land s \in H) \land K (g) = s) \to K (g) \in H$
11	10	adantlr	$⊢ (((W \in LVec \land s \in H) \land g \in F) \land K (g) = s) \to K (g) \in H$
12		simplll	$⊢ (((W \in LVec \land s \in H) \land g \in F) \land K (g) = s) \to W \in LVec$
13		simplr	$⊢ (((W \in LVec \land s \in H) \land g \in F) \land K (g) = s) \to g \in F$
14	1 2 3 4 5 6 12 13	lkrshp3	$⊢ (((W \in LVec \land s \in H) \land g \in F) \land K (g) = s) \to (K (g) \in H \leftrightarrow g \neq V \times \{\underset{˙}{0}\})$
15	11 14	mpbid	$⊢ (((W \in LVec \land s \in H) \land g \in F) \land K (g) = s) \to g \neq V \times \{\underset{˙}{0}\}$
16	15	ex	$⊢ ((W \in LVec \land s \in H) \land g \in F) \to (K (g) = s \to g \neq V \times \{\underset{˙}{0}\})$
17		eqimss2	$⊢ K (g) = s \to s \subseteq K (g)$
18		eqimss	$⊢ K (g) = s \to K (g) \subseteq s$
19	17 18	eqssd	$⊢ K (g) = s \to s = K (g)$
20	19	a1i	$⊢ ((W \in LVec \land s \in H) \land g \in F) \to (K (g) = s \to s = K (g))$
21	16 20	jcad	$⊢ ((W \in LVec \land s \in H) \land g \in F) \to (K (g) = s \to (g \neq V \times \{\underset{˙}{0}\} \land s = K (g)))$
22	21	reximdva	$⊢ (W \in LVec \land s \in H) \to (\exists g \in F K (g) = s \to \exists g \in F (g \neq V \times \{\underset{˙}{0}\} \land s = K (g)))$
23	7 22	mpd	$⊢ (W \in LVec \land s \in H) \to \exists g \in F (g \neq V \times \{\underset{˙}{0}\} \land s = K (g))$
24	23	ex	$⊢ W \in LVec \to (s \in H \to \exists g \in F (g \neq V \times \{\underset{˙}{0}\} \land s = K (g)))$
25	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$
26	25	3adant3r	$⊢ (W \in LVec \land g \in F \land (g \neq V \times \{\underset{˙}{0}\} \land s = K (g))) \to K (g) \in H$
27		eqid	$⊢ LSpan (W) = LSpan (W)$
28		eqid	$⊢ LSubSp (W) = LSubSp (W)$
29	1 27 28 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))$
30	29	3ad2ant1	$⊢ (W \in LVec \land g \in F \land (g \neq V \times \{\underset{˙}{0}\} \land s = K (g))) \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))$
31	26 30	mpbid	$⊢ (W \in LVec \land g \in F \land (g \neq V \times \{\underset{˙}{0}\} \land s = K (g))) \to (K (g) \in LSubSp (W) \land K (g) \neq V \land \exists v \in V LSpan (W) (K (g) \cup \{v\}) = V)$
32		eleq1	$⊢ s = K (g) \to (s \in LSubSp (W) \leftrightarrow K (g) \in LSubSp (W))$
33		neeq1	$⊢ s = K (g) \to (s \neq V \leftrightarrow K (g) \neq V)$
34		uneq1	$⊢ s = K (g) \to s \cup \{v\} = K (g) \cup \{v\}$
35	34	fveqeq2d	$⊢ s = K (g) \to (LSpan (W) (s \cup \{v\}) = V \leftrightarrow LSpan (W) (K (g) \cup \{v\}) = V)$
36	35	rexbidv	$⊢ s = K (g) \to (\exists v \in V LSpan (W) (s \cup \{v\}) = V \leftrightarrow \exists v \in V LSpan (W) (K (g) \cup \{v\}) = V)$
37	32 33 36	3anbi123d	$⊢ s = K (g) \to ((s \in LSubSp (W) \land s \neq V \land \exists v \in V LSpan (W) (s \cup \{v\}) = V) \leftrightarrow (K (g) \in LSubSp (W) \land K (g) \neq V \land \exists v \in V LSpan (W) (K (g) \cup \{v\}) = V))$
38	37	adantl	$⊢ (g \neq V \times \{\underset{˙}{0}\} \land s = K (g)) \to ((s \in LSubSp (W) \land s \neq V \land \exists v \in V LSpan (W) (s \cup \{v\}) = V) \leftrightarrow (K (g) \in LSubSp (W) \land K (g) \neq V \land \exists v \in V LSpan (W) (K (g) \cup \{v\}) = V))$
39	38	3ad2ant3	$⊢ (W \in LVec \land g \in F \land (g \neq V \times \{\underset{˙}{0}\} \land s = K (g))) \to ((s \in LSubSp (W) \land s \neq V \land \exists v \in V LSpan (W) (s \cup \{v\}) = V) \leftrightarrow (K (g) \in LSubSp (W) \land K (g) \neq V \land \exists v \in V LSpan (W) (K (g) \cup \{v\}) = V))$
40	31 39	mpbird	$⊢ (W \in LVec \land g \in F \land (g \neq V \times \{\underset{˙}{0}\} \land s = K (g))) \to (s \in LSubSp (W) \land s \neq V \land \exists v \in V LSpan (W) (s \cup \{v\}) = V)$
41	40	rexlimdv3a	$⊢ W \in LVec \to (\exists g \in F (g \neq V \times \{\underset{˙}{0}\} \land s = K (g)) \to (s \in LSubSp (W) \land s \neq V \land \exists v \in V LSpan (W) (s \cup \{v\}) = V))$
42	1 27 28 4	islshp	$⊢ W \in LVec \to (s \in H \leftrightarrow (s \in LSubSp (W) \land s \neq V \land \exists v \in V LSpan (W) (s \cup \{v\}) = V))$
43	41 42	sylibrd	$⊢ W \in LVec \to (\exists g \in F (g \neq V \times \{\underset{˙}{0}\} \land s = K (g)) \to s \in H)$
44	24 43	impbid	$⊢ W \in LVec \to (s \in H \leftrightarrow \exists g \in F (g \neq V \times \{\underset{˙}{0}\} \land s = K (g)))$
45	44	eqabdv	$⊢ W \in LVec \to H = \{s \| \exists g \in F (g \neq V \times \{\underset{˙}{0}\} \land s = K (g))\}$

Metamath Proof Explorer

Theorem lshpset2N

Proof