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

Definition df-lss 15690
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  =  ( w  e.  _V  |->  { s  e.  ( ~P ( Base `  w
)  \  { (/) } )  |  A. x  e.  ( Base `  (Scalar `  w ) ) A. a  e.  s  A. b  e.  s  (
( x ( .s
`  w ) a ) ( +g  `  w
) b )  e.  s } )
Distinct variable group:    a, b, s, x, w

Detailed syntax breakdown of Definition df-lss
StepHypRef Expression
1 clss 15689 . 2  class  LSubSp
2 vw . . 3  set  w
3 cvv 2788 . . 3  class  _V
4 vx . . . . . . . . . . 11  set  x
54cv 1622 . . . . . . . . . 10  class  x
6 va . . . . . . . . . . 11  set  a
76cv 1622 . . . . . . . . . 10  class  a
82cv 1622 . . . . . . . . . . 11  class  w
9 cvsca 13212 . . . . . . . . . . 11  class  .s
108, 9cfv 5255 . . . . . . . . . 10  class  ( .s
`  w )
115, 7, 10co 5858 . . . . . . . . 9  class  ( x ( .s `  w
) a )
12 vb . . . . . . . . . 10  set  b
1312cv 1622 . . . . . . . . 9  class  b
14 cplusg 13208 . . . . . . . . . 10  class  +g
158, 14cfv 5255 . . . . . . . . 9  class  ( +g  `  w )
1611, 13, 15co 5858 . . . . . . . 8  class  ( ( x ( .s `  w ) a ) ( +g  `  w
) b )
17 vs . . . . . . . . 9  set  s
1817cv 1622 . . . . . . . 8  class  s
1916, 18wcel 1684 . . . . . . 7  wff  ( ( x ( .s `  w ) a ) ( +g  `  w
) b )  e.  s
2019, 12, 18wral 2543 . . . . . 6  wff  A. b  e.  s  ( (
x ( .s `  w ) a ) ( +g  `  w
) b )  e.  s
2120, 6, 18wral 2543 . . . . 5  wff  A. a  e.  s  A. b  e.  s  ( (
x ( .s `  w ) a ) ( +g  `  w
) b )  e.  s
22 csca 13211 . . . . . . 7  class Scalar
238, 22cfv 5255 . . . . . 6  class  (Scalar `  w )
24 cbs 13148 . . . . . 6  class  Base
2523, 24cfv 5255 . . . . 5  class  ( Base `  (Scalar `  w )
)
2621, 4, 25wral 2543 . . . 4  wff  A. x  e.  ( Base `  (Scalar `  w ) ) A. a  e.  s  A. b  e.  s  (
( x ( .s
`  w ) a ) ( +g  `  w
) b )  e.  s
278, 24cfv 5255 . . . . . 6  class  ( Base `  w )
2827cpw 3625 . . . . 5  class  ~P ( Base `  w )
29 c0 3455 . . . . . 6  class  (/)
3029csn 3640 . . . . 5  class  { (/) }
3128, 30cdif 3149 . . . 4  class  ( ~P ( Base `  w
)  \  { (/) } )
3226, 17, 31crab 2547 . . 3  class  { s  e.  ( ~P ( Base `  w )  \  { (/) } )  | 
A. x  e.  (
Base `  (Scalar `  w
) ) A. a  e.  s  A. b  e.  s  ( (
x ( .s `  w ) a ) ( +g  `  w
) b )  e.  s }
332, 3, 32cmpt 4077 . 2  class  ( w  e.  _V  |->  { s  e.  ( ~P ( Base `  w )  \  { (/) } )  | 
A. x  e.  (
Base `  (Scalar `  w
) ) A. a  e.  s  A. b  e.  s  ( (
x ( .s `  w ) a ) ( +g  `  w
) b )  e.  s } )
341, 33wceq 1623 1  wff  LSubSp  =  ( w  e.  _V  |->  { s  e.  ( ~P ( Base `  w
)  \  { (/) } )  |  A. x  e.  ( Base `  (Scalar `  w ) ) A. a  e.  s  A. b  e.  s  (
( x ( .s
`  w ) a ) ( +g  `  w
) b )  e.  s } )
Colors of variables: wff set class
This definition is referenced by:  lssset  15691
  Copyright terms: Public domain W3C validator