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 19635
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 19634 . 2 class LSubSp
2 vw . . 3 setvar 𝑤
3 cvv 3495 . . 3 class V
4 vx . . . . . . . . . . 11 setvar 𝑥
54cv 1527 . . . . . . . . . 10 class 𝑥
6 va . . . . . . . . . . 11 setvar 𝑎
76cv 1527 . . . . . . . . . 10 class 𝑎
82cv 1527 . . . . . . . . . . 11 class 𝑤
9 cvsca 16559 . . . . . . . . . . 11 class ·𝑠
108, 9cfv 6349 . . . . . . . . . 10 class ( ·𝑠𝑤)
115, 7, 10co 7145 . . . . . . . . 9 class (𝑥( ·𝑠𝑤)𝑎)
12 vb . . . . . . . . . 10 setvar 𝑏
1312cv 1527 . . . . . . . . 9 class 𝑏
14 cplusg 16555 . . . . . . . . . 10 class +g
158, 14cfv 6349 . . . . . . . . 9 class (+g𝑤)
1611, 13, 15co 7145 . . . . . . . 8 class ((𝑥( ·𝑠𝑤)𝑎)(+g𝑤)𝑏)
17 vs . . . . . . . . 9 setvar 𝑠
1817cv 1527 . . . . . . . 8 class 𝑠
1916, 18wcel 2105 . . . . . . 7 wff ((𝑥( ·𝑠𝑤)𝑎)(+g𝑤)𝑏) ∈ 𝑠
2019, 12, 18wral 3138 . . . . . 6 wff 𝑏𝑠 ((𝑥( ·𝑠𝑤)𝑎)(+g𝑤)𝑏) ∈ 𝑠
2120, 6, 18wral 3138 . . . . 5 wff 𝑎𝑠𝑏𝑠 ((𝑥( ·𝑠𝑤)𝑎)(+g𝑤)𝑏) ∈ 𝑠
22 csca 16558 . . . . . . 7 class Scalar
238, 22cfv 6349 . . . . . 6 class (Scalar‘𝑤)
24 cbs 16473 . . . . . 6 class Base
2523, 24cfv 6349 . . . . 5 class (Base‘(Scalar‘𝑤))
2621, 4, 25wral 3138 . . . 4 wff 𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎𝑠𝑏𝑠 ((𝑥( ·𝑠𝑤)𝑎)(+g𝑤)𝑏) ∈ 𝑠
278, 24cfv 6349 . . . . . 6 class (Base‘𝑤)
2827cpw 4537 . . . . 5 class 𝒫 (Base‘𝑤)
29 c0 4290 . . . . . 6 class
3029csn 4559 . . . . 5 class {∅}
3128, 30cdif 3932 . . . 4 class (𝒫 (Base‘𝑤) ∖ {∅})
3226, 17, 31crab 3142 . . 3 class {𝑠 ∈ (𝒫 (Base‘𝑤) ∖ {∅}) ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎𝑠𝑏𝑠 ((𝑥( ·𝑠𝑤)𝑎)(+g𝑤)𝑏) ∈ 𝑠}
332, 3, 32cmpt 5138 . 2 class (𝑤 ∈ V ↦ {𝑠 ∈ (𝒫 (Base‘𝑤) ∖ {∅}) ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎𝑠𝑏𝑠 ((𝑥( ·𝑠𝑤)𝑎)(+g𝑤)𝑏) ∈ 𝑠})
341, 33wceq 1528 1 wff LSubSp = (𝑤 ∈ V ↦ {𝑠 ∈ (𝒫 (Base‘𝑤) ∖ {∅}) ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎𝑠𝑏𝑠 ((𝑥( ·𝑠𝑤)𝑎)(+g𝑤)𝑏) ∈ 𝑠})
Colors of variables: wff setvar class
This definition is referenced by:  lssset  19636
  Copyright terms: Public domain W3C validator