Step | Hyp | Ref
| Expression |
1 | | abvfval.a |
. 2
⊢ 𝐴 = (AbsVal‘𝑅) |
2 | | fveq2 6191 |
. . . . . 6
⊢ (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅)) |
3 | | abvfval.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑅) |
4 | 2, 3 | syl6eqr 2674 |
. . . . 5
⊢ (𝑟 = 𝑅 → (Base‘𝑟) = 𝐵) |
5 | 4 | oveq2d 6666 |
. . . 4
⊢ (𝑟 = 𝑅 → ((0[,)+∞)
↑𝑚 (Base‘𝑟)) = ((0[,)+∞)
↑𝑚 𝐵)) |
6 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → (0g‘𝑟) = (0g‘𝑅)) |
7 | | abvfval.z |
. . . . . . . . 9
⊢ 0 =
(0g‘𝑅) |
8 | 6, 7 | syl6eqr 2674 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → (0g‘𝑟) = 0 ) |
9 | 8 | eqeq2d 2632 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → (𝑥 = (0g‘𝑟) ↔ 𝑥 = 0 )) |
10 | 9 | bibi2d 332 |
. . . . . 6
⊢ (𝑟 = 𝑅 → (((𝑓‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑟)) ↔ ((𝑓‘𝑥) = 0 ↔ 𝑥 = 0 ))) |
11 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑟 = 𝑅 → (.r‘𝑟) = (.r‘𝑅)) |
12 | | abvfval.t |
. . . . . . . . . . . 12
⊢ · =
(.r‘𝑅) |
13 | 11, 12 | syl6eqr 2674 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑅 → (.r‘𝑟) = · ) |
14 | 13 | oveqd 6667 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 → (𝑥(.r‘𝑟)𝑦) = (𝑥 · 𝑦)) |
15 | 14 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → (𝑓‘(𝑥(.r‘𝑟)𝑦)) = (𝑓‘(𝑥 · 𝑦))) |
16 | 15 | eqeq1d 2624 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → ((𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥) · (𝑓‘𝑦)) ↔ (𝑓‘(𝑥 · 𝑦)) = ((𝑓‘𝑥) · (𝑓‘𝑦)))) |
17 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑟 = 𝑅 → (+g‘𝑟) = (+g‘𝑅)) |
18 | | abvfval.p |
. . . . . . . . . . . 12
⊢ + =
(+g‘𝑅) |
19 | 17, 18 | syl6eqr 2674 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑅 → (+g‘𝑟) = + ) |
20 | 19 | oveqd 6667 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 → (𝑥(+g‘𝑟)𝑦) = (𝑥 + 𝑦)) |
21 | 20 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → (𝑓‘(𝑥(+g‘𝑟)𝑦)) = (𝑓‘(𝑥 + 𝑦))) |
22 | 21 | breq1d 4663 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → ((𝑓‘(𝑥(+g‘𝑟)𝑦)) ≤ ((𝑓‘𝑥) + (𝑓‘𝑦)) ↔ (𝑓‘(𝑥 + 𝑦)) ≤ ((𝑓‘𝑥) + (𝑓‘𝑦)))) |
23 | 16, 22 | anbi12d 747 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → (((𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥) · (𝑓‘𝑦)) ∧ (𝑓‘(𝑥(+g‘𝑟)𝑦)) ≤ ((𝑓‘𝑥) + (𝑓‘𝑦))) ↔ ((𝑓‘(𝑥 · 𝑦)) = ((𝑓‘𝑥) · (𝑓‘𝑦)) ∧ (𝑓‘(𝑥 + 𝑦)) ≤ ((𝑓‘𝑥) + (𝑓‘𝑦))))) |
24 | 4, 23 | raleqbidv 3152 |
. . . . . 6
⊢ (𝑟 = 𝑅 → (∀𝑦 ∈ (Base‘𝑟)((𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥) · (𝑓‘𝑦)) ∧ (𝑓‘(𝑥(+g‘𝑟)𝑦)) ≤ ((𝑓‘𝑥) + (𝑓‘𝑦))) ↔ ∀𝑦 ∈ 𝐵 ((𝑓‘(𝑥 · 𝑦)) = ((𝑓‘𝑥) · (𝑓‘𝑦)) ∧ (𝑓‘(𝑥 + 𝑦)) ≤ ((𝑓‘𝑥) + (𝑓‘𝑦))))) |
25 | 10, 24 | anbi12d 747 |
. . . . 5
⊢ (𝑟 = 𝑅 → ((((𝑓‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑟)) ∧ ∀𝑦 ∈ (Base‘𝑟)((𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥) · (𝑓‘𝑦)) ∧ (𝑓‘(𝑥(+g‘𝑟)𝑦)) ≤ ((𝑓‘𝑥) + (𝑓‘𝑦)))) ↔ (((𝑓‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝐵 ((𝑓‘(𝑥 · 𝑦)) = ((𝑓‘𝑥) · (𝑓‘𝑦)) ∧ (𝑓‘(𝑥 + 𝑦)) ≤ ((𝑓‘𝑥) + (𝑓‘𝑦)))))) |
26 | 4, 25 | raleqbidv 3152 |
. . . 4
⊢ (𝑟 = 𝑅 → (∀𝑥 ∈ (Base‘𝑟)(((𝑓‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑟)) ∧ ∀𝑦 ∈ (Base‘𝑟)((𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥) · (𝑓‘𝑦)) ∧ (𝑓‘(𝑥(+g‘𝑟)𝑦)) ≤ ((𝑓‘𝑥) + (𝑓‘𝑦)))) ↔ ∀𝑥 ∈ 𝐵 (((𝑓‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝐵 ((𝑓‘(𝑥 · 𝑦)) = ((𝑓‘𝑥) · (𝑓‘𝑦)) ∧ (𝑓‘(𝑥 + 𝑦)) ≤ ((𝑓‘𝑥) + (𝑓‘𝑦)))))) |
27 | 5, 26 | rabeqbidv 3195 |
. . 3
⊢ (𝑟 = 𝑅 → {𝑓 ∈ ((0[,)+∞)
↑𝑚 (Base‘𝑟)) ∣ ∀𝑥 ∈ (Base‘𝑟)(((𝑓‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑟)) ∧ ∀𝑦 ∈ (Base‘𝑟)((𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥) · (𝑓‘𝑦)) ∧ (𝑓‘(𝑥(+g‘𝑟)𝑦)) ≤ ((𝑓‘𝑥) + (𝑓‘𝑦))))} = {𝑓 ∈ ((0[,)+∞)
↑𝑚 𝐵) ∣ ∀𝑥 ∈ 𝐵 (((𝑓‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝐵 ((𝑓‘(𝑥 · 𝑦)) = ((𝑓‘𝑥) · (𝑓‘𝑦)) ∧ (𝑓‘(𝑥 + 𝑦)) ≤ ((𝑓‘𝑥) + (𝑓‘𝑦))))}) |
28 | | df-abv 18817 |
. . 3
⊢ AbsVal =
(𝑟 ∈ Ring ↦
{𝑓 ∈ ((0[,)+∞)
↑𝑚 (Base‘𝑟)) ∣ ∀𝑥 ∈ (Base‘𝑟)(((𝑓‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑟)) ∧ ∀𝑦 ∈ (Base‘𝑟)((𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥) · (𝑓‘𝑦)) ∧ (𝑓‘(𝑥(+g‘𝑟)𝑦)) ≤ ((𝑓‘𝑥) + (𝑓‘𝑦))))}) |
29 | | ovex 6678 |
. . . 4
⊢
((0[,)+∞) ↑𝑚 𝐵) ∈ V |
30 | 29 | rabex 4813 |
. . 3
⊢ {𝑓 ∈ ((0[,)+∞)
↑𝑚 𝐵) ∣ ∀𝑥 ∈ 𝐵 (((𝑓‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝐵 ((𝑓‘(𝑥 · 𝑦)) = ((𝑓‘𝑥) · (𝑓‘𝑦)) ∧ (𝑓‘(𝑥 + 𝑦)) ≤ ((𝑓‘𝑥) + (𝑓‘𝑦))))} ∈ V |
31 | 27, 28, 30 | fvmpt 6282 |
. 2
⊢ (𝑅 ∈ Ring →
(AbsVal‘𝑅) = {𝑓 ∈ ((0[,)+∞)
↑𝑚 𝐵) ∣ ∀𝑥 ∈ 𝐵 (((𝑓‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝐵 ((𝑓‘(𝑥 · 𝑦)) = ((𝑓‘𝑥) · (𝑓‘𝑦)) ∧ (𝑓‘(𝑥 + 𝑦)) ≤ ((𝑓‘𝑥) + (𝑓‘𝑦))))}) |
32 | 1, 31 | syl5eq 2668 |
1
⊢ (𝑅 ∈ Ring → 𝐴 = {𝑓 ∈ ((0[,)+∞)
↑𝑚 𝐵) ∣ ∀𝑥 ∈ 𝐵 (((𝑓‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝐵 ((𝑓‘(𝑥 · 𝑦)) = ((𝑓‘𝑥) · (𝑓‘𝑦)) ∧ (𝑓‘(𝑥 + 𝑦)) ≤ ((𝑓‘𝑥) + (𝑓‘𝑦))))}) |