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

Definition df-nlm 18626
 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 18620 . 2 NrmMod
2 vf . . . . . . 7
32cv 1651 . . . . . 6
4 cnrg 18619 . . . . . 6 NrmRing
53, 4wcel 1725 . . . . 5 NrmRing
6 vx . . . . . . . . . . 11
76cv 1651 . . . . . . . . . 10
8 vy . . . . . . . . . . 11
98cv 1651 . . . . . . . . . 10
10 vw . . . . . . . . . . . 12
1110cv 1651 . . . . . . . . . . 11
12 cvsca 13525 . . . . . . . . . . 11
1311, 12cfv 5446 . . . . . . . . . 10
147, 9, 13co 6073 . . . . . . . . 9
15 cnm 18616 . . . . . . . . . 10
1611, 15cfv 5446 . . . . . . . . 9
1714, 16cfv 5446 . . . . . . . 8
183, 15cfv 5446 . . . . . . . . . 10
197, 18cfv 5446 . . . . . . . . 9
209, 16cfv 5446 . . . . . . . . 9
21 cmul 8987 . . . . . . . . 9
2219, 20, 21co 6073 . . . . . . . 8
2317, 22wceq 1652 . . . . . . 7
24 cbs 13461 . . . . . . . 8
2511, 24cfv 5446 . . . . . . 7
2623, 8, 25wral 2697 . . . . . 6
273, 24cfv 5446 . . . . . 6
2826, 6, 27wral 2697 . . . . 5
295, 28wa 359 . . . 4 NrmRing
30 csca 13524 . . . . 5 Scalar
3111, 30cfv 5446 . . . 4 Scalar
3229, 2, 31wsbc 3153 . . 3 Scalar NrmRing
33 cngp 18617 . . . 4 NrmGrp
34 clmod 15942 . . . 4
3533, 34cin 3311 . . 3 NrmGrp
3632, 10, 35crab 2701 . 2 NrmGrp Scalar NrmRing
371, 36wceq 1652 1 NrmMod NrmGrp Scalar NrmRing
 Colors of variables: wff set class This definition is referenced by:  isnlm  18703
 Copyright terms: Public domain W3C validator