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

Definition df-abv 17592
Description: Define the set of absolute values on a ring. An absolute value is a generalization of the usual absolute value function df-abs 13080 to arbitrary rings. (Contributed by Mario Carneiro, 8-Sep-2014.)
Assertion
Ref Expression
df-abv  |- AbsVal  =  ( r  e.  Ring  |->  { f  e.  ( ( 0 [,) +oo )  ^m  ( Base `  r )
)  |  A. x  e.  ( Base `  r
) ( ( ( f `  x )  =  0  <->  x  =  ( 0g `  r ) )  /\  A. y  e.  ( Base `  r
) ( ( f `
 ( x ( .r `  r ) y ) )  =  ( ( f `  x )  x.  (
f `  y )
)  /\  ( f `  ( x ( +g  `  r ) y ) )  <_  ( (
f `  x )  +  ( f `  y ) ) ) ) } )
Distinct variable group:    f, r, x, y

Detailed syntax breakdown of Definition df-abv
StepHypRef Expression
1 cabv 17591 . 2  class AbsVal
2 vr . . 3  setvar  r
3 crg 17324 . . 3  class  Ring
4 vx . . . . . . . . . 10  setvar  x
54cv 1394 . . . . . . . . 9  class  x
6 vf . . . . . . . . . 10  setvar  f
76cv 1394 . . . . . . . . 9  class  f
85, 7cfv 5594 . . . . . . . 8  class  ( f `
 x )
9 cc0 9509 . . . . . . . 8  class  0
108, 9wceq 1395 . . . . . . 7  wff  ( f `
 x )  =  0
112cv 1394 . . . . . . . . 9  class  r
12 c0g 14856 . . . . . . . . 9  class  0g
1311, 12cfv 5594 . . . . . . . 8  class  ( 0g
`  r )
145, 13wceq 1395 . . . . . . 7  wff  x  =  ( 0g `  r
)
1510, 14wb 184 . . . . . 6  wff  ( ( f `  x )  =  0  <->  x  =  ( 0g `  r ) )
16 vy . . . . . . . . . . . 12  setvar  y
1716cv 1394 . . . . . . . . . . 11  class  y
18 cmulr 14712 . . . . . . . . . . . 12  class  .r
1911, 18cfv 5594 . . . . . . . . . . 11  class  ( .r
`  r )
205, 17, 19co 6296 . . . . . . . . . 10  class  ( x ( .r `  r
) y )
2120, 7cfv 5594 . . . . . . . . 9  class  ( f `
 ( x ( .r `  r ) y ) )
2217, 7cfv 5594 . . . . . . . . . 10  class  ( f `
 y )
23 cmul 9514 . . . . . . . . . 10  class  x.
248, 22, 23co 6296 . . . . . . . . 9  class  ( ( f `  x )  x.  ( f `  y ) )
2521, 24wceq 1395 . . . . . . . 8  wff  ( f `
 ( x ( .r `  r ) y ) )  =  ( ( f `  x )  x.  (
f `  y )
)
26 cplusg 14711 . . . . . . . . . . . 12  class  +g
2711, 26cfv 5594 . . . . . . . . . . 11  class  ( +g  `  r )
285, 17, 27co 6296 . . . . . . . . . 10  class  ( x ( +g  `  r
) y )
2928, 7cfv 5594 . . . . . . . . 9  class  ( f `
 ( x ( +g  `  r ) y ) )
30 caddc 9512 . . . . . . . . . 10  class  +
318, 22, 30co 6296 . . . . . . . . 9  class  ( ( f `  x )  +  ( f `  y ) )
32 cle 9646 . . . . . . . . 9  class  <_
3329, 31, 32wbr 4456 . . . . . . . 8  wff  ( f `
 ( x ( +g  `  r ) y ) )  <_ 
( ( f `  x )  +  ( f `  y ) )
3425, 33wa 369 . . . . . . 7  wff  ( ( f `  ( x ( .r `  r
) y ) )  =  ( ( f `
 x )  x.  ( f `  y
) )  /\  (
f `  ( x
( +g  `  r ) y ) )  <_ 
( ( f `  x )  +  ( f `  y ) ) )
35 cbs 14643 . . . . . . . 8  class  Base
3611, 35cfv 5594 . . . . . . 7  class  ( Base `  r )
3734, 16, 36wral 2807 . . . . . 6  wff  A. y  e.  ( Base `  r
) ( ( f `
 ( x ( .r `  r ) y ) )  =  ( ( f `  x )  x.  (
f `  y )
)  /\  ( f `  ( x ( +g  `  r ) y ) )  <_  ( (
f `  x )  +  ( f `  y ) ) )
3815, 37wa 369 . . . . 5  wff  ( ( ( f `  x
)  =  0  <->  x  =  ( 0g `  r ) )  /\  A. y  e.  ( Base `  r ) ( ( f `  ( x ( .r `  r
) y ) )  =  ( ( f `
 x )  x.  ( f `  y
) )  /\  (
f `  ( x
( +g  `  r ) y ) )  <_ 
( ( f `  x )  +  ( f `  y ) ) ) )
3938, 4, 36wral 2807 . . . 4  wff  A. x  e.  ( Base `  r
) ( ( ( f `  x )  =  0  <->  x  =  ( 0g `  r ) )  /\  A. y  e.  ( Base `  r
) ( ( f `
 ( x ( .r `  r ) y ) )  =  ( ( f `  x )  x.  (
f `  y )
)  /\  ( f `  ( x ( +g  `  r ) y ) )  <_  ( (
f `  x )  +  ( f `  y ) ) ) )
40 cpnf 9642 . . . . . 6  class +oo
41 cico 11556 . . . . . 6  class  [,)
429, 40, 41co 6296 . . . . 5  class  ( 0 [,) +oo )
43 cmap 7438 . . . . 5  class  ^m
4442, 36, 43co 6296 . . . 4  class  ( ( 0 [,) +oo )  ^m  ( Base `  r
) )
4539, 6, 44crab 2811 . . 3  class  { f  e.  ( ( 0 [,) +oo )  ^m  ( Base `  r )
)  |  A. x  e.  ( Base `  r
) ( ( ( f `  x )  =  0  <->  x  =  ( 0g `  r ) )  /\  A. y  e.  ( Base `  r
) ( ( f `
 ( x ( .r `  r ) y ) )  =  ( ( f `  x )  x.  (
f `  y )
)  /\  ( f `  ( x ( +g  `  r ) y ) )  <_  ( (
f `  x )  +  ( f `  y ) ) ) ) }
462, 3, 45cmpt 4515 . 2  class  ( r  e.  Ring  |->  { f  e.  ( ( 0 [,) +oo )  ^m  ( Base `  r )
)  |  A. x  e.  ( Base `  r
) ( ( ( f `  x )  =  0  <->  x  =  ( 0g `  r ) )  /\  A. y  e.  ( Base `  r
) ( ( f `
 ( x ( .r `  r ) y ) )  =  ( ( f `  x )  x.  (
f `  y )
)  /\  ( f `  ( x ( +g  `  r ) y ) )  <_  ( (
f `  x )  +  ( f `  y ) ) ) ) } )
471, 46wceq 1395 1  wff AbsVal  =  ( r  e.  Ring  |->  { f  e.  ( ( 0 [,) +oo )  ^m  ( Base `  r )
)  |  A. x  e.  ( Base `  r
) ( ( ( f `  x )  =  0  <->  x  =  ( 0g `  r ) )  /\  A. y  e.  ( Base `  r
) ( ( f `
 ( x ( .r `  r ) y ) )  =  ( ( f `  x )  x.  (
f `  y )
)  /\  ( f `  ( x ( +g  `  r ) y ) )  <_  ( (
f `  x )  +  ( f `  y ) ) ) ) } )
Colors of variables: wff setvar class
This definition is referenced by:  abvfval  17593  abvrcl  17596
  Copyright terms: Public domain W3C validator