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

Definition df-lss 18156
 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 18155 . 2
2 vw . . 3
3 cvv 3045 . . 3
4 vx . . . . . . . . . . 11
54cv 1443 . . . . . . . . . 10
6 va . . . . . . . . . . 11
76cv 1443 . . . . . . . . . 10
82cv 1443 . . . . . . . . . . 11
9 cvsca 15194 . . . . . . . . . . 11
108, 9cfv 5582 . . . . . . . . . 10
115, 7, 10co 6290 . . . . . . . . 9
12 vb . . . . . . . . . 10
1312cv 1443 . . . . . . . . 9
14 cplusg 15190 . . . . . . . . . 10
158, 14cfv 5582 . . . . . . . . 9
1611, 13, 15co 6290 . . . . . . . 8
17 vs . . . . . . . . 9
1817cv 1443 . . . . . . . 8
1916, 18wcel 1887 . . . . . . 7
2019, 12, 18wral 2737 . . . . . 6
2120, 6, 18wral 2737 . . . . 5
22 csca 15193 . . . . . . 7 Scalar
238, 22cfv 5582 . . . . . 6 Scalar
24 cbs 15121 . . . . . 6
2523, 24cfv 5582 . . . . 5 Scalar
2621, 4, 25wral 2737 . . . 4 Scalar
278, 24cfv 5582 . . . . . 6
2827cpw 3951 . . . . 5
29 c0 3731 . . . . . 6
3029csn 3968 . . . . 5
3128, 30cdif 3401 . . . 4
3226, 17, 31crab 2741 . . 3 Scalar
332, 3, 32cmpt 4461 . 2 Scalar
341, 33wceq 1444 1 Scalar
 Colors of variables: wff setvar class This definition is referenced by:  lssset  18157
 Copyright terms: Public domain W3C validator