Definition df-abv 18640

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

Assertion

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

Distinct variable group:   𝑓,𝑟,𝑥,𝑦

Detailed syntax breakdown of Definition df-abv

Step	Hyp	Ref	Expression
1		cabv 18639	. 2 class AbsVal
2		vr	. . 3 setvar 𝑟
3		crg 18370	. . 3 class Ring
4		vx	. . . . . . . . . 10 setvar 𝑥
5	4	cv 1474	. . . . . . . . 9 class 𝑥
6		vf	. . . . . . . . . 10 setvar 𝑓
7	6	cv 1474	. . . . . . . . 9 class 𝑓
8	5, 7	cfv 5804	. . . . . . . 8 class (𝑓‘𝑥)
9		cc0 9815	. . . . . . . 8 class 0
10	8, 9	wceq 1475	. . . . . . 7 wff (𝑓‘𝑥) = 0
11	2	cv 1474	. . . . . . . . 9 class 𝑟
12		c0g 15923	. . . . . . . . 9 class 0g
13	11, 12	cfv 5804	. . . . . . . 8 class (0g‘𝑟)
14	5, 13	wceq 1475	. . . . . . 7 wff 𝑥 = (0g‘𝑟)
15	10, 14	wb 195	. . . . . 6 wff ((𝑓‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑟))
16		vy	. . . . . . . . . . . 12 setvar 𝑦
17	16	cv 1474	. . . . . . . . . . 11 class 𝑦
18		cmulr 15769	. . . . . . . . . . . 12 class .r
19	11, 18	cfv 5804	. . . . . . . . . . 11 class (.r‘𝑟)
20	5, 17, 19	co 6549	. . . . . . . . . 10 class (𝑥(.r‘𝑟)𝑦)
21	20, 7	cfv 5804	. . . . . . . . 9 class (𝑓‘(𝑥(.r‘𝑟)𝑦))
22	17, 7	cfv 5804	. . . . . . . . . 10 class (𝑓‘𝑦)
23		cmul 9820	. . . . . . . . . 10 class ·
24	8, 22, 23	co 6549	. . . . . . . . 9 class ((𝑓‘𝑥) · (𝑓‘𝑦))
25	21, 24	wceq 1475	. . . . . . . 8 wff (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥) · (𝑓‘𝑦))
26		cplusg 15768	. . . . . . . . . . . 12 class +g
27	11, 26	cfv 5804	. . . . . . . . . . 11 class (+g‘𝑟)
28	5, 17, 27	co 6549	. . . . . . . . . 10 class (𝑥(+g‘𝑟)𝑦)
29	28, 7	cfv 5804	. . . . . . . . 9 class (𝑓‘(𝑥(+g‘𝑟)𝑦))
30		caddc 9818	. . . . . . . . . 10 class +
31	8, 22, 30	co 6549	. . . . . . . . 9 class ((𝑓‘𝑥) + (𝑓‘𝑦))
32		cle 9954	. . . . . . . . 9 class ≤
33	29, 31, 32	wbr 4583	. . . . . . . 8 wff (𝑓‘(𝑥(+g‘𝑟)𝑦)) ≤ ((𝑓‘𝑥) + (𝑓‘𝑦))
34	25, 33	wa 383	. . . . . . 7 wff ((𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥) · (𝑓‘𝑦)) ∧ (𝑓‘(𝑥(+g‘𝑟)𝑦)) ≤ ((𝑓‘𝑥) + (𝑓‘𝑦)))
35		cbs 15695	. . . . . . . 8 class Base
36	11, 35	cfv 5804	. . . . . . 7 class (Base‘𝑟)
37	34, 16, 36	wral 2896	. . . . . 6 wff ∀𝑦 ∈ (Base‘𝑟)((𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥) · (𝑓‘𝑦)) ∧ (𝑓‘(𝑥(+g‘𝑟)𝑦)) ≤ ((𝑓‘𝑥) + (𝑓‘𝑦)))
38	15, 37	wa 383	. . . . 5 wff (((𝑓‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑟)) ∧ ∀𝑦 ∈ (Base‘𝑟)((𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥) · (𝑓‘𝑦)) ∧ (𝑓‘(𝑥(+g‘𝑟)𝑦)) ≤ ((𝑓‘𝑥) + (𝑓‘𝑦))))
39	38, 4, 36	wral 2896	. . . 4 wff ∀𝑥 ∈ (Base‘𝑟)(((𝑓‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑟)) ∧ ∀𝑦 ∈ (Base‘𝑟)((𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥) · (𝑓‘𝑦)) ∧ (𝑓‘(𝑥(+g‘𝑟)𝑦)) ≤ ((𝑓‘𝑥) + (𝑓‘𝑦))))
40		cpnf 9950	. . . . . 6 class +∞
41		cico 12048	. . . . . 6 class [,)
42	9, 40, 41	co 6549	. . . . 5 class (0[,)+∞)
43		cmap 7744	. . . . 5 class ↑𝑚
44	42, 36, 43	co 6549	. . . 4 class ((0[,)+∞) ↑𝑚 (Base‘𝑟))
45	39, 6, 44	crab 2900	. . 3 class {𝑓 ∈ ((0[,)+∞) ↑𝑚 (Base‘𝑟)) ∣ ∀𝑥 ∈ (Base‘𝑟)(((𝑓‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑟)) ∧ ∀𝑦 ∈ (Base‘𝑟)((𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥) · (𝑓‘𝑦)) ∧ (𝑓‘(𝑥(+g‘𝑟)𝑦)) ≤ ((𝑓‘𝑥) + (𝑓‘𝑦))))}
46	2, 3, 45	cmpt 4643	. 2 class (𝑟 ∈ Ring ↦ {𝑓 ∈ ((0[,)+∞) ↑𝑚 (Base‘𝑟)) ∣ ∀𝑥 ∈ (Base‘𝑟)(((𝑓‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑟)) ∧ ∀𝑦 ∈ (Base‘𝑟)((𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥) · (𝑓‘𝑦)) ∧ (𝑓‘(𝑥(+g‘𝑟)𝑦)) ≤ ((𝑓‘𝑥) + (𝑓‘𝑦))))})
47	1, 46	wceq 1475	1 wff AbsVal = (𝑟 ∈ Ring ↦ {𝑓 ∈ ((0[,)+∞) ↑𝑚 (Base‘𝑟)) ∣ ∀𝑥 ∈ (Base‘𝑟)(((𝑓‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑟)) ∧ ∀𝑦 ∈ (Base‘𝑟)((𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥) · (𝑓‘𝑦)) ∧ (𝑓‘(𝑥(+g‘𝑟)𝑦)) ≤ ((𝑓‘𝑥) + (𝑓‘𝑦))))})

This definition is referenced by:  abvfval  18641  abvrcl  18644