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 ) ∧ ∀ 𝑦𝐵 ( ( 𝑓 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑓𝑥 ) · ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( 𝑓𝑥 ) + ( 𝑓𝑦 ) ) ) ) } )