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

Definition df-nlm 18109
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  =  {
w  e.  (NrmGrp  i^i  LMod )  |  [. (Scalar `  w )  /  f ]. ( f  e. NrmRing  /\  A. x  e.  ( Base `  f ) A. y  e.  ( Base `  w
) ( ( norm `  w ) `  (
x ( .s `  w ) y ) )  =  ( ( ( norm `  f
) `  x )  x.  ( ( norm `  w
) `  y )
) ) }
Distinct variable group:    w, f, x, y

Detailed syntax breakdown of Definition df-nlm
StepHypRef Expression
1 cnlm 18103 . 2  class NrmMod
2 vf . . . . . . 7  set  f
32cv 1622 . . . . . 6  class  f
4 cnrg 18102 . . . . . 6  class NrmRing
53, 4wcel 1684 . . . . 5  wff  f  e. NrmRing
6 vx . . . . . . . . . . 11  set  x
76cv 1622 . . . . . . . . . 10  class  x
8 vy . . . . . . . . . . 11  set  y
98cv 1622 . . . . . . . . . 10  class  y
10 vw . . . . . . . . . . . 12  set  w
1110cv 1622 . . . . . . . . . . 11  class  w
12 cvsca 13212 . . . . . . . . . . 11  class  .s
1311, 12cfv 5255 . . . . . . . . . 10  class  ( .s
`  w )
147, 9, 13co 5858 . . . . . . . . 9  class  ( x ( .s `  w
) y )
15 cnm 18099 . . . . . . . . . 10  class  norm
1611, 15cfv 5255 . . . . . . . . 9  class  ( norm `  w )
1714, 16cfv 5255 . . . . . . . 8  class  ( (
norm `  w ) `  ( x ( .s
`  w ) y ) )
183, 15cfv 5255 . . . . . . . . . 10  class  ( norm `  f )
197, 18cfv 5255 . . . . . . . . 9  class  ( (
norm `  f ) `  x )
209, 16cfv 5255 . . . . . . . . 9  class  ( (
norm `  w ) `  y )
21 cmul 8742 . . . . . . . . 9  class  x.
2219, 20, 21co 5858 . . . . . . . 8  class  ( ( ( norm `  f
) `  x )  x.  ( ( norm `  w
) `  y )
)
2317, 22wceq 1623 . . . . . . 7  wff  ( (
norm `  w ) `  ( x ( .s
`  w ) y ) )  =  ( ( ( norm `  f
) `  x )  x.  ( ( norm `  w
) `  y )
)
24 cbs 13148 . . . . . . . 8  class  Base
2511, 24cfv 5255 . . . . . . 7  class  ( Base `  w )
2623, 8, 25wral 2543 . . . . . 6  wff  A. y  e.  ( Base `  w
) ( ( norm `  w ) `  (
x ( .s `  w ) y ) )  =  ( ( ( norm `  f
) `  x )  x.  ( ( norm `  w
) `  y )
)
273, 24cfv 5255 . . . . . 6  class  ( Base `  f )
2826, 6, 27wral 2543 . . . . 5  wff  A. x  e.  ( Base `  f
) A. y  e.  ( Base `  w
) ( ( norm `  w ) `  (
x ( .s `  w ) y ) )  =  ( ( ( norm `  f
) `  x )  x.  ( ( norm `  w
) `  y )
)
295, 28wa 358 . . . 4  wff  ( f  e. NrmRing  /\  A. x  e.  ( Base `  f
) A. y  e.  ( Base `  w
) ( ( norm `  w ) `  (
x ( .s `  w ) y ) )  =  ( ( ( norm `  f
) `  x )  x.  ( ( norm `  w
) `  y )
) )
30 csca 13211 . . . . 5  class Scalar
3111, 30cfv 5255 . . . 4  class  (Scalar `  w )
3229, 2, 31wsbc 2991 . . 3  wff  [. (Scalar `  w )  /  f ]. ( f  e. NrmRing  /\  A. x  e.  ( Base `  f ) A. y  e.  ( Base `  w
) ( ( norm `  w ) `  (
x ( .s `  w ) y ) )  =  ( ( ( norm `  f
) `  x )  x.  ( ( norm `  w
) `  y )
) )
33 cngp 18100 . . . 4  class NrmGrp
34 clmod 15627 . . . 4  class  LMod
3533, 34cin 3151 . . 3  class  (NrmGrp  i^i  LMod )
3632, 10, 35crab 2547 . 2  class  { w  e.  (NrmGrp  i^i  LMod )  | 
[. (Scalar `  w )  /  f ]. (
f  e. NrmRing  /\  A. x  e.  ( Base `  f
) A. y  e.  ( Base `  w
) ( ( norm `  w ) `  (
x ( .s `  w ) y ) )  =  ( ( ( norm `  f
) `  x )  x.  ( ( norm `  w
) `  y )
) ) }
371, 36wceq 1623 1  wff NrmMod  =  {
w  e.  (NrmGrp  i^i  LMod )  |  [. (Scalar `  w )  /  f ]. ( f  e. NrmRing  /\  A. x  e.  ( Base `  f ) A. y  e.  ( Base `  w
) ( ( norm `  w ) `  (
x ( .s `  w ) y ) )  =  ( ( ( norm `  f
) `  x )  x.  ( ( norm `  w
) `  y )
) ) }
Colors of variables: wff set class
This definition is referenced by:  isnlm  18186
  Copyright terms: Public domain W3C validator