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 ⊢ ≤
37 caddc ⊢ +
38 16 29 37 co ⊢ ( ( 𝑓 ‘ 𝑥 ) + ( 𝑓 ‘ 𝑦 ) )
39 35 38 36 wbr ⊢ ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) ≤ ( ( 𝑓 ‘ 𝑥 ) + ( 𝑓 ‘ 𝑦 ) )
40 31 39 wa ⊢ ( ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) ≤ ( ( 𝑓 ‘ 𝑥 ) + ( 𝑓 ‘ 𝑦 ) ) )
41 40 22 11 wral ⊢ ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) ≤ ( ( 𝑓 ‘ 𝑥 ) + ( 𝑓 ‘ 𝑦 ) ) )
42 21 41 wa ⊢ ( ( ( 𝑓 ‘ 𝑥 ) = 0 ↔ 𝑥 = ( 0g ‘ 𝑟 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) ≤ ( ( 𝑓 ‘ 𝑥 ) + ( 𝑓 ‘ 𝑦 ) ) ) )
43 42 13 11 wral ⊢ ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ( ( ( 𝑓 ‘ 𝑥 ) = 0 ↔ 𝑥 = ( 0g ‘ 𝑟 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) ≤ ( ( 𝑓 ‘ 𝑥 ) + ( 𝑓 ‘ 𝑦 ) ) ) )
44 43 3 12 crab ⊢ { 𝑓 ∈ ( ( 0 [,) +∞ ) ↑m ( Base ‘ 𝑟 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ( ( ( 𝑓 ‘ 𝑥 ) = 0 ↔ 𝑥 = ( 0g ‘ 𝑟 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) ≤ ( ( 𝑓 ‘ 𝑥 ) + ( 𝑓 ‘ 𝑦 ) ) ) ) }
45 1 2 44 cmpt ⊢ ( 𝑟 ∈ Ring ↦ { 𝑓 ∈ ( ( 0 [,) +∞ ) ↑m ( Base ‘ 𝑟 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ( ( ( 𝑓 ‘ 𝑥 ) = 0 ↔ 𝑥 = ( 0g ‘ 𝑟 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) ≤ ( ( 𝑓 ‘ 𝑥 ) + ( 𝑓 ‘ 𝑦 ) ) ) ) } )
46 0 45 wceq ⊢ AbsVal = ( 𝑟 ∈ Ring ↦ { 𝑓 ∈ ( ( 0 [,) +∞ ) ↑m ( Base ‘ 𝑟 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ( ( ( 𝑓 ‘ 𝑥 ) = 0 ↔ 𝑥 = ( 0g ‘ 𝑟 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) ≤ ( ( 𝑓 ‘ 𝑥 ) + ( 𝑓 ‘ 𝑦 ) ) ) ) } )