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

Definition df-nlm 21679
 Description: A normed (left) module is a module which is also a normed group over a normed ring, such that the norm distributes over scalar multiplication. (Contributed by Mario Carneiro, 4-Oct-2015.)
Assertion
Ref Expression
df-nlm NrmMod NrmGrp Scalar NrmRing
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-nlm
StepHypRef Expression
1 cnlm 21673 . 2 NrmMod
2 vf . . . . . . 7
32cv 1451 . . . . . 6
4 cnrg 21672 . . . . . 6 NrmRing
53, 4wcel 1904 . . . . 5 NrmRing
6 vx . . . . . . . . . . 11
76cv 1451 . . . . . . . . . 10
8 vy . . . . . . . . . . 11
98cv 1451 . . . . . . . . . 10
10 vw . . . . . . . . . . . 12
1110cv 1451 . . . . . . . . . . 11
12 cvsca 15272 . . . . . . . . . . 11
1311, 12cfv 5589 . . . . . . . . . 10
147, 9, 13co 6308 . . . . . . . . 9
15 cnm 21669 . . . . . . . . . 10
1611, 15cfv 5589 . . . . . . . . 9
1714, 16cfv 5589 . . . . . . . 8
183, 15cfv 5589 . . . . . . . . . 10
197, 18cfv 5589 . . . . . . . . 9
209, 16cfv 5589 . . . . . . . . 9
21 cmul 9562 . . . . . . . . 9
2219, 20, 21co 6308 . . . . . . . 8
2317, 22wceq 1452 . . . . . . 7
24 cbs 15199 . . . . . . . 8
2511, 24cfv 5589 . . . . . . 7
2623, 8, 25wral 2756 . . . . . 6
273, 24cfv 5589 . . . . . 6
2826, 6, 27wral 2756 . . . . 5
295, 28wa 376 . . . 4 NrmRing
30 csca 15271 . . . . 5 Scalar
3111, 30cfv 5589 . . . 4 Scalar
3229, 2, 31wsbc 3255 . . 3 Scalar NrmRing
33 cngp 21670 . . . 4 NrmGrp
34 clmod 18169 . . . 4
3533, 34cin 3389 . . 3 NrmGrp
3632, 10, 35crab 2760 . 2 NrmGrp Scalar NrmRing
371, 36wceq 1452 1 NrmMod NrmGrp Scalar NrmRing
 Colors of variables: wff setvar class This definition is referenced by:  isnlm  21756
 Copyright terms: Public domain W3C validator