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

Definition df-abv 15578
Description: Define the set of absolute values on a ring. An absolute value is a generalization of the usual absolute value function df-abs 11717 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 15577 . 2  class AbsVal
2 vr . . 3  set  r
3 crg 15333 . . 3  class  Ring
4 vx . . . . . . . . . 10  set  x
54cv 1624 . . . . . . . . 9  class  x
6 vf . . . . . . . . . 10  set  f
76cv 1624 . . . . . . . . 9  class  f
85, 7cfv 5223 . . . . . . . 8  class  ( f `
 x )
9 cc0 8734 . . . . . . . 8  class  0
108, 9wceq 1625 . . . . . . 7  wff  ( f `
 x )  =  0
112cv 1624 . . . . . . . . 9  class  r
12 c0g 13396 . . . . . . . . 9  class  0g
1311, 12cfv 5223 . . . . . . . 8  class  ( 0g
`  r )
145, 13wceq 1625 . . . . . . 7  wff  x  =  ( 0g `  r
)
1510, 14wb 178 . . . . . 6  wff  ( ( f `  x )  =  0  <->  x  =  ( 0g `  r ) )
16 vy . . . . . . . . . . . 12  set  y
1716cv 1624 . . . . . . . . . . 11  class  y
18 cmulr 13205 . . . . . . . . . . . 12  class  .r
1911, 18cfv 5223 . . . . . . . . . . 11  class  ( .r
`  r )
205, 17, 19co 5821 . . . . . . . . . 10  class  ( x ( .r `  r
) y )
2120, 7cfv 5223 . . . . . . . . 9  class  ( f `
 ( x ( .r `  r ) y ) )
2217, 7cfv 5223 . . . . . . . . . 10  class  ( f `
 y )
23 cmul 8739 . . . . . . . . . 10  class  x.
248, 22, 23co 5821 . . . . . . . . 9  class  ( ( f `  x )  x.  ( f `  y ) )
2521, 24wceq 1625 . . . . . . . 8  wff  ( f `
 ( x ( .r `  r ) y ) )  =  ( ( f `  x )  x.  (
f `  y )
)
26 cplusg 13204 . . . . . . . . . . . 12  class  +g
2711, 26cfv 5223 . . . . . . . . . . 11  class  ( +g  `  r )
285, 17, 27co 5821 . . . . . . . . . 10  class  ( x ( +g  `  r
) y )
2928, 7cfv 5223 . . . . . . . . 9  class  ( f `
 ( x ( +g  `  r ) y ) )
30 caddc 8737 . . . . . . . . . 10  class  +
318, 22, 30co 5821 . . . . . . . . 9  class  ( ( f `  x )  +  ( f `  y ) )
32 cle 8865 . . . . . . . . 9  class  <_
3329, 31, 32wbr 4026 . . . . . . . 8  wff  ( f `
 ( x ( +g  `  r ) y ) )  <_ 
( ( f `  x )  +  ( f `  y ) )
3425, 33wa 360 . . . . . . 7  wff  ( ( f `  ( x ( .r `  r
) y ) )  =  ( ( f `
 x )  x.  ( f `  y
) )  /\  (
f `  ( x
( +g  `  r ) y ) )  <_ 
( ( f `  x )  +  ( f `  y ) ) )
35 cbs 13144 . . . . . . . 8  class  Base
3611, 35cfv 5223 . . . . . . 7  class  ( Base `  r )
3734, 16, 36wral 2546 . . . . . 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 360 . . . . 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 2546 . . . 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 8861 . . . . . 6  class  +oo
41 cico 10654 . . . . . 6  class  [,)
429, 40, 41co 5821 . . . . 5  class  ( 0 [,)  +oo )
43 cmap 6769 . . . . 5  class  ^m
4442, 36, 43co 5821 . . . 4  class  ( ( 0 [,)  +oo )  ^m  ( Base `  r
) )
4539, 6, 44crab 2550 . . 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 4080 . 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 1625 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 set class
This definition is referenced by:  abvfval  15579  abvrcl  15582
  Copyright terms: Public domain W3C validator