Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-lshyp Structured version   Visualization version   GIF version

Definition df-lshyp 35993
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 that the full space. (Contributed by NM, 29-Jun-2014.)
Assertion
Ref Expression
df-lshyp LSHyp = (𝑤 ∈ V ↦ {𝑠 ∈ (LSubSp‘𝑤) ∣ (𝑠 ≠ (Base‘𝑤) ∧ ∃𝑣 ∈ (Base‘𝑤)((LSpan‘𝑤)‘(𝑠 ∪ {𝑣})) = (Base‘𝑤))})
Distinct variable group:   𝑣,𝑠,𝑤

Detailed syntax breakdown of Definition df-lshyp
StepHypRef Expression
1 clsh 35991 . 2 class LSHyp
2 vw . . 3 setvar 𝑤
3 cvv 3492 . . 3 class V
4 vs . . . . . . 7 setvar 𝑠
54cv 1527 . . . . . 6 class 𝑠
62cv 1527 . . . . . . 7 class 𝑤
7 cbs 16471 . . . . . . 7 class Base
86, 7cfv 6348 . . . . . 6 class (Base‘𝑤)
95, 8wne 3013 . . . . 5 wff 𝑠 ≠ (Base‘𝑤)
10 vv . . . . . . . . . . 11 setvar 𝑣
1110cv 1527 . . . . . . . . . 10 class 𝑣
1211csn 4557 . . . . . . . . 9 class {𝑣}
135, 12cun 3931 . . . . . . . 8 class (𝑠 ∪ {𝑣})
14 clspn 19672 . . . . . . . . 9 class LSpan
156, 14cfv 6348 . . . . . . . 8 class (LSpan‘𝑤)
1613, 15cfv 6348 . . . . . . 7 class ((LSpan‘𝑤)‘(𝑠 ∪ {𝑣}))
1716, 8wceq 1528 . . . . . 6 wff ((LSpan‘𝑤)‘(𝑠 ∪ {𝑣})) = (Base‘𝑤)
1817, 10, 8wrex 3136 . . . . 5 wff 𝑣 ∈ (Base‘𝑤)((LSpan‘𝑤)‘(𝑠 ∪ {𝑣})) = (Base‘𝑤)
199, 18wa 396 . . . 4 wff (𝑠 ≠ (Base‘𝑤) ∧ ∃𝑣 ∈ (Base‘𝑤)((LSpan‘𝑤)‘(𝑠 ∪ {𝑣})) = (Base‘𝑤))
20 clss 19632 . . . . 5 class LSubSp
216, 20cfv 6348 . . . 4 class (LSubSp‘𝑤)
2219, 4, 21crab 3139 . . 3 class {𝑠 ∈ (LSubSp‘𝑤) ∣ (𝑠 ≠ (Base‘𝑤) ∧ ∃𝑣 ∈ (Base‘𝑤)((LSpan‘𝑤)‘(𝑠 ∪ {𝑣})) = (Base‘𝑤))}
232, 3, 22cmpt 5137 . 2 class (𝑤 ∈ V ↦ {𝑠 ∈ (LSubSp‘𝑤) ∣ (𝑠 ≠ (Base‘𝑤) ∧ ∃𝑣 ∈ (Base‘𝑤)((LSpan‘𝑤)‘(𝑠 ∪ {𝑣})) = (Base‘𝑤))})
241, 23wceq 1528 1 wff LSHyp = (𝑤 ∈ V ↦ {𝑠 ∈ (LSubSp‘𝑤) ∣ (𝑠 ≠ (Base‘𝑤) ∧ ∃𝑣 ∈ (Base‘𝑤)((LSpan‘𝑤)‘(𝑠 ∪ {𝑣})) = (Base‘𝑤))})
Colors of variables: wff setvar class
This definition is referenced by:  lshpset  35994
  Copyright terms: Public domain W3C validator