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

Definition df-nlm 19879
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 19873 . 2
2 vf . . . . . . 7
32cv 1686 . . . . . 6
4 cnrg 19872 . . . . . 6
53, 4wcel 1749 . . . . 5
6 vx . . . . . . . . . . 11
76cv 1686 . . . . . . . . . 10
8 vy . . . . . . . . . . 11
98cv 1686 . . . . . . . . . 10
10 vw . . . . . . . . . . . 12
1110cv 1686 . . . . . . . . . . 11
12 cvsca 14182 . . . . . . . . . . 11
1311, 12cfv 5390 . . . . . . . . . 10
147, 9, 13co 6061 . . . . . . . . 9
15 cnm 19869 . . . . . . . . . 10
1611, 15cfv 5390 . . . . . . . . 9
1714, 16cfv 5390 . . . . . . . 8
183, 15cfv 5390 . . . . . . . . . 10
197, 18cfv 5390 . . . . . . . . 9
209, 16cfv 5390 . . . . . . . . 9
21 cmul 9233 . . . . . . . . 9
2219, 20, 21co 6061 . . . . . . . 8
2317, 22wceq 1687 . . . . . . 7
24 cbs 14114 . . . . . . . 8
2511, 24cfv 5390 . . . . . . 7
2623, 8, 25wral 2694 . . . . . 6
273, 24cfv 5390 . . . . . 6
2826, 6, 27wral 2694 . . . . 5
295, 28wa 362 . . . 4
30 csca 14181 . . . . 5
3111, 30cfv 5390 . . . 4
3229, 2, 31wsbc 3164 . . 3
33 cngp 19870 . . . 4
34 clmod 16761 . . . 4
3533, 34cin 3304 . . 3
3632, 10, 35crab 2698 . 2
371, 36wceq 1687 1
Colors of variables: wff setvar class
This definition is referenced by:  isnlm  19956
  Copyright terms: Public domain W3C validator