df-lshyp

Description: Define the set of all hyperplanes of a left module or left vector space. Also called co-atoms, these are subspaces that are one dimension less than the full space. (Contributed by NM, 29-Jun-2014)

		Ref	Expression
	Assertion	df-lshyp	$⊢ LSHyp = (w \in V ⟼ \{s \in LSubSp (w) \| (s \neq {Base}_{w} \land \exists v \in {Base}_{w} LSpan (w) (s \cup \{v\}) = {Base}_{w})\})$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clsh	$class LSHyp$
1		vw	$setvar w$
2		cvv	$class V$
3		vs	$setvar s$
4		clss	$class LSubSp$
5	1	cv	$setvar w$
6	5 4	cfv	$class LSubSp (w)$
7	3	cv	$setvar s$
8		cbs	$class Base$
9	5 8	cfv	$class {Base}_{w}$
10	7 9	wne	$wff s \neq {Base}_{w}$
11		vv	$setvar v$
12		clspn	$class LSpan$
13	5 12	cfv	$class LSpan (w)$
14	11	cv	$setvar v$
15	14	csn	$class \{v\}$
16	7 15	cun	$class (s \cup \{v\})$
17	16 13	cfv	$class LSpan (w) (s \cup \{v\})$
18	17 9	wceq	$wff LSpan (w) (s \cup \{v\}) = {Base}_{w}$
19	18 11 9	wrex	$wff \exists v \in {Base}_{w} LSpan (w) (s \cup \{v\}) = {Base}_{w}$
20	10 19	wa	$wff (s \neq {Base}_{w} \land \exists v \in {Base}_{w} LSpan (w) (s \cup \{v\}) = {Base}_{w})$
21	20 3 6	crab	$class \{s \in LSubSp (w) \| (s \neq {Base}_{w} \land \exists v \in {Base}_{w} LSpan (w) (s \cup \{v\}) = {Base}_{w})\}$
22	1 2 21	cmpt	$class (w \in V ⟼ \{s \in LSubSp (w) \| (s \neq {Base}_{w} \land \exists v \in {Base}_{w} LSpan (w) (s \cup \{v\}) = {Base}_{w})\})$
23	0 22	wceq	$wff LSHyp = (w \in V ⟼ \{s \in LSubSp (w) \| (s \neq {Base}_{w} \land \exists v \in {Base}_{w} LSpan (w) (s \cup \{v\}) = {Base}_{w})\})$

Metamath Proof Explorer

Definition df-lshyp

Detailed syntax breakdown