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

Definition df-lss 16040
 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 Scalar
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-lss
StepHypRef Expression
1 clss 16039 . 2
2 vw . . 3
3 cvv 2962 . . 3
4 vx . . . . . . . . . . 11
54cv 1652 . . . . . . . . . 10
6 va . . . . . . . . . . 11
76cv 1652 . . . . . . . . . 10
82cv 1652 . . . . . . . . . . 11
9 cvsca 13564 . . . . . . . . . . 11
108, 9cfv 5483 . . . . . . . . . 10
115, 7, 10co 6110 . . . . . . . . 9
12 vb . . . . . . . . . 10
1312cv 1652 . . . . . . . . 9
14 cplusg 13560 . . . . . . . . . 10
158, 14cfv 5483 . . . . . . . . 9
1611, 13, 15co 6110 . . . . . . . 8
17 vs . . . . . . . . 9
1817cv 1652 . . . . . . . 8
1916, 18wcel 1727 . . . . . . 7
2019, 12, 18wral 2711 . . . . . 6
2120, 6, 18wral 2711 . . . . 5
22 csca 13563 . . . . . . 7 Scalar
238, 22cfv 5483 . . . . . 6 Scalar
24 cbs 13500 . . . . . 6
2523, 24cfv 5483 . . . . 5 Scalar
2621, 4, 25wral 2711 . . . 4 Scalar
278, 24cfv 5483 . . . . . 6
2827cpw 3823 . . . . 5
29 c0 3613 . . . . . 6
3029csn 3838 . . . . 5
3128, 30cdif 3303 . . . 4
3226, 17, 31crab 2715 . . 3 Scalar
332, 3, 32cmpt 4291 . 2 Scalar
341, 33wceq 1653 1 Scalar
 Colors of variables: wff set class This definition is referenced by:  lssset  16041
 Copyright terms: Public domain W3C validator