MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-abv Structured version   Visualization version   GIF version

Definition df-abv 18586
Description: Define the set of absolute values on a ring. An absolute value is a generalization of the usual absolute value function df-abs 13770 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
StepHypRef Expression
1 cabv 18585 . 2 class AbsVal
2 vr . . 3 setvar 𝑟
3 crg 18316 . . 3 class Ring
4 vx . . . . . . . . . 10 setvar 𝑥
54cv 1473 . . . . . . . . 9 class 𝑥
6 vf . . . . . . . . . 10 setvar 𝑓
76cv 1473 . . . . . . . . 9 class 𝑓
85, 7cfv 5790 . . . . . . . 8 class (𝑓𝑥)
9 cc0 9792 . . . . . . . 8 class 0
108, 9wceq 1474 . . . . . . 7 wff (𝑓𝑥) = 0
112cv 1473 . . . . . . . . 9 class 𝑟
12 c0g 15869 . . . . . . . . 9 class 0g
1311, 12cfv 5790 . . . . . . . 8 class (0g𝑟)
145, 13wceq 1474 . . . . . . 7 wff 𝑥 = (0g𝑟)
1510, 14wb 194 . . . . . 6 wff ((𝑓𝑥) = 0 ↔ 𝑥 = (0g𝑟))
16 vy . . . . . . . . . . . 12 setvar 𝑦
1716cv 1473 . . . . . . . . . . 11 class 𝑦
18 cmulr 15715 . . . . . . . . . . . 12 class .r
1911, 18cfv 5790 . . . . . . . . . . 11 class (.r𝑟)
205, 17, 19co 6527 . . . . . . . . . 10 class (𝑥(.r𝑟)𝑦)
2120, 7cfv 5790 . . . . . . . . 9 class (𝑓‘(𝑥(.r𝑟)𝑦))
2217, 7cfv 5790 . . . . . . . . . 10 class (𝑓𝑦)
23 cmul 9797 . . . . . . . . . 10 class ·
248, 22, 23co 6527 . . . . . . . . 9 class ((𝑓𝑥) · (𝑓𝑦))
2521, 24wceq 1474 . . . . . . . 8 wff (𝑓‘(𝑥(.r𝑟)𝑦)) = ((𝑓𝑥) · (𝑓𝑦))
26 cplusg 15714 . . . . . . . . . . . 12 class +g
2711, 26cfv 5790 . . . . . . . . . . 11 class (+g𝑟)
285, 17, 27co 6527 . . . . . . . . . 10 class (𝑥(+g𝑟)𝑦)
2928, 7cfv 5790 . . . . . . . . 9 class (𝑓‘(𝑥(+g𝑟)𝑦))
30 caddc 9795 . . . . . . . . . 10 class +
318, 22, 30co 6527 . . . . . . . . 9 class ((𝑓𝑥) + (𝑓𝑦))
32 cle 9931 . . . . . . . . 9 class
3329, 31, 32wbr 4577 . . . . . . . 8 wff (𝑓‘(𝑥(+g𝑟)𝑦)) ≤ ((𝑓𝑥) + (𝑓𝑦))
3425, 33wa 382 . . . . . . 7 wff ((𝑓‘(𝑥(.r𝑟)𝑦)) = ((𝑓𝑥) · (𝑓𝑦)) ∧ (𝑓‘(𝑥(+g𝑟)𝑦)) ≤ ((𝑓𝑥) + (𝑓𝑦)))
35 cbs 15641 . . . . . . . 8 class Base
3611, 35cfv 5790 . . . . . . 7 class (Base‘𝑟)
3734, 16, 36wral 2895 . . . . . 6 wff 𝑦 ∈ (Base‘𝑟)((𝑓‘(𝑥(.r𝑟)𝑦)) = ((𝑓𝑥) · (𝑓𝑦)) ∧ (𝑓‘(𝑥(+g𝑟)𝑦)) ≤ ((𝑓𝑥) + (𝑓𝑦)))
3815, 37wa 382 . . . . 5 wff (((𝑓𝑥) = 0 ↔ 𝑥 = (0g𝑟)) ∧ ∀𝑦 ∈ (Base‘𝑟)((𝑓‘(𝑥(.r𝑟)𝑦)) = ((𝑓𝑥) · (𝑓𝑦)) ∧ (𝑓‘(𝑥(+g𝑟)𝑦)) ≤ ((𝑓𝑥) + (𝑓𝑦))))
3938, 4, 36wral 2895 . . . 4 wff 𝑥 ∈ (Base‘𝑟)(((𝑓𝑥) = 0 ↔ 𝑥 = (0g𝑟)) ∧ ∀𝑦 ∈ (Base‘𝑟)((𝑓‘(𝑥(.r𝑟)𝑦)) = ((𝑓𝑥) · (𝑓𝑦)) ∧ (𝑓‘(𝑥(+g𝑟)𝑦)) ≤ ((𝑓𝑥) + (𝑓𝑦))))
40 cpnf 9927 . . . . . 6 class +∞
41 cico 12004 . . . . . 6 class [,)
429, 40, 41co 6527 . . . . 5 class (0[,)+∞)
43 cmap 7721 . . . . 5 class 𝑚
4442, 36, 43co 6527 . . . 4 class ((0[,)+∞) ↑𝑚 (Base‘𝑟))
4539, 6, 44crab 2899 . . 3 class {𝑓 ∈ ((0[,)+∞) ↑𝑚 (Base‘𝑟)) ∣ ∀𝑥 ∈ (Base‘𝑟)(((𝑓𝑥) = 0 ↔ 𝑥 = (0g𝑟)) ∧ ∀𝑦 ∈ (Base‘𝑟)((𝑓‘(𝑥(.r𝑟)𝑦)) = ((𝑓𝑥) · (𝑓𝑦)) ∧ (𝑓‘(𝑥(+g𝑟)𝑦)) ≤ ((𝑓𝑥) + (𝑓𝑦))))}
462, 3, 45cmpt 4637 . 2 class (𝑟 ∈ Ring ↦ {𝑓 ∈ ((0[,)+∞) ↑𝑚 (Base‘𝑟)) ∣ ∀𝑥 ∈ (Base‘𝑟)(((𝑓𝑥) = 0 ↔ 𝑥 = (0g𝑟)) ∧ ∀𝑦 ∈ (Base‘𝑟)((𝑓‘(𝑥(.r𝑟)𝑦)) = ((𝑓𝑥) · (𝑓𝑦)) ∧ (𝑓‘(𝑥(+g𝑟)𝑦)) ≤ ((𝑓𝑥) + (𝑓𝑦))))})
471, 46wceq 1474 1 wff AbsVal = (𝑟 ∈ Ring ↦ {𝑓 ∈ ((0[,)+∞) ↑𝑚 (Base‘𝑟)) ∣ ∀𝑥 ∈ (Base‘𝑟)(((𝑓𝑥) = 0 ↔ 𝑥 = (0g𝑟)) ∧ ∀𝑦 ∈ (Base‘𝑟)((𝑓‘(𝑥(.r𝑟)𝑦)) = ((𝑓𝑥) · (𝑓𝑦)) ∧ (𝑓‘(𝑥(+g𝑟)𝑦)) ≤ ((𝑓𝑥) + (𝑓𝑦))))})
Colors of variables: wff setvar class
This definition is referenced by:  abvfval  18587  abvrcl  18590
  Copyright terms: Public domain W3C validator