Definition df-abv 18817

Description: Define the set of absolute values on a ring. An absolute value is a generalization of the usual absolute value function df-abs 13976 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

Step	Hyp	Ref	Expression
1		cabv 18816	. 2 class AbsVal
2		vr	. . 3 setvar r
3		crg 18547	. . 3 class Ring
4		vx	. . . . . . . . . 10 setvar x
5	4	cv 1482	. . . . . . . . 9 class x
6		vf	. . . . . . . . . 10 setvar f
7	6	cv 1482	. . . . . . . . 9 class f
8	5, 7	cfv 5888	. . . . . . . 8 class ( f ` x )
9		cc0 9936	. . . . . . . 8 class 0
10	8, 9	wceq 1483	. . . . . . 7 wff ( f ` x ) = 0
11	2	cv 1482	. . . . . . . . 9 class r
12		c0g 16100	. . . . . . . . 9 class 0g
13	11, 12	cfv 5888	. . . . . . . 8 class ( 0g ` r )
14	5, 13	wceq 1483	. . . . . . 7 wff x = ( 0g ` r )
15	10, 14	wb 196	. . . . . 6 wff ( ( f ` x ) = 0 <-> x = ( 0g ` r ) )
16		vy	. . . . . . . . . . . 12 setvar y
17	16	cv 1482	. . . . . . . . . . 11 class y
18		cmulr 15942	. . . . . . . . . . . 12 class .r
19	11, 18	cfv 5888	. . . . . . . . . . 11 class ( .r ` r )
20	5, 17, 19	co 6650	. . . . . . . . . 10 class ( x ( .r ` r ) y )
21	20, 7	cfv 5888	. . . . . . . . 9 class ( f ` ( x ( .r ` r ) y ) )
22	17, 7	cfv 5888	. . . . . . . . . 10 class ( f ` y )
23		cmul 9941	. . . . . . . . . 10 class x.
24	8, 22, 23	co 6650	. . . . . . . . 9 class ( ( f ` x ) x. ( f ` y ) )
25	21, 24	wceq 1483	. . . . . . . 8 wff ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) x. ( f ` y ) )
26		cplusg 15941	. . . . . . . . . . . 12 class +g
27	11, 26	cfv 5888	. . . . . . . . . . 11 class ( +g ` r )
28	5, 17, 27	co 6650	. . . . . . . . . 10 class ( x ( +g ` r ) y )
29	28, 7	cfv 5888	. . . . . . . . 9 class ( f ` ( x ( +g ` r ) y ) )
30		caddc 9939	. . . . . . . . . 10 class +
31	8, 22, 30	co 6650	. . . . . . . . 9 class ( ( f ` x ) + ( f ` y ) )
32		cle 10075	. . . . . . . . 9 class <_
33	29, 31, 32	wbr 4653	. . . . . . . 8 wff ( f ` ( x ( +g ` r ) y ) ) <_ ( ( f ` x ) + ( f ` y ) )
34	25, 33	wa 384	. . . . . . 7 wff ( ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) x. ( f ` y ) ) /\ ( f ` ( x ( +g ` r ) y ) ) <_ ( ( f ` x ) + ( f ` y ) ) )
35		cbs 15857	. . . . . . . 8 class Base
36	11, 35	cfv 5888	. . . . . . 7 class ( Base ` r )
37	34, 16, 36	wral 2912	. . . . . 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 ) ) )
38	15, 37	wa 384	. . . . 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 ) ) ) )
39	38, 4, 36	wral 2912	. . . 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 10071	. . . . . 6 class +oo
41		cico 12177	. . . . . 6 class [,)
42	9, 40, 41	co 6650	. . . . 5 class ( 0 [,) +oo )
43		cmap 7857	. . . . 5 class ^m
44	42, 36, 43	co 6650	. . . 4 class ( ( 0 [,) +oo ) ^m ( Base ` r ) )
45	39, 6, 44	crab 2916	. . 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 ) ) ) ) }
46	2, 3, 45	cmpt 4729	. 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 ) ) ) ) } )
47	1, 46	wceq 1483	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 ) ) ) ) } )

This definition is referenced by:  abvfval  18818  abvrcl  18821