Metamath Proof Explorer


Definition df-nlm

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)

Ref Expression
Assertion 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 ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cnlm
 |-  NrmMod
1 vw
 |-  w
2 cngp
 |-  NrmGrp
3 clmod
 |-  LMod
4 2 3 cin
 |-  ( NrmGrp i^i LMod )
5 csca
 |-  Scalar
6 1 cv
 |-  w
7 6 5 cfv
 |-  ( Scalar ` w )
8 vf
 |-  f
9 8 cv
 |-  f
10 cnrg
 |-  NrmRing
11 9 10 wcel
 |-  f e. NrmRing
12 vx
 |-  x
13 cbs
 |-  Base
14 9 13 cfv
 |-  ( Base ` f )
15 vy
 |-  y
16 6 13 cfv
 |-  ( Base ` w )
17 cnm
 |-  norm
18 6 17 cfv
 |-  ( norm ` w )
19 12 cv
 |-  x
20 cvsca
 |-  .s
21 6 20 cfv
 |-  ( .s ` w )
22 15 cv
 |-  y
23 19 22 21 co
 |-  ( x ( .s ` w ) y )
24 23 18 cfv
 |-  ( ( norm ` w ) ` ( x ( .s ` w ) y ) )
25 9 17 cfv
 |-  ( norm ` f )
26 19 25 cfv
 |-  ( ( norm ` f ) ` x )
27 cmul
 |-  x.
28 22 18 cfv
 |-  ( ( norm ` w ) ` y )
29 26 28 27 co
 |-  ( ( ( norm ` f ) ` x ) x. ( ( norm ` w ) ` y ) )
30 24 29 wceq
 |-  ( ( norm ` w ) ` ( x ( .s ` w ) y ) ) = ( ( ( norm ` f ) ` x ) x. ( ( norm ` w ) ` y ) )
31 30 15 16 wral
 |-  A. y e. ( Base ` w ) ( ( norm ` w ) ` ( x ( .s ` w ) y ) ) = ( ( ( norm ` f ) ` x ) x. ( ( norm ` w ) ` y ) )
32 31 12 14 wral
 |-  A. x e. ( Base ` f ) A. y e. ( Base ` w ) ( ( norm ` w ) ` ( x ( .s ` w ) y ) ) = ( ( ( norm ` f ) ` x ) x. ( ( norm ` w ) ` y ) )
33 11 32 wa
 |-  ( 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 ) ) )
34 33 8 7 wsbc
 |-  [. ( 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 ) ) )
35 34 1 4 crab
 |-  { 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 ) ) ) }
36 0 35 wceq
 |-  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 ) ) ) }