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 18697
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 18696 . 2 class LSubSp
2 vw . . 3 setvar 𝑤
3 cvv 3169 . . 3 class V
4 vx . . . . . . . . . . 11 setvar 𝑥
54cv 1473 . . . . . . . . . 10 class 𝑥
6 va . . . . . . . . . . 11 setvar 𝑎
76cv 1473 . . . . . . . . . 10 class 𝑎
82cv 1473 . . . . . . . . . . 11 class 𝑤
9 cvsca 15715 . . . . . . . . . . 11 class ·𝑠
108, 9cfv 5787 . . . . . . . . . 10 class ( ·𝑠𝑤)
115, 7, 10co 6524 . . . . . . . . 9 class (𝑥( ·𝑠𝑤)𝑎)
12 vb . . . . . . . . . 10 setvar 𝑏
1312cv 1473 . . . . . . . . 9 class 𝑏
14 cplusg 15711 . . . . . . . . . 10 class +g
158, 14cfv 5787 . . . . . . . . 9 class (+g𝑤)
1611, 13, 15co 6524 . . . . . . . 8 class ((𝑥( ·𝑠𝑤)𝑎)(+g𝑤)𝑏)
17 vs . . . . . . . . 9 setvar 𝑠
1817cv 1473 . . . . . . . 8 class 𝑠
1916, 18wcel 1976 . . . . . . 7 wff ((𝑥( ·𝑠𝑤)𝑎)(+g𝑤)𝑏) ∈ 𝑠
2019, 12, 18wral 2892 . . . . . 6 wff 𝑏𝑠 ((𝑥( ·𝑠𝑤)𝑎)(+g𝑤)𝑏) ∈ 𝑠
2120, 6, 18wral 2892 . . . . 5 wff 𝑎𝑠𝑏𝑠 ((𝑥( ·𝑠𝑤)𝑎)(+g𝑤)𝑏) ∈ 𝑠
22 csca 15714 . . . . . . 7 class Scalar
238, 22cfv 5787 . . . . . 6 class (Scalar‘𝑤)
24 cbs 15638 . . . . . 6 class Base
2523, 24cfv 5787 . . . . 5 class (Base‘(Scalar‘𝑤))
2621, 4, 25wral 2892 . . . 4 wff 𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎𝑠𝑏𝑠 ((𝑥( ·𝑠𝑤)𝑎)(+g𝑤)𝑏) ∈ 𝑠
278, 24cfv 5787 . . . . . 6 class (Base‘𝑤)
2827cpw 4104 . . . . 5 class 𝒫 (Base‘𝑤)
29 c0 3870 . . . . . 6 class
3029csn 4121 . . . . 5 class {∅}
3128, 30cdif 3533 . . . 4 class (𝒫 (Base‘𝑤) ∖ {∅})
3226, 17, 31crab 2896 . . 3 class {𝑠 ∈ (𝒫 (Base‘𝑤) ∖ {∅}) ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎𝑠𝑏𝑠 ((𝑥( ·𝑠𝑤)𝑎)(+g𝑤)𝑏) ∈ 𝑠}
332, 3, 32cmpt 4634 . 2 class (𝑤 ∈ V ↦ {𝑠 ∈ (𝒫 (Base‘𝑤) ∖ {∅}) ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎𝑠𝑏𝑠 ((𝑥( ·𝑠𝑤)𝑎)(+g𝑤)𝑏) ∈ 𝑠})
341, 33wceq 1474 1 wff LSubSp = (𝑤 ∈ V ↦ {𝑠 ∈ (𝒫 (Base‘𝑤) ∖ {∅}) ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎𝑠𝑏𝑠 ((𝑥( ·𝑠𝑤)𝑎)(+g𝑤)𝑏) ∈ 𝑠})
Colors of variables: wff setvar class
This definition is referenced by:  lssset  18698
  Copyright terms: Public domain W3C validator