Definition df-abv 21059

Description: Define the set of absolute values on a ring. An absolute value is a generalization of the usual absolute value function df-abs 15396 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 21058	. 2 class AbsVal
2		vr	. . 3 setvar 𝑟
3		crg 20452	. . 3 class Ring
4		vx	. . . . . . . . . 10 setvar 𝑥
5	4	cv 1569	. . . . . . . . 9 class 𝑥
6		vf	. . . . . . . . . 10 setvar 𝑓
7	6	cv 1569	. . . . . . . . 9 class 𝑓
8	5, 7	cfv 6537	. . . . . . . 8 class (𝑓‘𝑥)
9		cc0 11193	. . . . . . . 8 class 0
10	8, 9	wceq 1570	. . . . . . 7 wff (𝑓‘𝑥) = 0
11	2	cv 1569	. . . . . . . . 9 class 𝑟
12		c0g 17603	. . . . . . . . 9 class 0g
13	11, 12	cfv 6537	. . . . . . . 8 class (0g‘𝑟)
14	5, 13	wceq 1570	. . . . . . 7 wff 𝑥 = (0g‘𝑟)
15	10, 14	wb 209	. . . . . 6 wff ((𝑓‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑟))
16		vy	. . . . . . . . . . . 12 setvar 𝑦
17	16	cv 1569	. . . . . . . . . . 11 class 𝑦
18		cmulr 17422	. . . . . . . . . . . 12 class .r
19	11, 18	cfv 6537	. . . . . . . . . . 11 class (.r‘𝑟)
20	5, 17, 19	co 7418	. . . . . . . . . 10 class (𝑥(.r‘𝑟)𝑦)
21	20, 7	cfv 6537	. . . . . . . . 9 class (𝑓‘(𝑥(.r‘𝑟)𝑦))
22	17, 7	cfv 6537	. . . . . . . . . 10 class (𝑓‘𝑦)
23		cmul 11198	. . . . . . . . . 10 class ·
24	8, 22, 23	co 7418	. . . . . . . . 9 class ((𝑓‘𝑥) · (𝑓‘𝑦))
25	21, 24	wceq 1570	. . . . . . . 8 wff (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥) · (𝑓‘𝑦))
26		cplusg 17421	. . . . . . . . . . . 12 class +g
27	11, 26	cfv 6537	. . . . . . . . . . 11 class (+g‘𝑟)
28	5, 17, 27	co 7418	. . . . . . . . . 10 class (𝑥(+g‘𝑟)𝑦)
29	28, 7	cfv 6537	. . . . . . . . 9 class (𝑓‘(𝑥(+g‘𝑟)𝑦))
30		caddc 11196	. . . . . . . . . 10 class +
31	8, 22, 30	co 7418	. . . . . . . . 9 class ((𝑓‘𝑥) + (𝑓‘𝑦))
32		cle 11337	. . . . . . . . 9 class ≤
33	29, 31, 32	wbr 5103	. . . . . . . 8 wff (𝑓‘(𝑥(+g‘𝑟)𝑦)) ≤ ((𝑓‘𝑥) + (𝑓‘𝑦))
34	25, 33	wa 401	. . . . . . 7 wff ((𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥) · (𝑓‘𝑦)) ∧ (𝑓‘(𝑥(+g‘𝑟)𝑦)) ≤ ((𝑓‘𝑥) + (𝑓‘𝑦)))
35		cbs 17380	. . . . . . . 8 class Base
36	11, 35	cfv 6537	. . . . . . 7 class (Base‘𝑟)
37	34, 16, 36	wral 3077	. . . . . 6 wff ∀𝑦 ∈ (Base‘𝑟)((𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥) · (𝑓‘𝑦)) ∧ (𝑓‘(𝑥(+g‘𝑟)𝑦)) ≤ ((𝑓‘𝑥) + (𝑓‘𝑦)))
38	15, 37	wa 401	. . . . 5 wff (((𝑓‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑟)) ∧ ∀𝑦 ∈ (Base‘𝑟)((𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥) · (𝑓‘𝑦)) ∧ (𝑓‘(𝑥(+g‘𝑟)𝑦)) ≤ ((𝑓‘𝑥) + (𝑓‘𝑦))))
39	38, 4, 36	wral 3077	. . . 4 wff ∀𝑥 ∈ (Base‘𝑟)(((𝑓‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑟)) ∧ ∀𝑦 ∈ (Base‘𝑟)((𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥) · (𝑓‘𝑦)) ∧ (𝑓‘(𝑥(+g‘𝑟)𝑦)) ≤ ((𝑓‘𝑥) + (𝑓‘𝑦))))
40		cpnf 11333	. . . . . 6 class +∞
41		cico 13471	. . . . . 6 class [,)
42	9, 40, 41	co 7418	. . . . 5 class (0[,)+∞)
43		cmap 8840	. . . . 5 class ↑m
44	42, 36, 43	co 7418	. . . 4 class ((0[,)+∞) ↑m (Base‘𝑟))
45	39, 6, 44	crab 3413	. . 3 class {𝑓 ∈ ((0[,)+∞) ↑m (Base‘𝑟)) ∣ ∀𝑥 ∈ (Base‘𝑟)(((𝑓‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑟)) ∧ ∀𝑦 ∈ (Base‘𝑟)((𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥) · (𝑓‘𝑦)) ∧ (𝑓‘(𝑥(+g‘𝑟)𝑦)) ≤ ((𝑓‘𝑥) + (𝑓‘𝑦))))}
46	2, 3, 45	cmpt 5186	. 2 class (𝑟 ∈ Ring ↦ {𝑓 ∈ ((0[,)+∞) ↑m (Base‘𝑟)) ∣ ∀𝑥 ∈ (Base‘𝑟)(((𝑓‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑟)) ∧ ∀𝑦 ∈ (Base‘𝑟)((𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥) · (𝑓‘𝑦)) ∧ (𝑓‘(𝑥(+g‘𝑟)𝑦)) ≤ ((𝑓‘𝑥) + (𝑓‘𝑦))))})
47	1, 46	wceq 1570	1 wff AbsVal = (𝑟 ∈ Ring ↦ {𝑓 ∈ ((0[,)+∞) ↑m (Base‘𝑟)) ∣ ∀𝑥 ∈ (Base‘𝑟)(((𝑓‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑟)) ∧ ∀𝑦 ∈ (Base‘𝑟)((𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥) · (𝑓‘𝑦)) ∧ (𝑓‘(𝑥(+g‘𝑟)𝑦)) ≤ ((𝑓‘𝑥) + (𝑓‘𝑦))))})

This definition is used by:  abvfval  21060  abvrcl  21063