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 20909
Description: Define the set of linear subspaces of a left module or left vector space: a linear subspace of a left module or left vector space is a non-empty subset of the base set of the left module/vector space with a closure condition on vector addition and scalar multiplication. (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 20908 . 2 class LSubSp
2 vw . . 3 setvar 𝑤
3 cvv 3462 . . 3 class V
4 vx . . . . . . . . . . 11 setvar 𝑥
54cv 1533 . . . . . . . . . 10 class 𝑥
6 va . . . . . . . . . . 11 setvar 𝑎
76cv 1533 . . . . . . . . . 10 class 𝑎
82cv 1533 . . . . . . . . . . 11 class 𝑤
9 cvsca 17270 . . . . . . . . . . 11 class ·𝑠
108, 9cfv 6554 . . . . . . . . . 10 class ( ·𝑠𝑤)
115, 7, 10co 7424 . . . . . . . . 9 class (𝑥( ·𝑠𝑤)𝑎)
12 vb . . . . . . . . . 10 setvar 𝑏
1312cv 1533 . . . . . . . . 9 class 𝑏
14 cplusg 17266 . . . . . . . . . 10 class +g
158, 14cfv 6554 . . . . . . . . 9 class (+g𝑤)
1611, 13, 15co 7424 . . . . . . . 8 class ((𝑥( ·𝑠𝑤)𝑎)(+g𝑤)𝑏)
17 vs . . . . . . . . 9 setvar 𝑠
1817cv 1533 . . . . . . . 8 class 𝑠
1916, 18wcel 2099 . . . . . . 7 wff ((𝑥( ·𝑠𝑤)𝑎)(+g𝑤)𝑏) ∈ 𝑠
2019, 12, 18wral 3051 . . . . . 6 wff 𝑏𝑠 ((𝑥( ·𝑠𝑤)𝑎)(+g𝑤)𝑏) ∈ 𝑠
2120, 6, 18wral 3051 . . . . 5 wff 𝑎𝑠𝑏𝑠 ((𝑥( ·𝑠𝑤)𝑎)(+g𝑤)𝑏) ∈ 𝑠
22 csca 17269 . . . . . . 7 class Scalar
238, 22cfv 6554 . . . . . 6 class (Scalar‘𝑤)
24 cbs 17213 . . . . . 6 class Base
2523, 24cfv 6554 . . . . 5 class (Base‘(Scalar‘𝑤))
2621, 4, 25wral 3051 . . . 4 wff 𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎𝑠𝑏𝑠 ((𝑥( ·𝑠𝑤)𝑎)(+g𝑤)𝑏) ∈ 𝑠
278, 24cfv 6554 . . . . . 6 class (Base‘𝑤)
2827cpw 4607 . . . . 5 class 𝒫 (Base‘𝑤)
29 c0 4325 . . . . . 6 class
3029csn 4633 . . . . 5 class {∅}
3128, 30cdif 3944 . . . 4 class (𝒫 (Base‘𝑤) ∖ {∅})
3226, 17, 31crab 3419 . . 3 class {𝑠 ∈ (𝒫 (Base‘𝑤) ∖ {∅}) ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎𝑠𝑏𝑠 ((𝑥( ·𝑠𝑤)𝑎)(+g𝑤)𝑏) ∈ 𝑠}
332, 3, 32cmpt 5236 . 2 class (𝑤 ∈ V ↦ {𝑠 ∈ (𝒫 (Base‘𝑤) ∖ {∅}) ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎𝑠𝑏𝑠 ((𝑥( ·𝑠𝑤)𝑎)(+g𝑤)𝑏) ∈ 𝑠})
341, 33wceq 1534 1 wff LSubSp = (𝑤 ∈ V ↦ {𝑠 ∈ (𝒫 (Base‘𝑤) ∖ {∅}) ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎𝑠𝑏𝑠 ((𝑥( ·𝑠𝑤)𝑎)(+g𝑤)𝑏) ∈ 𝑠})
Colors of variables: wff setvar class
This definition is referenced by:  lssset  20910
  Copyright terms: Public domain W3C validator