MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-lss Structured version   Visualization version   GIF version

Definition df-lss 19137
Description: Define the set of linear subspaces of a left module or left vector space. (Contributed by NM, 8-Dec-2013.)
Assertion
Ref Expression
df-lss LSubSp = (𝑤 ∈ V ↦ {𝑠 ∈ (𝒫 (Base‘𝑤) ∖ {∅}) ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎𝑠𝑏𝑠 ((𝑥( ·𝑠𝑤)𝑎)(+g𝑤)𝑏) ∈ 𝑠})
Distinct variable group:   𝑎,𝑏,𝑠,𝑥,𝑤

Detailed syntax breakdown of Definition df-lss
StepHypRef Expression
1 clss 19136 . 2 class LSubSp
2 vw . . 3 setvar 𝑤
3 cvv 3391 . . 3 class V
4 vx . . . . . . . . . . 11 setvar 𝑥
54cv 1636 . . . . . . . . . 10 class 𝑥
6 va . . . . . . . . . . 11 setvar 𝑎
76cv 1636 . . . . . . . . . 10 class 𝑎
82cv 1636 . . . . . . . . . . 11 class 𝑤
9 cvsca 16157 . . . . . . . . . . 11 class ·𝑠
108, 9cfv 6101 . . . . . . . . . 10 class ( ·𝑠𝑤)
115, 7, 10co 6874 . . . . . . . . 9 class (𝑥( ·𝑠𝑤)𝑎)
12 vb . . . . . . . . . 10 setvar 𝑏
1312cv 1636 . . . . . . . . 9 class 𝑏
14 cplusg 16153 . . . . . . . . . 10 class +g
158, 14cfv 6101 . . . . . . . . 9 class (+g𝑤)
1611, 13, 15co 6874 . . . . . . . 8 class ((𝑥( ·𝑠𝑤)𝑎)(+g𝑤)𝑏)
17 vs . . . . . . . . 9 setvar 𝑠
1817cv 1636 . . . . . . . 8 class 𝑠
1916, 18wcel 2156 . . . . . . 7 wff ((𝑥( ·𝑠𝑤)𝑎)(+g𝑤)𝑏) ∈ 𝑠
2019, 12, 18wral 3096 . . . . . 6 wff 𝑏𝑠 ((𝑥( ·𝑠𝑤)𝑎)(+g𝑤)𝑏) ∈ 𝑠
2120, 6, 18wral 3096 . . . . 5 wff 𝑎𝑠𝑏𝑠 ((𝑥( ·𝑠𝑤)𝑎)(+g𝑤)𝑏) ∈ 𝑠
22 csca 16156 . . . . . . 7 class Scalar
238, 22cfv 6101 . . . . . 6 class (Scalar‘𝑤)
24 cbs 16068 . . . . . 6 class Base
2523, 24cfv 6101 . . . . 5 class (Base‘(Scalar‘𝑤))
2621, 4, 25wral 3096 . . . 4 wff 𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎𝑠𝑏𝑠 ((𝑥( ·𝑠𝑤)𝑎)(+g𝑤)𝑏) ∈ 𝑠
278, 24cfv 6101 . . . . . 6 class (Base‘𝑤)
2827cpw 4351 . . . . 5 class 𝒫 (Base‘𝑤)
29 c0 4116 . . . . . 6 class
3029csn 4370 . . . . 5 class {∅}
3128, 30cdif 3766 . . . 4 class (𝒫 (Base‘𝑤) ∖ {∅})
3226, 17, 31crab 3100 . . 3 class {𝑠 ∈ (𝒫 (Base‘𝑤) ∖ {∅}) ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎𝑠𝑏𝑠 ((𝑥( ·𝑠𝑤)𝑎)(+g𝑤)𝑏) ∈ 𝑠}
332, 3, 32cmpt 4923 . 2 class (𝑤 ∈ V ↦ {𝑠 ∈ (𝒫 (Base‘𝑤) ∖ {∅}) ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎𝑠𝑏𝑠 ((𝑥( ·𝑠𝑤)𝑎)(+g𝑤)𝑏) ∈ 𝑠})
341, 33wceq 1637 1 wff LSubSp = (𝑤 ∈ V ↦ {𝑠 ∈ (𝒫 (Base‘𝑤) ∖ {∅}) ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎𝑠𝑏𝑠 ((𝑥( ·𝑠𝑤)𝑎)(+g𝑤)𝑏) ∈ 𝑠})
Colors of variables: wff setvar class
This definition is referenced by:  lssset  19138
  Copyright terms: Public domain W3C validator