| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | abvf.a | . . . . . . 7
⊢ 𝐴 = (AbsVal‘𝑅) | 
| 2 | 1 | abvrcl 20814 | . . . . . 6
⊢ (𝐹 ∈ 𝐴 → 𝑅 ∈ Ring) | 
| 3 |  | abvf.b | . . . . . . 7
⊢ 𝐵 = (Base‘𝑅) | 
| 4 |  | abvtri.p | . . . . . . 7
⊢  + =
(+g‘𝑅) | 
| 5 |  | eqid 2737 | . . . . . . 7
⊢
(.r‘𝑅) = (.r‘𝑅) | 
| 6 |  | eqid 2737 | . . . . . . 7
⊢
(0g‘𝑅) = (0g‘𝑅) | 
| 7 | 1, 3, 4, 5, 6 | isabv 20812 | . . . . . 6
⊢ (𝑅 ∈ Ring → (𝐹 ∈ 𝐴 ↔ (𝐹:𝐵⟶(0[,)+∞) ∧ ∀𝑥 ∈ 𝐵 (((𝐹‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑅)) ∧ ∀𝑦 ∈ 𝐵 ((𝐹‘(𝑥(.r‘𝑅)𝑦)) = ((𝐹‘𝑥) · (𝐹‘𝑦)) ∧ (𝐹‘(𝑥 + 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦))))))) | 
| 8 | 2, 7 | syl 17 | . . . . 5
⊢ (𝐹 ∈ 𝐴 → (𝐹 ∈ 𝐴 ↔ (𝐹:𝐵⟶(0[,)+∞) ∧ ∀𝑥 ∈ 𝐵 (((𝐹‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑅)) ∧ ∀𝑦 ∈ 𝐵 ((𝐹‘(𝑥(.r‘𝑅)𝑦)) = ((𝐹‘𝑥) · (𝐹‘𝑦)) ∧ (𝐹‘(𝑥 + 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦))))))) | 
| 9 | 8 | ibi 267 | . . . 4
⊢ (𝐹 ∈ 𝐴 → (𝐹:𝐵⟶(0[,)+∞) ∧ ∀𝑥 ∈ 𝐵 (((𝐹‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑅)) ∧ ∀𝑦 ∈ 𝐵 ((𝐹‘(𝑥(.r‘𝑅)𝑦)) = ((𝐹‘𝑥) · (𝐹‘𝑦)) ∧ (𝐹‘(𝑥 + 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦)))))) | 
| 10 |  | simpr 484 | . . . . . . 7
⊢ (((𝐹‘(𝑥(.r‘𝑅)𝑦)) = ((𝐹‘𝑥) · (𝐹‘𝑦)) ∧ (𝐹‘(𝑥 + 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦))) → (𝐹‘(𝑥 + 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦))) | 
| 11 | 10 | ralimi 3083 | . . . . . 6
⊢
(∀𝑦 ∈
𝐵 ((𝐹‘(𝑥(.r‘𝑅)𝑦)) = ((𝐹‘𝑥) · (𝐹‘𝑦)) ∧ (𝐹‘(𝑥 + 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦))) → ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦))) | 
| 12 | 11 | adantl 481 | . . . . 5
⊢ ((((𝐹‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑅)) ∧ ∀𝑦 ∈ 𝐵 ((𝐹‘(𝑥(.r‘𝑅)𝑦)) = ((𝐹‘𝑥) · (𝐹‘𝑦)) ∧ (𝐹‘(𝑥 + 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦)))) → ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦))) | 
| 13 | 12 | ralimi 3083 | . . . 4
⊢
(∀𝑥 ∈
𝐵 (((𝐹‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑅)) ∧ ∀𝑦 ∈ 𝐵 ((𝐹‘(𝑥(.r‘𝑅)𝑦)) = ((𝐹‘𝑥) · (𝐹‘𝑦)) ∧ (𝐹‘(𝑥 + 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦)))) → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦))) | 
| 14 | 9, 13 | simpl2im 503 | . . 3
⊢ (𝐹 ∈ 𝐴 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦))) | 
| 15 |  | fvoveq1 7454 | . . . . 5
⊢ (𝑥 = 𝑋 → (𝐹‘(𝑥 + 𝑦)) = (𝐹‘(𝑋 + 𝑦))) | 
| 16 |  | fveq2 6906 | . . . . . 6
⊢ (𝑥 = 𝑋 → (𝐹‘𝑥) = (𝐹‘𝑋)) | 
| 17 | 16 | oveq1d 7446 | . . . . 5
⊢ (𝑥 = 𝑋 → ((𝐹‘𝑥) + (𝐹‘𝑦)) = ((𝐹‘𝑋) + (𝐹‘𝑦))) | 
| 18 | 15, 17 | breq12d 5156 | . . . 4
⊢ (𝑥 = 𝑋 → ((𝐹‘(𝑥 + 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦)) ↔ (𝐹‘(𝑋 + 𝑦)) ≤ ((𝐹‘𝑋) + (𝐹‘𝑦)))) | 
| 19 |  | oveq2 7439 | . . . . . 6
⊢ (𝑦 = 𝑌 → (𝑋 + 𝑦) = (𝑋 + 𝑌)) | 
| 20 | 19 | fveq2d 6910 | . . . . 5
⊢ (𝑦 = 𝑌 → (𝐹‘(𝑋 + 𝑦)) = (𝐹‘(𝑋 + 𝑌))) | 
| 21 |  | fveq2 6906 | . . . . . 6
⊢ (𝑦 = 𝑌 → (𝐹‘𝑦) = (𝐹‘𝑌)) | 
| 22 | 21 | oveq2d 7447 | . . . . 5
⊢ (𝑦 = 𝑌 → ((𝐹‘𝑋) + (𝐹‘𝑦)) = ((𝐹‘𝑋) + (𝐹‘𝑌))) | 
| 23 | 20, 22 | breq12d 5156 | . . . 4
⊢ (𝑦 = 𝑌 → ((𝐹‘(𝑋 + 𝑦)) ≤ ((𝐹‘𝑋) + (𝐹‘𝑦)) ↔ (𝐹‘(𝑋 + 𝑌)) ≤ ((𝐹‘𝑋) + (𝐹‘𝑌)))) | 
| 24 | 18, 23 | rspc2v 3633 | . . 3
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦)) → (𝐹‘(𝑋 + 𝑌)) ≤ ((𝐹‘𝑋) + (𝐹‘𝑌)))) | 
| 25 | 14, 24 | syl5com 31 | . 2
⊢ (𝐹 ∈ 𝐴 → ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐹‘(𝑋 + 𝑌)) ≤ ((𝐹‘𝑋) + (𝐹‘𝑌)))) | 
| 26 | 25 | 3impib 1117 | 1
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐹‘(𝑋 + 𝑌)) ≤ ((𝐹‘𝑋) + (𝐹‘𝑌))) |