Definition df-abv 19992

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

Assertion

Ref	Expression
df-abv	⊢ AbsVal = (𝑟 ∈ Ring ↦ {𝑓 ∈ ((0[,)+∞) ↑m (Base‘𝑟)) ∣ ∀𝑥 ∈ (Base‘𝑟)(((𝑓‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑟)) ∧ ∀𝑦 ∈ (Base‘𝑟)((𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥) · (𝑓‘𝑦)) ∧ (𝑓‘(𝑥(+g‘𝑟)𝑦)) ≤ ((𝑓‘𝑥) + (𝑓‘𝑦))))})

Distinct variable group:   𝑓,𝑟,𝑥,𝑦

Detailed syntax breakdown of Definition df-abv

Step	Hyp	Ref	Expression
1		cabv 19991	. 2 class AbsVal
2		vr	. . 3 setvar 𝑟
3		crg 19698	. . 3 class Ring
4		vx	. . . . . . . . . 10 setvar 𝑥
5	4	cv 1538	. . . . . . . . 9 class 𝑥
6		vf	. . . . . . . . . 10 setvar 𝑓
7	6	cv 1538	. . . . . . . . 9 class 𝑓
8	5, 7	cfv 6418	. . . . . . . 8 class (𝑓‘𝑥)
9		cc0 10802	. . . . . . . 8 class 0
10	8, 9	wceq 1539	. . . . . . 7 wff (𝑓‘𝑥) = 0
11	2	cv 1538	. . . . . . . . 9 class 𝑟
12		c0g 17067	. . . . . . . . 9 class 0g
13	11, 12	cfv 6418	. . . . . . . 8 class (0g‘𝑟)
14	5, 13	wceq 1539	. . . . . . 7 wff 𝑥 = (0g‘𝑟)
15	10, 14	wb 205	. . . . . 6 wff ((𝑓‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑟))
16		vy	. . . . . . . . . . . 12 setvar 𝑦
17	16	cv 1538	. . . . . . . . . . 11 class 𝑦
18		cmulr 16889	. . . . . . . . . . . 12 class .r
19	11, 18	cfv 6418	. . . . . . . . . . 11 class (.r‘𝑟)
20	5, 17, 19	co 7255	. . . . . . . . . 10 class (𝑥(.r‘𝑟)𝑦)
21	20, 7	cfv 6418	. . . . . . . . 9 class (𝑓‘(𝑥(.r‘𝑟)𝑦))
22	17, 7	cfv 6418	. . . . . . . . . 10 class (𝑓‘𝑦)
23		cmul 10807	. . . . . . . . . 10 class ·
24	8, 22, 23	co 7255	. . . . . . . . 9 class ((𝑓‘𝑥) · (𝑓‘𝑦))
25	21, 24	wceq 1539	. . . . . . . 8 wff (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥) · (𝑓‘𝑦))
26		cplusg 16888	. . . . . . . . . . . 12 class +g
27	11, 26	cfv 6418	. . . . . . . . . . 11 class (+g‘𝑟)
28	5, 17, 27	co 7255	. . . . . . . . . 10 class (𝑥(+g‘𝑟)𝑦)
29	28, 7	cfv 6418	. . . . . . . . 9 class (𝑓‘(𝑥(+g‘𝑟)𝑦))
30		caddc 10805	. . . . . . . . . 10 class +
31	8, 22, 30	co 7255	. . . . . . . . 9 class ((𝑓‘𝑥) + (𝑓‘𝑦))
32		cle 10941	. . . . . . . . 9 class ≤
33	29, 31, 32	wbr 5070	. . . . . . . 8 wff (𝑓‘(𝑥(+g‘𝑟)𝑦)) ≤ ((𝑓‘𝑥) + (𝑓‘𝑦))
34	25, 33	wa 395	. . . . . . 7 wff ((𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥) · (𝑓‘𝑦)) ∧ (𝑓‘(𝑥(+g‘𝑟)𝑦)) ≤ ((𝑓‘𝑥) + (𝑓‘𝑦)))
35		cbs 16840	. . . . . . . 8 class Base
36	11, 35	cfv 6418	. . . . . . 7 class (Base‘𝑟)
37	34, 16, 36	wral 3063	. . . . . 6 wff ∀𝑦 ∈ (Base‘𝑟)((𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥) · (𝑓‘𝑦)) ∧ (𝑓‘(𝑥(+g‘𝑟)𝑦)) ≤ ((𝑓‘𝑥) + (𝑓‘𝑦)))
38	15, 37	wa 395	. . . . 5 wff (((𝑓‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑟)) ∧ ∀𝑦 ∈ (Base‘𝑟)((𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥) · (𝑓‘𝑦)) ∧ (𝑓‘(𝑥(+g‘𝑟)𝑦)) ≤ ((𝑓‘𝑥) + (𝑓‘𝑦))))
39	38, 4, 36	wral 3063	. . . 4 wff ∀𝑥 ∈ (Base‘𝑟)(((𝑓‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑟)) ∧ ∀𝑦 ∈ (Base‘𝑟)((𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥) · (𝑓‘𝑦)) ∧ (𝑓‘(𝑥(+g‘𝑟)𝑦)) ≤ ((𝑓‘𝑥) + (𝑓‘𝑦))))
40		cpnf 10937	. . . . . 6 class +∞
41		cico 13010	. . . . . 6 class [,)
42	9, 40, 41	co 7255	. . . . 5 class (0[,)+∞)
43		cmap 8573	. . . . 5 class ↑m
44	42, 36, 43	co 7255	. . . 4 class ((0[,)+∞) ↑m (Base‘𝑟))
45	39, 6, 44	crab 3067	. . 3 class {𝑓 ∈ ((0[,)+∞) ↑m (Base‘𝑟)) ∣ ∀𝑥 ∈ (Base‘𝑟)(((𝑓‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑟)) ∧ ∀𝑦 ∈ (Base‘𝑟)((𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥) · (𝑓‘𝑦)) ∧ (𝑓‘(𝑥(+g‘𝑟)𝑦)) ≤ ((𝑓‘𝑥) + (𝑓‘𝑦))))}
46	2, 3, 45	cmpt 5153	. 2 class (𝑟 ∈ Ring ↦ {𝑓 ∈ ((0[,)+∞) ↑m (Base‘𝑟)) ∣ ∀𝑥 ∈ (Base‘𝑟)(((𝑓‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑟)) ∧ ∀𝑦 ∈ (Base‘𝑟)((𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥) · (𝑓‘𝑦)) ∧ (𝑓‘(𝑥(+g‘𝑟)𝑦)) ≤ ((𝑓‘𝑥) + (𝑓‘𝑦))))})
47	1, 46	wceq 1539	1 wff AbsVal = (𝑟 ∈ Ring ↦ {𝑓 ∈ ((0[,)+∞) ↑m (Base‘𝑟)) ∣ ∀𝑥 ∈ (Base‘𝑟)(((𝑓‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑟)) ∧ ∀𝑦 ∈ (Base‘𝑟)((𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥) · (𝑓‘𝑦)) ∧ (𝑓‘(𝑥(+g‘𝑟)𝑦)) ≤ ((𝑓‘𝑥) + (𝑓‘𝑦))))})

This definition is referenced by:  abvfval  19993  abvrcl  19996