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 ) ) ) }