# Metamath Proof Explorer

## Definition df-abv

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

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

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cabv AbsVal
1 vr 𝑟
2 crg Ring
3 vf 𝑓
4 cc0 0
5 cico [,)
6 cpnf +∞
7 4 6 5 co ( 0 [,) +∞ )
8 cmap m
9 cbs Base
10 1 cv 𝑟
11 10 9 cfv ( Base ‘ 𝑟 )
12 7 11 8 co ( ( 0 [,) +∞ ) ↑m ( Base ‘ 𝑟 ) )
13 vx 𝑥
14 3 cv 𝑓
15 13 cv 𝑥
16 15 14 cfv ( 𝑓𝑥 )
17 16 4 wceq ( 𝑓𝑥 ) = 0
18 c0g 0g
19 10 18 cfv ( 0g𝑟 )
20 15 19 wceq 𝑥 = ( 0g𝑟 )
21 17 20 wb ( ( 𝑓𝑥 ) = 0 ↔ 𝑥 = ( 0g𝑟 ) )
22 vy 𝑦
23 cmulr .r
24 10 23 cfv ( .r𝑟 )
25 22 cv 𝑦
26 15 25 24 co ( 𝑥 ( .r𝑟 ) 𝑦 )
27 26 14 cfv ( 𝑓 ‘ ( 𝑥 ( .r𝑟 ) 𝑦 ) )
28 cmul ·
29 25 14 cfv ( 𝑓𝑦 )
30 16 29 28 co ( ( 𝑓𝑥 ) · ( 𝑓𝑦 ) )
31 27 30 wceq ( 𝑓 ‘ ( 𝑥 ( .r𝑟 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) · ( 𝑓𝑦 ) )
32 cplusg +g
33 10 32 cfv ( +g𝑟 )
34 15 25 33 co ( 𝑥 ( +g𝑟 ) 𝑦 )
35 34 14 cfv ( 𝑓 ‘ ( 𝑥 ( +g𝑟 ) 𝑦 ) )
36 cle