Metamath Proof Explorer

Definition df-abv

Description: Define the set of absolute values on a ring. An absolute value is a generalization of the usual absolute value function df-abs to arbitrary rings. (Contributed by Mario Carneiro, 8-Sep-2014)

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 cabv 
 |-  AbsVal
1 vr 
 |-  r
2 crg 
 |-  Ring
3 vf 
 |-  f
4 cc0 
 |-  0
5 cico 
 |-  [,)
6 cpnf 
 |-  +oo
7 4 6 5 co 
 |-  ( 0 [,) +oo )
8 cmap 
 |-  ^m
9 cbs 
 |-  Base
10 1 cv 
 |-  r
11 10 9 cfv 
 |-  ( Base ` r )
12 7 11 8 co 
 |-  ( ( 0 [,) +oo ) ^m ( Base ` r ) )
13 vx 
 |-  x
14 3 cv 
 |-  f
15 13 cv 
 |-  x
16 15 14 cfv 
 |-  ( f ` x )
17 16 4 wceq 
 |-  ( f ` x ) = 0
18 c0g 
 |-  0g
19 10 18 cfv 
 |-  ( 0g ` r )
20 15 19 wceq 
 |-  x = ( 0g ` r )
21 17 20 wb 
 |-  ( ( f ` x ) = 0 <-> x = ( 0g ` r ) )
22 vy 
 |-  y
23 cmulr 
 |-  .r
24 10 23 cfv 
 |-  ( .r ` r )
25 22 cv 
 |-  y
26 15 25 24 co 
 |-  ( x ( .r ` r ) y )
27 26 14 cfv 
 |-  ( f ` ( x ( .r ` r ) y ) )
28 cmul 
 |-  x.
29 25 14 cfv 
 |-  ( f ` y )
30 16 29 28 co 
 |-  ( ( f ` x ) x. ( f ` y ) )
31 27 30 wceq 
 |-  ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) x. ( f ` y ) )
32 cplusg 
 |-  +g
33 10 32 cfv 
 |-  ( +g ` r )
34 15 25 33 co 
 |-  ( x ( +g ` r ) y )
35 34 14 cfv 
 |-  ( f ` ( x ( +g ` r ) y ) )
36 cle 
 |-  <_
37 caddc 
 |-  +
38 16 29 37 co 
 |-  ( ( f ` x ) + ( f ` y ) )
39 35 38 36 wbr 
 |-  ( f ` ( x ( +g ` r ) y ) ) <_ ( ( f ` x ) + ( f ` y ) )
40 31 39 wa 
 |-  ( ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) x. ( f ` y ) ) /\ ( f ` ( x ( +g ` r ) y ) ) <_ ( ( f ` x ) + ( f ` y ) ) )
41 40 22 11 wral 
 |-  A. y e. ( Base ` r ) ( ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) x. ( f ` y ) ) /\ ( f ` ( x ( +g ` r ) y ) ) <_ ( ( f ` x ) + ( f ` y ) ) )
42 21 41 wa 
 |-  ( ( ( 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 ) ) ) )
43 42 13 11 wral 
 |-  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 ) ) ) )
44 43 3 12 crab 
 |-  { 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 ) ) ) ) }
45 1 2 44 cmpt 
 |-  ( 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 ) ) ) ) } )
46 0 45 wceq 
 |-  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 ) ) ) ) } )