| Step | Hyp | Ref
| Expression |
| 1 | | abvres.b |
. . 3
⊢ 𝐵 = (AbsVal‘𝑆) |
| 2 | 1 | a1i 11 |
. 2
⊢ ((𝐹 ∈ 𝐴 ∧ 𝐶 ∈ (SubRing‘𝑅)) → 𝐵 = (AbsVal‘𝑆)) |
| 3 | | abvres.s |
. . . 4
⊢ 𝑆 = (𝑅 ↾s 𝐶) |
| 4 | 3 | subrgbas 20581 |
. . 3
⊢ (𝐶 ∈ (SubRing‘𝑅) → 𝐶 = (Base‘𝑆)) |
| 5 | 4 | adantl 481 |
. 2
⊢ ((𝐹 ∈ 𝐴 ∧ 𝐶 ∈ (SubRing‘𝑅)) → 𝐶 = (Base‘𝑆)) |
| 6 | | eqid 2737 |
. . . 4
⊢
(+g‘𝑅) = (+g‘𝑅) |
| 7 | 3, 6 | ressplusg 17334 |
. . 3
⊢ (𝐶 ∈ (SubRing‘𝑅) →
(+g‘𝑅) =
(+g‘𝑆)) |
| 8 | 7 | adantl 481 |
. 2
⊢ ((𝐹 ∈ 𝐴 ∧ 𝐶 ∈ (SubRing‘𝑅)) → (+g‘𝑅) = (+g‘𝑆)) |
| 9 | | eqid 2737 |
. . . 4
⊢
(.r‘𝑅) = (.r‘𝑅) |
| 10 | 3, 9 | ressmulr 17351 |
. . 3
⊢ (𝐶 ∈ (SubRing‘𝑅) →
(.r‘𝑅) =
(.r‘𝑆)) |
| 11 | 10 | adantl 481 |
. 2
⊢ ((𝐹 ∈ 𝐴 ∧ 𝐶 ∈ (SubRing‘𝑅)) → (.r‘𝑅) = (.r‘𝑆)) |
| 12 | | subrgsubg 20577 |
. . . 4
⊢ (𝐶 ∈ (SubRing‘𝑅) → 𝐶 ∈ (SubGrp‘𝑅)) |
| 13 | 12 | adantl 481 |
. . 3
⊢ ((𝐹 ∈ 𝐴 ∧ 𝐶 ∈ (SubRing‘𝑅)) → 𝐶 ∈ (SubGrp‘𝑅)) |
| 14 | | eqid 2737 |
. . . 4
⊢
(0g‘𝑅) = (0g‘𝑅) |
| 15 | 3, 14 | subg0 19150 |
. . 3
⊢ (𝐶 ∈ (SubGrp‘𝑅) →
(0g‘𝑅) =
(0g‘𝑆)) |
| 16 | 13, 15 | syl 17 |
. 2
⊢ ((𝐹 ∈ 𝐴 ∧ 𝐶 ∈ (SubRing‘𝑅)) → (0g‘𝑅) = (0g‘𝑆)) |
| 17 | 3 | subrgring 20574 |
. . 3
⊢ (𝐶 ∈ (SubRing‘𝑅) → 𝑆 ∈ Ring) |
| 18 | 17 | adantl 481 |
. 2
⊢ ((𝐹 ∈ 𝐴 ∧ 𝐶 ∈ (SubRing‘𝑅)) → 𝑆 ∈ Ring) |
| 19 | | abvres.a |
. . . 4
⊢ 𝐴 = (AbsVal‘𝑅) |
| 20 | | eqid 2737 |
. . . 4
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 21 | 19, 20 | abvf 20816 |
. . 3
⊢ (𝐹 ∈ 𝐴 → 𝐹:(Base‘𝑅)⟶ℝ) |
| 22 | 20 | subrgss 20572 |
. . 3
⊢ (𝐶 ∈ (SubRing‘𝑅) → 𝐶 ⊆ (Base‘𝑅)) |
| 23 | | fssres 6774 |
. . 3
⊢ ((𝐹:(Base‘𝑅)⟶ℝ ∧ 𝐶 ⊆ (Base‘𝑅)) → (𝐹 ↾ 𝐶):𝐶⟶ℝ) |
| 24 | 21, 22, 23 | syl2an 596 |
. 2
⊢ ((𝐹 ∈ 𝐴 ∧ 𝐶 ∈ (SubRing‘𝑅)) → (𝐹 ↾ 𝐶):𝐶⟶ℝ) |
| 25 | 14 | subg0cl 19152 |
. . . 4
⊢ (𝐶 ∈ (SubGrp‘𝑅) →
(0g‘𝑅)
∈ 𝐶) |
| 26 | | fvres 6925 |
. . . 4
⊢
((0g‘𝑅) ∈ 𝐶 → ((𝐹 ↾ 𝐶)‘(0g‘𝑅)) = (𝐹‘(0g‘𝑅))) |
| 27 | 13, 25, 26 | 3syl 18 |
. . 3
⊢ ((𝐹 ∈ 𝐴 ∧ 𝐶 ∈ (SubRing‘𝑅)) → ((𝐹 ↾ 𝐶)‘(0g‘𝑅)) = (𝐹‘(0g‘𝑅))) |
| 28 | 19, 14 | abv0 20824 |
. . . 4
⊢ (𝐹 ∈ 𝐴 → (𝐹‘(0g‘𝑅)) = 0) |
| 29 | 28 | adantr 480 |
. . 3
⊢ ((𝐹 ∈ 𝐴 ∧ 𝐶 ∈ (SubRing‘𝑅)) → (𝐹‘(0g‘𝑅)) = 0) |
| 30 | 27, 29 | eqtrd 2777 |
. 2
⊢ ((𝐹 ∈ 𝐴 ∧ 𝐶 ∈ (SubRing‘𝑅)) → ((𝐹 ↾ 𝐶)‘(0g‘𝑅)) = 0) |
| 31 | | simp1l 1198 |
. . . 4
⊢ (((𝐹 ∈ 𝐴 ∧ 𝐶 ∈ (SubRing‘𝑅)) ∧ 𝑥 ∈ 𝐶 ∧ 𝑥 ≠ (0g‘𝑅)) → 𝐹 ∈ 𝐴) |
| 32 | 22 | adantl 481 |
. . . . . 6
⊢ ((𝐹 ∈ 𝐴 ∧ 𝐶 ∈ (SubRing‘𝑅)) → 𝐶 ⊆ (Base‘𝑅)) |
| 33 | 32 | sselda 3983 |
. . . . 5
⊢ (((𝐹 ∈ 𝐴 ∧ 𝐶 ∈ (SubRing‘𝑅)) ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ (Base‘𝑅)) |
| 34 | 33 | 3adant3 1133 |
. . . 4
⊢ (((𝐹 ∈ 𝐴 ∧ 𝐶 ∈ (SubRing‘𝑅)) ∧ 𝑥 ∈ 𝐶 ∧ 𝑥 ≠ (0g‘𝑅)) → 𝑥 ∈ (Base‘𝑅)) |
| 35 | | simp3 1139 |
. . . 4
⊢ (((𝐹 ∈ 𝐴 ∧ 𝐶 ∈ (SubRing‘𝑅)) ∧ 𝑥 ∈ 𝐶 ∧ 𝑥 ≠ (0g‘𝑅)) → 𝑥 ≠ (0g‘𝑅)) |
| 36 | 19, 20, 14 | abvgt0 20821 |
. . . 4
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑥 ≠ (0g‘𝑅)) → 0 < (𝐹‘𝑥)) |
| 37 | 31, 34, 35, 36 | syl3anc 1373 |
. . 3
⊢ (((𝐹 ∈ 𝐴 ∧ 𝐶 ∈ (SubRing‘𝑅)) ∧ 𝑥 ∈ 𝐶 ∧ 𝑥 ≠ (0g‘𝑅)) → 0 < (𝐹‘𝑥)) |
| 38 | | fvres 6925 |
. . . 4
⊢ (𝑥 ∈ 𝐶 → ((𝐹 ↾ 𝐶)‘𝑥) = (𝐹‘𝑥)) |
| 39 | 38 | 3ad2ant2 1135 |
. . 3
⊢ (((𝐹 ∈ 𝐴 ∧ 𝐶 ∈ (SubRing‘𝑅)) ∧ 𝑥 ∈ 𝐶 ∧ 𝑥 ≠ (0g‘𝑅)) → ((𝐹 ↾ 𝐶)‘𝑥) = (𝐹‘𝑥)) |
| 40 | 37, 39 | breqtrrd 5171 |
. 2
⊢ (((𝐹 ∈ 𝐴 ∧ 𝐶 ∈ (SubRing‘𝑅)) ∧ 𝑥 ∈ 𝐶 ∧ 𝑥 ≠ (0g‘𝑅)) → 0 < ((𝐹 ↾ 𝐶)‘𝑥)) |
| 41 | | simp1l 1198 |
. . . 4
⊢ (((𝐹 ∈ 𝐴 ∧ 𝐶 ∈ (SubRing‘𝑅)) ∧ (𝑥 ∈ 𝐶 ∧ 𝑥 ≠ (0g‘𝑅)) ∧ (𝑦 ∈ 𝐶 ∧ 𝑦 ≠ (0g‘𝑅))) → 𝐹 ∈ 𝐴) |
| 42 | | simp1r 1199 |
. . . . . 6
⊢ (((𝐹 ∈ 𝐴 ∧ 𝐶 ∈ (SubRing‘𝑅)) ∧ (𝑥 ∈ 𝐶 ∧ 𝑥 ≠ (0g‘𝑅)) ∧ (𝑦 ∈ 𝐶 ∧ 𝑦 ≠ (0g‘𝑅))) → 𝐶 ∈ (SubRing‘𝑅)) |
| 43 | 42, 22 | syl 17 |
. . . . 5
⊢ (((𝐹 ∈ 𝐴 ∧ 𝐶 ∈ (SubRing‘𝑅)) ∧ (𝑥 ∈ 𝐶 ∧ 𝑥 ≠ (0g‘𝑅)) ∧ (𝑦 ∈ 𝐶 ∧ 𝑦 ≠ (0g‘𝑅))) → 𝐶 ⊆ (Base‘𝑅)) |
| 44 | | simp2l 1200 |
. . . . 5
⊢ (((𝐹 ∈ 𝐴 ∧ 𝐶 ∈ (SubRing‘𝑅)) ∧ (𝑥 ∈ 𝐶 ∧ 𝑥 ≠ (0g‘𝑅)) ∧ (𝑦 ∈ 𝐶 ∧ 𝑦 ≠ (0g‘𝑅))) → 𝑥 ∈ 𝐶) |
| 45 | 43, 44 | sseldd 3984 |
. . . 4
⊢ (((𝐹 ∈ 𝐴 ∧ 𝐶 ∈ (SubRing‘𝑅)) ∧ (𝑥 ∈ 𝐶 ∧ 𝑥 ≠ (0g‘𝑅)) ∧ (𝑦 ∈ 𝐶 ∧ 𝑦 ≠ (0g‘𝑅))) → 𝑥 ∈ (Base‘𝑅)) |
| 46 | | simp3l 1202 |
. . . . 5
⊢ (((𝐹 ∈ 𝐴 ∧ 𝐶 ∈ (SubRing‘𝑅)) ∧ (𝑥 ∈ 𝐶 ∧ 𝑥 ≠ (0g‘𝑅)) ∧ (𝑦 ∈ 𝐶 ∧ 𝑦 ≠ (0g‘𝑅))) → 𝑦 ∈ 𝐶) |
| 47 | 43, 46 | sseldd 3984 |
. . . 4
⊢ (((𝐹 ∈ 𝐴 ∧ 𝐶 ∈ (SubRing‘𝑅)) ∧ (𝑥 ∈ 𝐶 ∧ 𝑥 ≠ (0g‘𝑅)) ∧ (𝑦 ∈ 𝐶 ∧ 𝑦 ≠ (0g‘𝑅))) → 𝑦 ∈ (Base‘𝑅)) |
| 48 | 19, 20, 9 | abvmul 20822 |
. . . 4
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → (𝐹‘(𝑥(.r‘𝑅)𝑦)) = ((𝐹‘𝑥) · (𝐹‘𝑦))) |
| 49 | 41, 45, 47, 48 | syl3anc 1373 |
. . 3
⊢ (((𝐹 ∈ 𝐴 ∧ 𝐶 ∈ (SubRing‘𝑅)) ∧ (𝑥 ∈ 𝐶 ∧ 𝑥 ≠ (0g‘𝑅)) ∧ (𝑦 ∈ 𝐶 ∧ 𝑦 ≠ (0g‘𝑅))) → (𝐹‘(𝑥(.r‘𝑅)𝑦)) = ((𝐹‘𝑥) · (𝐹‘𝑦))) |
| 50 | 9 | subrgmcl 20584 |
. . . . 5
⊢ ((𝐶 ∈ (SubRing‘𝑅) ∧ 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶) → (𝑥(.r‘𝑅)𝑦) ∈ 𝐶) |
| 51 | 42, 44, 46, 50 | syl3anc 1373 |
. . . 4
⊢ (((𝐹 ∈ 𝐴 ∧ 𝐶 ∈ (SubRing‘𝑅)) ∧ (𝑥 ∈ 𝐶 ∧ 𝑥 ≠ (0g‘𝑅)) ∧ (𝑦 ∈ 𝐶 ∧ 𝑦 ≠ (0g‘𝑅))) → (𝑥(.r‘𝑅)𝑦) ∈ 𝐶) |
| 52 | 51 | fvresd 6926 |
. . 3
⊢ (((𝐹 ∈ 𝐴 ∧ 𝐶 ∈ (SubRing‘𝑅)) ∧ (𝑥 ∈ 𝐶 ∧ 𝑥 ≠ (0g‘𝑅)) ∧ (𝑦 ∈ 𝐶 ∧ 𝑦 ≠ (0g‘𝑅))) → ((𝐹 ↾ 𝐶)‘(𝑥(.r‘𝑅)𝑦)) = (𝐹‘(𝑥(.r‘𝑅)𝑦))) |
| 53 | 44 | fvresd 6926 |
. . . 4
⊢ (((𝐹 ∈ 𝐴 ∧ 𝐶 ∈ (SubRing‘𝑅)) ∧ (𝑥 ∈ 𝐶 ∧ 𝑥 ≠ (0g‘𝑅)) ∧ (𝑦 ∈ 𝐶 ∧ 𝑦 ≠ (0g‘𝑅))) → ((𝐹 ↾ 𝐶)‘𝑥) = (𝐹‘𝑥)) |
| 54 | 46 | fvresd 6926 |
. . . 4
⊢ (((𝐹 ∈ 𝐴 ∧ 𝐶 ∈ (SubRing‘𝑅)) ∧ (𝑥 ∈ 𝐶 ∧ 𝑥 ≠ (0g‘𝑅)) ∧ (𝑦 ∈ 𝐶 ∧ 𝑦 ≠ (0g‘𝑅))) → ((𝐹 ↾ 𝐶)‘𝑦) = (𝐹‘𝑦)) |
| 55 | 53, 54 | oveq12d 7449 |
. . 3
⊢ (((𝐹 ∈ 𝐴 ∧ 𝐶 ∈ (SubRing‘𝑅)) ∧ (𝑥 ∈ 𝐶 ∧ 𝑥 ≠ (0g‘𝑅)) ∧ (𝑦 ∈ 𝐶 ∧ 𝑦 ≠ (0g‘𝑅))) → (((𝐹 ↾ 𝐶)‘𝑥) · ((𝐹 ↾ 𝐶)‘𝑦)) = ((𝐹‘𝑥) · (𝐹‘𝑦))) |
| 56 | 49, 52, 55 | 3eqtr4d 2787 |
. 2
⊢ (((𝐹 ∈ 𝐴 ∧ 𝐶 ∈ (SubRing‘𝑅)) ∧ (𝑥 ∈ 𝐶 ∧ 𝑥 ≠ (0g‘𝑅)) ∧ (𝑦 ∈ 𝐶 ∧ 𝑦 ≠ (0g‘𝑅))) → ((𝐹 ↾ 𝐶)‘(𝑥(.r‘𝑅)𝑦)) = (((𝐹 ↾ 𝐶)‘𝑥) · ((𝐹 ↾ 𝐶)‘𝑦))) |
| 57 | 19, 20, 6 | abvtri 20823 |
. . . 4
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → (𝐹‘(𝑥(+g‘𝑅)𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦))) |
| 58 | 41, 45, 47, 57 | syl3anc 1373 |
. . 3
⊢ (((𝐹 ∈ 𝐴 ∧ 𝐶 ∈ (SubRing‘𝑅)) ∧ (𝑥 ∈ 𝐶 ∧ 𝑥 ≠ (0g‘𝑅)) ∧ (𝑦 ∈ 𝐶 ∧ 𝑦 ≠ (0g‘𝑅))) → (𝐹‘(𝑥(+g‘𝑅)𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦))) |
| 59 | 6 | subrgacl 20583 |
. . . . 5
⊢ ((𝐶 ∈ (SubRing‘𝑅) ∧ 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶) → (𝑥(+g‘𝑅)𝑦) ∈ 𝐶) |
| 60 | 42, 44, 46, 59 | syl3anc 1373 |
. . . 4
⊢ (((𝐹 ∈ 𝐴 ∧ 𝐶 ∈ (SubRing‘𝑅)) ∧ (𝑥 ∈ 𝐶 ∧ 𝑥 ≠ (0g‘𝑅)) ∧ (𝑦 ∈ 𝐶 ∧ 𝑦 ≠ (0g‘𝑅))) → (𝑥(+g‘𝑅)𝑦) ∈ 𝐶) |
| 61 | 60 | fvresd 6926 |
. . 3
⊢ (((𝐹 ∈ 𝐴 ∧ 𝐶 ∈ (SubRing‘𝑅)) ∧ (𝑥 ∈ 𝐶 ∧ 𝑥 ≠ (0g‘𝑅)) ∧ (𝑦 ∈ 𝐶 ∧ 𝑦 ≠ (0g‘𝑅))) → ((𝐹 ↾ 𝐶)‘(𝑥(+g‘𝑅)𝑦)) = (𝐹‘(𝑥(+g‘𝑅)𝑦))) |
| 62 | 53, 54 | oveq12d 7449 |
. . 3
⊢ (((𝐹 ∈ 𝐴 ∧ 𝐶 ∈ (SubRing‘𝑅)) ∧ (𝑥 ∈ 𝐶 ∧ 𝑥 ≠ (0g‘𝑅)) ∧ (𝑦 ∈ 𝐶 ∧ 𝑦 ≠ (0g‘𝑅))) → (((𝐹 ↾ 𝐶)‘𝑥) + ((𝐹 ↾ 𝐶)‘𝑦)) = ((𝐹‘𝑥) + (𝐹‘𝑦))) |
| 63 | 58, 61, 62 | 3brtr4d 5175 |
. 2
⊢ (((𝐹 ∈ 𝐴 ∧ 𝐶 ∈ (SubRing‘𝑅)) ∧ (𝑥 ∈ 𝐶 ∧ 𝑥 ≠ (0g‘𝑅)) ∧ (𝑦 ∈ 𝐶 ∧ 𝑦 ≠ (0g‘𝑅))) → ((𝐹 ↾ 𝐶)‘(𝑥(+g‘𝑅)𝑦)) ≤ (((𝐹 ↾ 𝐶)‘𝑥) + ((𝐹 ↾ 𝐶)‘𝑦))) |
| 64 | 2, 5, 8, 11, 16, 18, 24, 30, 40, 56, 63 | isabvd 20813 |
1
⊢ ((𝐹 ∈ 𝐴 ∧ 𝐶 ∈ (SubRing‘𝑅)) → (𝐹 ↾ 𝐶) ∈ 𝐵) |