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

Definition df-lss 18754
 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 18753 . 2 class LSubSp
2 vw . . 3 setvar 𝑤
3 cvv 3173 . . 3 class V
4 vx . . . . . . . . . . 11 setvar 𝑥
54cv 1474 . . . . . . . . . 10 class 𝑥
6 va . . . . . . . . . . 11 setvar 𝑎
76cv 1474 . . . . . . . . . 10 class 𝑎
82cv 1474 . . . . . . . . . . 11 class 𝑤
9 cvsca 15772 . . . . . . . . . . 11 class ·𝑠
108, 9cfv 5804 . . . . . . . . . 10 class ( ·𝑠𝑤)
115, 7, 10co 6549 . . . . . . . . 9 class (𝑥( ·𝑠𝑤)𝑎)
12 vb . . . . . . . . . 10 setvar 𝑏
1312cv 1474 . . . . . . . . 9 class 𝑏
14 cplusg 15768 . . . . . . . . . 10 class +g
158, 14cfv 5804 . . . . . . . . 9 class (+g𝑤)
1611, 13, 15co 6549 . . . . . . . 8 class ((𝑥( ·𝑠𝑤)𝑎)(+g𝑤)𝑏)
17 vs . . . . . . . . 9 setvar 𝑠
1817cv 1474 . . . . . . . 8 class 𝑠
1916, 18wcel 1977 . . . . . . 7 wff ((𝑥( ·𝑠𝑤)𝑎)(+g𝑤)𝑏) ∈ 𝑠
2019, 12, 18wral 2896 . . . . . 6 wff 𝑏𝑠 ((𝑥( ·𝑠𝑤)𝑎)(+g𝑤)𝑏) ∈ 𝑠
2120, 6, 18wral 2896 . . . . 5 wff 𝑎𝑠𝑏𝑠 ((𝑥( ·𝑠𝑤)𝑎)(+g𝑤)𝑏) ∈ 𝑠
22 csca 15771 . . . . . . 7 class Scalar
238, 22cfv 5804 . . . . . 6 class (Scalar‘𝑤)
24 cbs 15695 . . . . . 6 class Base
2523, 24cfv 5804 . . . . 5 class (Base‘(Scalar‘𝑤))
2621, 4, 25wral 2896 . . . 4 wff 𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎𝑠𝑏𝑠 ((𝑥( ·𝑠𝑤)𝑎)(+g𝑤)𝑏) ∈ 𝑠
278, 24cfv 5804 . . . . . 6 class (Base‘𝑤)
2827cpw 4108 . . . . 5 class 𝒫 (Base‘𝑤)
29 c0 3874 . . . . . 6 class
3029csn 4125 . . . . 5 class {∅}
3128, 30cdif 3537 . . . 4 class (𝒫 (Base‘𝑤) ∖ {∅})
3226, 17, 31crab 2900 . . 3 class {𝑠 ∈ (𝒫 (Base‘𝑤) ∖ {∅}) ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎𝑠𝑏𝑠 ((𝑥( ·𝑠𝑤)𝑎)(+g𝑤)𝑏) ∈ 𝑠}
332, 3, 32cmpt 4643 . 2 class (𝑤 ∈ V ↦ {𝑠 ∈ (𝒫 (Base‘𝑤) ∖ {∅}) ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎𝑠𝑏𝑠 ((𝑥( ·𝑠𝑤)𝑎)(+g𝑤)𝑏) ∈ 𝑠})
341, 33wceq 1475 1 wff LSubSp = (𝑤 ∈ V ↦ {𝑠 ∈ (𝒫 (Base‘𝑤) ∖ {∅}) ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎𝑠𝑏𝑠 ((𝑥( ·𝑠𝑤)𝑎)(+g𝑤)𝑏) ∈ 𝑠})
 Colors of variables: wff setvar class This definition is referenced by:  lssset  18755
 Copyright terms: Public domain W3C validator