MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  isnlm Structured version   Unicode version

Theorem isnlm 20156
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.)
Hypotheses
Ref Expression
isnlm.v  |-  V  =  ( Base `  W
)
isnlm.n  |-  N  =  ( norm `  W
)
isnlm.s  |-  .x.  =  ( .s `  W )
isnlm.f  |-  F  =  (Scalar `  W )
isnlm.k  |-  K  =  ( Base `  F
)
isnlm.a  |-  A  =  ( norm `  F
)
Assertion
Ref Expression
isnlm  |-  ( W  e. NrmMod 
<->  ( ( W  e. NrmGrp  /\  W  e.  LMod  /\  F  e. NrmRing )  /\  A. x  e.  K  A. y  e.  V  ( N `  ( x  .x.  y ) )  =  ( ( A `  x )  x.  ( N `  y )
) ) )
Distinct variable groups:    x, y, A    x, N, y    x, V, y    x, K    x, W, y    x,  .x. , y
Allowed substitution hints:    F( x, y)    K( y)

Proof of Theorem isnlm
Dummy variables  w  f are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 anass 644 . 2  |-  ( ( ( W  e.  (NrmGrp 
i^i  LMod )  /\  F  e. NrmRing )  /\  A. x  e.  K  A. y  e.  V  ( N `  ( x  .x.  y
) )  =  ( ( A `  x
)  x.  ( N `
 y ) ) )  <->  ( W  e.  (NrmGrp  i^i  LMod )  /\  ( F  e. NrmRing  /\  A. x  e.  K  A. y  e.  V  ( N `  ( x  .x.  y ) )  =  ( ( A `  x )  x.  ( N `  y )
) ) ) )
2 df-3an 962 . . . 4  |-  ( ( W  e. NrmGrp  /\  W  e. 
LMod  /\  F  e. NrmRing )  <->  ( ( W  e. NrmGrp  /\  W  e.  LMod )  /\  F  e. NrmRing ) )
3 elin 3536 . . . . 5  |-  ( W  e.  (NrmGrp  i^i  LMod ) 
<->  ( W  e. NrmGrp  /\  W  e.  LMod ) )
43anbi1i 690 . . . 4  |-  ( ( W  e.  (NrmGrp  i^i  LMod )  /\  F  e. NrmRing ) 
<->  ( ( W  e. NrmGrp  /\  W  e.  LMod )  /\  F  e. NrmRing )
)
52, 4bitr4i 252 . . 3  |-  ( ( W  e. NrmGrp  /\  W  e. 
LMod  /\  F  e. NrmRing )  <->  ( W  e.  (NrmGrp  i^i  LMod )  /\  F  e. NrmRing ) )
65anbi1i 690 . 2  |-  ( ( ( W  e. NrmGrp  /\  W  e.  LMod  /\  F  e. NrmRing )  /\  A. x  e.  K  A. y  e.  V  ( N `  ( x  .x.  y ) )  =  ( ( A `  x )  x.  ( N `  y ) ) )  <-> 
( ( W  e.  (NrmGrp  i^i  LMod )  /\  F  e. NrmRing )  /\  A. x  e.  K  A. y  e.  V  ( N `  ( x  .x.  y ) )  =  ( ( A `  x )  x.  ( N `  y )
) ) )
7 fvex 5698 . . . . 5  |-  (Scalar `  w )  e.  _V
87a1i 11 . . . 4  |-  ( w  =  W  ->  (Scalar `  w )  e.  _V )
9 id 22 . . . . . . 7  |-  ( f  =  (Scalar `  w
)  ->  f  =  (Scalar `  w ) )
10 fveq2 5688 . . . . . . . 8  |-  ( w  =  W  ->  (Scalar `  w )  =  (Scalar `  W ) )
11 isnlm.f . . . . . . . 8  |-  F  =  (Scalar `  W )
1210, 11syl6eqr 2491 . . . . . . 7  |-  ( w  =  W  ->  (Scalar `  w )  =  F )
139, 12sylan9eqr 2495 . . . . . 6  |-  ( ( w  =  W  /\  f  =  (Scalar `  w
) )  ->  f  =  F )
1413eleq1d 2507 . . . . 5  |-  ( ( w  =  W  /\  f  =  (Scalar `  w
) )  ->  (
f  e. NrmRing  <->  F  e. NrmRing ) )
1513fveq2d 5692 . . . . . . 7  |-  ( ( w  =  W  /\  f  =  (Scalar `  w
) )  ->  ( Base `  f )  =  ( Base `  F
) )
16 isnlm.k . . . . . . 7  |-  K  =  ( Base `  F
)
1715, 16syl6eqr 2491 . . . . . 6  |-  ( ( w  =  W  /\  f  =  (Scalar `  w
) )  ->  ( Base `  f )  =  K )
18 simpl 454 . . . . . . . . 9  |-  ( ( w  =  W  /\  f  =  (Scalar `  w
) )  ->  w  =  W )
1918fveq2d 5692 . . . . . . . 8  |-  ( ( w  =  W  /\  f  =  (Scalar `  w
) )  ->  ( Base `  w )  =  ( Base `  W
) )
20 isnlm.v . . . . . . . 8  |-  V  =  ( Base `  W
)
2119, 20syl6eqr 2491 . . . . . . 7  |-  ( ( w  =  W  /\  f  =  (Scalar `  w
) )  ->  ( Base `  w )  =  V )
2218fveq2d 5692 . . . . . . . . . 10  |-  ( ( w  =  W  /\  f  =  (Scalar `  w
) )  ->  ( norm `  w )  =  ( norm `  W
) )
23 isnlm.n . . . . . . . . . 10  |-  N  =  ( norm `  W
)
2422, 23syl6eqr 2491 . . . . . . . . 9  |-  ( ( w  =  W  /\  f  =  (Scalar `  w
) )  ->  ( norm `  w )  =  N )
2518fveq2d 5692 . . . . . . . . . . 11  |-  ( ( w  =  W  /\  f  =  (Scalar `  w
) )  ->  ( .s `  w )  =  ( .s `  W
) )
26 isnlm.s . . . . . . . . . . 11  |-  .x.  =  ( .s `  W )
2725, 26syl6eqr 2491 . . . . . . . . . 10  |-  ( ( w  =  W  /\  f  =  (Scalar `  w
) )  ->  ( .s `  w )  = 
.x.  )
2827oveqd 6107 . . . . . . . . 9  |-  ( ( w  =  W  /\  f  =  (Scalar `  w
) )  ->  (
x ( .s `  w ) y )  =  ( x  .x.  y ) )
2924, 28fveq12d 5694 . . . . . . . 8  |-  ( ( w  =  W  /\  f  =  (Scalar `  w
) )  ->  (
( norm `  w ) `  ( x ( .s
`  w ) y ) )  =  ( N `  ( x 
.x.  y ) ) )
3013fveq2d 5692 . . . . . . . . . . 11  |-  ( ( w  =  W  /\  f  =  (Scalar `  w
) )  ->  ( norm `  f )  =  ( norm `  F
) )
31 isnlm.a . . . . . . . . . . 11  |-  A  =  ( norm `  F
)
3230, 31syl6eqr 2491 . . . . . . . . . 10  |-  ( ( w  =  W  /\  f  =  (Scalar `  w
) )  ->  ( norm `  f )  =  A )
3332fveq1d 5690 . . . . . . . . 9  |-  ( ( w  =  W  /\  f  =  (Scalar `  w
) )  ->  (
( norm `  f ) `  x )  =  ( A `  x ) )
3424fveq1d 5690 . . . . . . . . 9  |-  ( ( w  =  W  /\  f  =  (Scalar `  w
) )  ->  (
( norm `  w ) `  y )  =  ( N `  y ) )
3533, 34oveq12d 6108 . . . . . . . 8  |-  ( ( w  =  W  /\  f  =  (Scalar `  w
) )  ->  (
( ( norm `  f
) `  x )  x.  ( ( norm `  w
) `  y )
)  =  ( ( A `  x )  x.  ( N `  y ) ) )
3629, 35eqeq12d 2455 . . . . . . 7  |-  ( ( w  =  W  /\  f  =  (Scalar `  w
) )  ->  (
( ( norm `  w
) `  ( x
( .s `  w
) y ) )  =  ( ( (
norm `  f ) `  x )  x.  (
( norm `  w ) `  y ) )  <->  ( N `  ( x  .x.  y
) )  =  ( ( A `  x
)  x.  ( N `
 y ) ) ) )
3721, 36raleqbidv 2929 . . . . . 6  |-  ( ( w  =  W  /\  f  =  (Scalar `  w
) )  ->  ( A. y  e.  ( Base `  w ) ( ( norm `  w
) `  ( x
( .s `  w
) y ) )  =  ( ( (
norm `  f ) `  x )  x.  (
( norm `  w ) `  y ) )  <->  A. y  e.  V  ( N `  ( x  .x.  y
) )  =  ( ( A `  x
)  x.  ( N `
 y ) ) ) )
3817, 37raleqbidv 2929 . . . . 5  |-  ( ( w  =  W  /\  f  =  (Scalar `  w
) )  ->  ( A. x  e.  ( Base `  f ) A. y  e.  ( Base `  w ) ( (
norm `  w ) `  ( x ( .s
`  w ) y ) )  =  ( ( ( norm `  f
) `  x )  x.  ( ( norm `  w
) `  y )
)  <->  A. x  e.  K  A. y  e.  V  ( N `  ( x 
.x.  y ) )  =  ( ( A `
 x )  x.  ( N `  y
) ) ) )
3914, 38anbi12d 705 . . . 4  |-  ( ( w  =  W  /\  f  =  (Scalar `  w
) )  ->  (
( 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 )
) )  <->  ( F  e. NrmRing  /\  A. x  e.  K  A. y  e.  V  ( N `  ( x  .x.  y ) )  =  ( ( A `  x )  x.  ( N `  y ) ) ) ) )
408, 39sbcied 3220 . . 3  |-  ( w  =  W  ->  ( [. (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 )
) )  <->  ( F  e. NrmRing  /\  A. x  e.  K  A. y  e.  V  ( N `  ( x  .x.  y ) )  =  ( ( A `  x )  x.  ( N `  y ) ) ) ) )
41 df-nlm 20079 . . 3  |- 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 )
) ) }
4240, 41elrab2 3116 . 2  |-  ( W  e. NrmMod 
<->  ( W  e.  (NrmGrp 
i^i  LMod )  /\  ( F  e. NrmRing  /\  A. x  e.  K  A. y  e.  V  ( N `  ( x  .x.  y
) )  =  ( ( A `  x
)  x.  ( N `
 y ) ) ) ) )
431, 6, 423bitr4ri 278 1  |-  ( W  e. NrmMod 
<->  ( ( W  e. NrmGrp  /\  W  e.  LMod  /\  F  e. NrmRing )  /\  A. x  e.  K  A. y  e.  V  ( N `  ( x  .x.  y ) )  =  ( ( A `  x )  x.  ( N `  y )
) ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369    /\ w3a 960    = wceq 1364    e. wcel 1761   A.wral 2713   _Vcvv 2970   [.wsbc 3183    i^i cin 3324   ` cfv 5415  (class class class)co 6090    x. cmul 9283   Basecbs 14170  Scalarcsca 14237   .scvsca 14238   LModclmod 16928   normcnm 20069  NrmGrpcngp 20070  NrmRingcnrg 20072  NrmModcnlm 20073
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-nul 4418
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2263  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-rab 2722  df-v 2972  df-sbc 3184  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-sn 3875  df-pr 3877  df-op 3881  df-uni 4089  df-br 4290  df-iota 5378  df-fv 5423  df-ov 6093  df-nlm 20079
This theorem is referenced by:  nmvs  20157  nlmngp  20158  nlmlmod  20159  nlmnrg  20160  sranlm  20165  lssnlm  20181  tchcph  20652  cnzh  26319  rezh  26320
  Copyright terms: Public domain W3C validator