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

Definition df-nlm 20578
 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
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-nlm
StepHypRef Expression
1 cnlm 20572 . 2
2 vf . . . . . . 7
32cv 1369 . . . . . 6
4 cnrg 20571 . . . . . 6
53, 4wcel 1758 . . . . 5
6 vx . . . . . . . . . . 11
76cv 1369 . . . . . . . . . 10
8 vy . . . . . . . . . . 11
98cv 1369 . . . . . . . . . 10
10 vw . . . . . . . . . . . 12
1110cv 1369 . . . . . . . . . . 11
12 cvsca 14401 . . . . . . . . . . 11
1311, 12cfv 5537 . . . . . . . . . 10
147, 9, 13co 6222 . . . . . . . . 9
15 cnm 20568 . . . . . . . . . 10
1611, 15cfv 5537 . . . . . . . . 9
1714, 16cfv 5537 . . . . . . . 8
183, 15cfv 5537 . . . . . . . . . 10
197, 18cfv 5537 . . . . . . . . 9
209, 16cfv 5537 . . . . . . . . 9
21 cmul 9424 . . . . . . . . 9
2219, 20, 21co 6222 . . . . . . . 8
2317, 22wceq 1370 . . . . . . 7
24 cbs 14332 . . . . . . . 8
2511, 24cfv 5537 . . . . . . 7
2623, 8, 25wral 2800 . . . . . 6
273, 24cfv 5537 . . . . . 6
2826, 6, 27wral 2800 . . . . 5
295, 28wa 369 . . . 4
30 csca 14400 . . . . 5
3111, 30cfv 5537 . . . 4
3229, 2, 31wsbc 3297 . . 3
33 cngp 20569 . . . 4
34 clmod 17124 . . . 4
3533, 34cin 3441 . . 3
3632, 10, 35crab 2804 . 2
371, 36wceq 1370 1
 Colors of variables: wff setvar class This definition is referenced by:  isnlm  20655
 Copyright terms: Public domain W3C validator