Metamath Proof Explorer

Definition 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 ∈ V ⟼ s ∈ LSubSp ⁡ w | s ≠ Base w ∧ ∃ v ∈ Base w LSpan ⁡ w ⁡ s ∪ 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 ≠ 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 ∪ v
17 16 13 cfv class LSpan ⁡ w ⁡ s ∪ v
18 17 9 wceq wff LSpan ⁡ w ⁡ s ∪ v = Base w
19 18 11 9 wrex wff ∃ v ∈ Base w LSpan ⁡ w ⁡ s ∪ v = Base w
20 10 19 wa wff s ≠ Base w ∧ ∃ v ∈ Base w LSpan ⁡ w ⁡ s ∪ v = Base w
21 20 3 6 crab class s ∈ LSubSp ⁡ w | s ≠ Base w ∧ ∃ v ∈ Base w LSpan ⁡ w ⁡ s ∪ v = Base w
22 1 2 21 cmpt class w ∈ V ⟼ s ∈ LSubSp ⁡ w | s ≠ Base w ∧ ∃ v ∈ Base w LSpan ⁡ w ⁡ s ∪ v = Base w
23 0 22 wceq wff LSHyp = w ∈ V ⟼ s ∈ LSubSp ⁡ w | s ≠ Base w ∧ ∃ v ∈ Base w LSpan ⁡ w ⁡ s ∪ v = Base w