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

Definition df-lss 15936
 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 15935 . 2
2 vw . . 3
3 cvv 2899 . . 3
4 vx . . . . . . . . . . 11
54cv 1648 . . . . . . . . . 10
6 va . . . . . . . . . . 11
76cv 1648 . . . . . . . . . 10
82cv 1648 . . . . . . . . . . 11
9 cvsca 13460 . . . . . . . . . . 11
108, 9cfv 5394 . . . . . . . . . 10
115, 7, 10co 6020 . . . . . . . . 9
12 vb . . . . . . . . . 10
1312cv 1648 . . . . . . . . 9
14 cplusg 13456 . . . . . . . . . 10
158, 14cfv 5394 . . . . . . . . 9
1611, 13, 15co 6020 . . . . . . . 8
17 vs . . . . . . . . 9
1817cv 1648 . . . . . . . 8
1916, 18wcel 1717 . . . . . . 7
2019, 12, 18wral 2649 . . . . . 6
2120, 6, 18wral 2649 . . . . 5
22 csca 13459 . . . . . . 7 Scalar
238, 22cfv 5394 . . . . . 6 Scalar
24 cbs 13396 . . . . . 6
2523, 24cfv 5394 . . . . 5 Scalar
2621, 4, 25wral 2649 . . . 4 Scalar
278, 24cfv 5394 . . . . . 6
2827cpw 3742 . . . . 5
29 c0 3571 . . . . . 6
3029csn 3757 . . . . 5
3128, 30cdif 3260 . . . 4
3226, 17, 31crab 2653 . . 3 Scalar
332, 3, 32cmpt 4207 . 2 Scalar
341, 33wceq 1649 1 Scalar
 Colors of variables: wff set class This definition is referenced by:  lssset  15937
 Copyright terms: Public domain W3C validator