Step | Hyp | Ref
| Expression |
1 | | abvf.a |
. . . . . . 7
⊢ 𝐴 = (AbsVal‘𝑅) |
2 | 1 | abvrcl 20091 |
. . . . . 6
⊢ (𝐹 ∈ 𝐴 → 𝑅 ∈ Ring) |
3 | | abvf.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑅) |
4 | | abvtri.p |
. . . . . . 7
⊢ + =
(+g‘𝑅) |
5 | | eqid 2738 |
. . . . . . 7
⊢
(.r‘𝑅) = (.r‘𝑅) |
6 | | eqid 2738 |
. . . . . . 7
⊢
(0g‘𝑅) = (0g‘𝑅) |
7 | 1, 3, 4, 5, 6 | isabv 20089 |
. . . . . 6
⊢ (𝑅 ∈ Ring → (𝐹 ∈ 𝐴 ↔ (𝐹:𝐵⟶(0[,)+∞) ∧ ∀𝑥 ∈ 𝐵 (((𝐹‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑅)) ∧ ∀𝑦 ∈ 𝐵 ((𝐹‘(𝑥(.r‘𝑅)𝑦)) = ((𝐹‘𝑥) · (𝐹‘𝑦)) ∧ (𝐹‘(𝑥 + 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦))))))) |
8 | 2, 7 | syl 17 |
. . . . 5
⊢ (𝐹 ∈ 𝐴 → (𝐹 ∈ 𝐴 ↔ (𝐹:𝐵⟶(0[,)+∞) ∧ ∀𝑥 ∈ 𝐵 (((𝐹‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑅)) ∧ ∀𝑦 ∈ 𝐵 ((𝐹‘(𝑥(.r‘𝑅)𝑦)) = ((𝐹‘𝑥) · (𝐹‘𝑦)) ∧ (𝐹‘(𝑥 + 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦))))))) |
9 | 8 | ibi 266 |
. . . 4
⊢ (𝐹 ∈ 𝐴 → (𝐹:𝐵⟶(0[,)+∞) ∧ ∀𝑥 ∈ 𝐵 (((𝐹‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑅)) ∧ ∀𝑦 ∈ 𝐵 ((𝐹‘(𝑥(.r‘𝑅)𝑦)) = ((𝐹‘𝑥) · (𝐹‘𝑦)) ∧ (𝐹‘(𝑥 + 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦)))))) |
10 | | simpr 485 |
. . . . . . 7
⊢ (((𝐹‘(𝑥(.r‘𝑅)𝑦)) = ((𝐹‘𝑥) · (𝐹‘𝑦)) ∧ (𝐹‘(𝑥 + 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦))) → (𝐹‘(𝑥 + 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦))) |
11 | 10 | ralimi 3087 |
. . . . . 6
⊢
(∀𝑦 ∈
𝐵 ((𝐹‘(𝑥(.r‘𝑅)𝑦)) = ((𝐹‘𝑥) · (𝐹‘𝑦)) ∧ (𝐹‘(𝑥 + 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦))) → ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦))) |
12 | 11 | adantl 482 |
. . . . 5
⊢ ((((𝐹‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑅)) ∧ ∀𝑦 ∈ 𝐵 ((𝐹‘(𝑥(.r‘𝑅)𝑦)) = ((𝐹‘𝑥) · (𝐹‘𝑦)) ∧ (𝐹‘(𝑥 + 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦)))) → ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦))) |
13 | 12 | ralimi 3087 |
. . . 4
⊢
(∀𝑥 ∈
𝐵 (((𝐹‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑅)) ∧ ∀𝑦 ∈ 𝐵 ((𝐹‘(𝑥(.r‘𝑅)𝑦)) = ((𝐹‘𝑥) · (𝐹‘𝑦)) ∧ (𝐹‘(𝑥 + 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦)))) → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦))) |
14 | 9, 13 | simpl2im 504 |
. . 3
⊢ (𝐹 ∈ 𝐴 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦))) |
15 | | fvoveq1 7290 |
. . . . 5
⊢ (𝑥 = 𝑋 → (𝐹‘(𝑥 + 𝑦)) = (𝐹‘(𝑋 + 𝑦))) |
16 | | fveq2 6766 |
. . . . . 6
⊢ (𝑥 = 𝑋 → (𝐹‘𝑥) = (𝐹‘𝑋)) |
17 | 16 | oveq1d 7282 |
. . . . 5
⊢ (𝑥 = 𝑋 → ((𝐹‘𝑥) + (𝐹‘𝑦)) = ((𝐹‘𝑋) + (𝐹‘𝑦))) |
18 | 15, 17 | breq12d 5086 |
. . . 4
⊢ (𝑥 = 𝑋 → ((𝐹‘(𝑥 + 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦)) ↔ (𝐹‘(𝑋 + 𝑦)) ≤ ((𝐹‘𝑋) + (𝐹‘𝑦)))) |
19 | | oveq2 7275 |
. . . . . 6
⊢ (𝑦 = 𝑌 → (𝑋 + 𝑦) = (𝑋 + 𝑌)) |
20 | 19 | fveq2d 6770 |
. . . . 5
⊢ (𝑦 = 𝑌 → (𝐹‘(𝑋 + 𝑦)) = (𝐹‘(𝑋 + 𝑌))) |
21 | | fveq2 6766 |
. . . . . 6
⊢ (𝑦 = 𝑌 → (𝐹‘𝑦) = (𝐹‘𝑌)) |
22 | 21 | oveq2d 7283 |
. . . . 5
⊢ (𝑦 = 𝑌 → ((𝐹‘𝑋) + (𝐹‘𝑦)) = ((𝐹‘𝑋) + (𝐹‘𝑌))) |
23 | 20, 22 | breq12d 5086 |
. . . 4
⊢ (𝑦 = 𝑌 → ((𝐹‘(𝑋 + 𝑦)) ≤ ((𝐹‘𝑋) + (𝐹‘𝑦)) ↔ (𝐹‘(𝑋 + 𝑌)) ≤ ((𝐹‘𝑋) + (𝐹‘𝑌)))) |
24 | 18, 23 | rspc2v 3569 |
. . 3
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦)) → (𝐹‘(𝑋 + 𝑌)) ≤ ((𝐹‘𝑋) + (𝐹‘𝑌)))) |
25 | 14, 24 | syl5com 31 |
. 2
⊢ (𝐹 ∈ 𝐴 → ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐹‘(𝑋 + 𝑌)) ≤ ((𝐹‘𝑋) + (𝐹‘𝑌)))) |
26 | 25 | 3impib 1115 |
1
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐹‘(𝑋 + 𝑌)) ≤ ((𝐹‘𝑋) + (𝐹‘𝑌))) |