Metamath Proof Explorer

Theorem abvfval

Description: Value of the set of absolute values. (Contributed by Mario Carneiro, 8-Sep-2014)

Ref Expression
Hypotheses abvfval.a ⊢ 𝐴 = ( AbsVal ‘ 𝑅 )
abvfval.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
abvfval.p ⊢ + = ( +g ‘ 𝑅 )
abvfval.t ⊢ · = ( .r ‘ 𝑅 )
abvfval.z ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion abvfval ( 𝑅 ∈ Ring → 𝐴 = { 𝑓 ∈ ( ( 0 [,) +∞ ) ↑m 𝐵 ) ∣ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑓 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑓 ‘ 𝑥 ) + ( 𝑓 ‘ 𝑦 ) ) ) ) } )

Proof

Step Hyp Ref Expression
1 abvfval.a ⊢ 𝐴 = ( AbsVal ‘ 𝑅 )
2 abvfval.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 abvfval.p ⊢ + = ( +g ‘ 𝑅 )
4 abvfval.t ⊢ · = ( .r ‘ 𝑅 )
5 abvfval.z ⊢ 0 = ( 0g ‘ 𝑅 )
6 fveq2 ⊢ ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) = ( Base ‘ 𝑅 ) )
7 6 2 eqtr4di ⊢ ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) = 𝐵 )
8 7 oveq2d ⊢ ( 𝑟 = 𝑅 → ( ( 0 [,) +∞ ) ↑m ( Base ‘ 𝑟 ) ) = ( ( 0 [,) +∞ ) ↑m 𝐵 ) )
9 fveq2 ⊢ ( 𝑟 = 𝑅 → ( 0g ‘ 𝑟 ) = ( 0g ‘ 𝑅 ) )
10 9 5 eqtr4di ⊢ ( 𝑟 = 𝑅 → ( 0g ‘ 𝑟 ) = 0 )
11 10 eqeq2d ⊢ ( 𝑟 = 𝑅 → ( 𝑥 = ( 0g ‘ 𝑟 ) ↔ 𝑥 = 0 ) )
12 11 bibi2d ⊢ ( 𝑟 = 𝑅 → ( ( ( 𝑓 ‘ 𝑥 ) = 0 ↔ 𝑥 = ( 0g ‘ 𝑟 ) ) ↔ ( ( 𝑓 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ) )
13 fveq2 ⊢ ( 𝑟 = 𝑅 → ( .r ‘ 𝑟 ) = ( .r ‘ 𝑅 ) )
14 13 4 eqtr4di ⊢ ( 𝑟 = 𝑅 → ( .r ‘ 𝑟 ) = · )
15 14 oveqd ⊢ ( 𝑟 = 𝑅 → ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) = ( 𝑥 · 𝑦 ) )
16 15 fveqeq2d ⊢ ( 𝑟 = 𝑅 → ( ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑦 ) ) ↔ ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑦 ) ) ) )
17 fveq2 ⊢ ( 𝑟 = 𝑅 → ( +g ‘ 𝑟 ) = ( +g ‘ 𝑅 ) )
18 17 3 eqtr4di ⊢ ( 𝑟 = 𝑅 → ( +g ‘ 𝑟 ) = + )
19 18 oveqd ⊢ ( 𝑟 = 𝑅 → ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) = ( 𝑥 + 𝑦 ) )
20 19 fveq2d ⊢ ( 𝑟 = 𝑅 → ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) )
21 20 breq1d ⊢ ( 𝑟 = 𝑅 → ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) ≤ ( ( 𝑓 ‘ 𝑥 ) + ( 𝑓 ‘ 𝑦 ) ) ↔ ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑓 ‘ 𝑥 ) + ( 𝑓 ‘ 𝑦 ) ) ) )
22 16 21 anbi12d ⊢ ( 𝑟 = 𝑅 → ( ( ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) ≤ ( ( 𝑓 ‘ 𝑥 ) + ( 𝑓 ‘ 𝑦 ) ) ) ↔ ( ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑓 ‘ 𝑥 ) + ( 𝑓 ‘ 𝑦 ) ) ) ) )
23 7 22 raleqbidv ⊢ ( 𝑟 = 𝑅 → ( ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) ≤ ( ( 𝑓 ‘ 𝑥 ) + ( 𝑓 ‘ 𝑦 ) ) ) ↔ ∀ 𝑦 ∈ 𝐵 ( ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑓 ‘ 𝑥 ) + ( 𝑓 ‘ 𝑦 ) ) ) ) )
24 12 23 anbi12d ⊢ ( 𝑟 = 𝑅 → ( ( ( ( 𝑓 ‘ 𝑥 ) = 0 ↔ 𝑥 = ( 0g ‘ 𝑟 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) ≤ ( ( 𝑓 ‘ 𝑥 ) + ( 𝑓 ‘ 𝑦 ) ) ) ) ↔ ( ( ( 𝑓 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑓 ‘ 𝑥 ) + ( 𝑓 ‘ 𝑦 ) ) ) ) ) )
25 7 24 raleqbidv ⊢ ( 𝑟 = 𝑅 → ( ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ( ( ( 𝑓 ‘ 𝑥 ) = 0 ↔ 𝑥 = ( 0g ‘ 𝑟 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) ≤ ( ( 𝑓 ‘ 𝑥 ) + ( 𝑓 ‘ 𝑦 ) ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑓 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑓 ‘ 𝑥 ) + ( 𝑓 ‘ 𝑦 ) ) ) ) ) )
26 8 25 rabeqbidv ⊢ ( 𝑟 = 𝑅 → { 𝑓 ∈ ( ( 0 [,) +∞ ) ↑m ( Base ‘ 𝑟 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ( ( ( 𝑓 ‘ 𝑥 ) = 0 ↔ 𝑥 = ( 0g ‘ 𝑟 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) ≤ ( ( 𝑓 ‘ 𝑥 ) + ( 𝑓 ‘ 𝑦 ) ) ) ) } = { 𝑓 ∈ ( ( 0 [,) +∞ ) ↑m 𝐵 ) ∣ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑓 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑓 ‘ 𝑥 ) + ( 𝑓 ‘ 𝑦 ) ) ) ) } )
27 df-abv ⊢ AbsVal = ( 𝑟 ∈ Ring ↦ { 𝑓 ∈ ( ( 0 [,) +∞ ) ↑m ( Base ‘ 𝑟 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ( ( ( 𝑓 ‘ 𝑥 ) = 0 ↔ 𝑥 = ( 0g ‘ 𝑟 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) ≤ ( ( 𝑓 ‘ 𝑥 ) + ( 𝑓 ‘ 𝑦 ) ) ) ) } )
28 ovex ⊢ ( ( 0 [,) +∞ ) ↑m 𝐵 ) ∈ V
29 28 rabex ⊢ { 𝑓 ∈ ( ( 0 [,) +∞ ) ↑m 𝐵 ) ∣ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑓 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑓 ‘ 𝑥 ) + ( 𝑓 ‘ 𝑦 ) ) ) ) } ∈ V
30 26 27 29 fvmpt ⊢ ( 𝑅 ∈ Ring → ( AbsVal ‘ 𝑅 ) = { 𝑓 ∈ ( ( 0 [,) +∞ ) ↑m 𝐵 ) ∣ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑓 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑓 ‘ 𝑥 ) + ( 𝑓 ‘ 𝑦 ) ) ) ) } )
31 1 30 syl5eq ⊢ ( 𝑅 ∈ Ring → 𝐴 = { 𝑓 ∈ ( ( 0 [,) +∞ ) ↑m 𝐵 ) ∣ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑓 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑓 ‘ 𝑥 ) + ( 𝑓 ‘ 𝑦 ) ) ) ) } )