| Step | Hyp | Ref
| Expression |
| 1 | | nrgring 24684 |
. . . 4
⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ Ring) |
| 2 | | nrginvrcn.u |
. . . . 5
⊢ 𝑈 = (Unit‘𝑅) |
| 3 | | eqid 2737 |
. . . . 5
⊢
((mulGrp‘𝑅)
↾s 𝑈) =
((mulGrp‘𝑅)
↾s 𝑈) |
| 4 | 2, 3 | unitgrp 20383 |
. . . 4
⊢ (𝑅 ∈ Ring →
((mulGrp‘𝑅)
↾s 𝑈)
∈ Grp) |
| 5 | 2, 3 | unitgrpbas 20382 |
. . . . 5
⊢ 𝑈 =
(Base‘((mulGrp‘𝑅) ↾s 𝑈)) |
| 6 | | nrginvrcn.i |
. . . . . 6
⊢ 𝐼 = (invr‘𝑅) |
| 7 | 2, 3, 6 | invrfval 20389 |
. . . . 5
⊢ 𝐼 =
(invg‘((mulGrp‘𝑅) ↾s 𝑈)) |
| 8 | 5, 7 | grpinvf 19004 |
. . . 4
⊢
(((mulGrp‘𝑅)
↾s 𝑈)
∈ Grp → 𝐼:𝑈⟶𝑈) |
| 9 | 1, 4, 8 | 3syl 18 |
. . 3
⊢ (𝑅 ∈ NrmRing → 𝐼:𝑈⟶𝑈) |
| 10 | | 1rp 13038 |
. . . . . . . 8
⊢ 1 ∈
ℝ+ |
| 11 | 10 | ne0ii 4344 |
. . . . . . 7
⊢
ℝ+ ≠ ∅ |
| 12 | 1 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ NrmRing ∧ (𝑥 ∈ 𝑈 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑈) → 𝑅 ∈ Ring) |
| 13 | | nrginvrcn.x |
. . . . . . . . . . . . . . . 16
⊢ 𝑋 = (Base‘𝑅) |
| 14 | 13, 2 | unitss 20376 |
. . . . . . . . . . . . . . 15
⊢ 𝑈 ⊆ 𝑋 |
| 15 | | simplrl 777 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ NrmRing ∧ (𝑥 ∈ 𝑈 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑈) → 𝑥 ∈ 𝑈) |
| 16 | 14, 15 | sselid 3981 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ NrmRing ∧ (𝑥 ∈ 𝑈 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑈) → 𝑥 ∈ 𝑋) |
| 17 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ NrmRing ∧ (𝑥 ∈ 𝑈 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑈) → 𝑦 ∈ 𝑈) |
| 18 | 14, 17 | sselid 3981 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ NrmRing ∧ (𝑥 ∈ 𝑈 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑈) → 𝑦 ∈ 𝑋) |
| 19 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢
(1r‘𝑅) = (1r‘𝑅) |
| 20 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢
(0g‘𝑅) = (0g‘𝑅) |
| 21 | 13, 19, 20 | ring1eq0 20295 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((1r‘𝑅) = (0g‘𝑅) → 𝑥 = 𝑦)) |
| 22 | 12, 16, 18, 21 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ NrmRing ∧ (𝑥 ∈ 𝑈 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑈) → ((1r‘𝑅) = (0g‘𝑅) → 𝑥 = 𝑦)) |
| 23 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢ (𝐼‘𝑦) = (𝐼‘𝑦) |
| 24 | | nrgngp 24683 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ NrmGrp) |
| 25 | | ngpms 24613 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑅 ∈ NrmGrp → 𝑅 ∈ MetSp) |
| 26 | | msxms 24464 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑅 ∈ MetSp → 𝑅 ∈
∞MetSp) |
| 27 | 24, 25, 26 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑅 ∈ NrmRing → 𝑅 ∈
∞MetSp) |
| 28 | 27 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑅 ∈ NrmRing ∧ (𝑥 ∈ 𝑈 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑈) → 𝑅 ∈ ∞MetSp) |
| 29 | 9 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑅 ∈ NrmRing ∧ (𝑥 ∈ 𝑈 ∧ 𝑟 ∈ ℝ+)) → 𝐼:𝑈⟶𝑈) |
| 30 | 29 | ffvelcdmda 7104 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑅 ∈ NrmRing ∧ (𝑥 ∈ 𝑈 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑈) → (𝐼‘𝑦) ∈ 𝑈) |
| 31 | 14, 30 | sselid 3981 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑅 ∈ NrmRing ∧ (𝑥 ∈ 𝑈 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑈) → (𝐼‘𝑦) ∈ 𝑋) |
| 32 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢
(dist‘𝑅) =
(dist‘𝑅) |
| 33 | 13, 32 | xmseq0 24474 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ ∞MetSp ∧
(𝐼‘𝑦) ∈ 𝑋 ∧ (𝐼‘𝑦) ∈ 𝑋) → (((𝐼‘𝑦)(dist‘𝑅)(𝐼‘𝑦)) = 0 ↔ (𝐼‘𝑦) = (𝐼‘𝑦))) |
| 34 | 28, 31, 31, 33 | syl3anc 1373 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ NrmRing ∧ (𝑥 ∈ 𝑈 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑈) → (((𝐼‘𝑦)(dist‘𝑅)(𝐼‘𝑦)) = 0 ↔ (𝐼‘𝑦) = (𝐼‘𝑦))) |
| 35 | 23, 34 | mpbiri 258 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ NrmRing ∧ (𝑥 ∈ 𝑈 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑈) → ((𝐼‘𝑦)(dist‘𝑅)(𝐼‘𝑦)) = 0) |
| 36 | | simplrr 778 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ NrmRing ∧ (𝑥 ∈ 𝑈 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑈) → 𝑟 ∈ ℝ+) |
| 37 | 36 | rpgt0d 13080 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ NrmRing ∧ (𝑥 ∈ 𝑈 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑈) → 0 < 𝑟) |
| 38 | 35, 37 | eqbrtrd 5165 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ NrmRing ∧ (𝑥 ∈ 𝑈 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑈) → ((𝐼‘𝑦)(dist‘𝑅)(𝐼‘𝑦)) < 𝑟) |
| 39 | | fveq2 6906 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → (𝐼‘𝑥) = (𝐼‘𝑦)) |
| 40 | 39 | oveq1d 7446 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → ((𝐼‘𝑥)(dist‘𝑅)(𝐼‘𝑦)) = ((𝐼‘𝑦)(dist‘𝑅)(𝐼‘𝑦))) |
| 41 | 40 | breq1d 5153 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → (((𝐼‘𝑥)(dist‘𝑅)(𝐼‘𝑦)) < 𝑟 ↔ ((𝐼‘𝑦)(dist‘𝑅)(𝐼‘𝑦)) < 𝑟)) |
| 42 | 38, 41 | syl5ibrcom 247 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ NrmRing ∧ (𝑥 ∈ 𝑈 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑈) → (𝑥 = 𝑦 → ((𝐼‘𝑥)(dist‘𝑅)(𝐼‘𝑦)) < 𝑟)) |
| 43 | 22, 42 | syld 47 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ NrmRing ∧ (𝑥 ∈ 𝑈 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑈) → ((1r‘𝑅) = (0g‘𝑅) → ((𝐼‘𝑥)(dist‘𝑅)(𝐼‘𝑦)) < 𝑟)) |
| 44 | 43 | imp 406 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ NrmRing ∧ (𝑥 ∈ 𝑈 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑈) ∧ (1r‘𝑅) = (0g‘𝑅)) → ((𝐼‘𝑥)(dist‘𝑅)(𝐼‘𝑦)) < 𝑟) |
| 45 | 44 | an32s 652 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ NrmRing ∧ (𝑥 ∈ 𝑈 ∧ 𝑟 ∈ ℝ+)) ∧
(1r‘𝑅) =
(0g‘𝑅))
∧ 𝑦 ∈ 𝑈) → ((𝐼‘𝑥)(dist‘𝑅)(𝐼‘𝑦)) < 𝑟) |
| 46 | 45 | a1d 25 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ NrmRing ∧ (𝑥 ∈ 𝑈 ∧ 𝑟 ∈ ℝ+)) ∧
(1r‘𝑅) =
(0g‘𝑅))
∧ 𝑦 ∈ 𝑈) → ((𝑥(dist‘𝑅)𝑦) < 𝑠 → ((𝐼‘𝑥)(dist‘𝑅)(𝐼‘𝑦)) < 𝑟)) |
| 47 | 46 | ralrimiva 3146 |
. . . . . . . 8
⊢ (((𝑅 ∈ NrmRing ∧ (𝑥 ∈ 𝑈 ∧ 𝑟 ∈ ℝ+)) ∧
(1r‘𝑅) =
(0g‘𝑅))
→ ∀𝑦 ∈
𝑈 ((𝑥(dist‘𝑅)𝑦) < 𝑠 → ((𝐼‘𝑥)(dist‘𝑅)(𝐼‘𝑦)) < 𝑟)) |
| 48 | 47 | ralrimivw 3150 |
. . . . . . 7
⊢ (((𝑅 ∈ NrmRing ∧ (𝑥 ∈ 𝑈 ∧ 𝑟 ∈ ℝ+)) ∧
(1r‘𝑅) =
(0g‘𝑅))
→ ∀𝑠 ∈
ℝ+ ∀𝑦 ∈ 𝑈 ((𝑥(dist‘𝑅)𝑦) < 𝑠 → ((𝐼‘𝑥)(dist‘𝑅)(𝐼‘𝑦)) < 𝑟)) |
| 49 | | r19.2z 4495 |
. . . . . . 7
⊢
((ℝ+ ≠ ∅ ∧ ∀𝑠 ∈ ℝ+ ∀𝑦 ∈ 𝑈 ((𝑥(dist‘𝑅)𝑦) < 𝑠 → ((𝐼‘𝑥)(dist‘𝑅)(𝐼‘𝑦)) < 𝑟)) → ∃𝑠 ∈ ℝ+ ∀𝑦 ∈ 𝑈 ((𝑥(dist‘𝑅)𝑦) < 𝑠 → ((𝐼‘𝑥)(dist‘𝑅)(𝐼‘𝑦)) < 𝑟)) |
| 50 | 11, 48, 49 | sylancr 587 |
. . . . . 6
⊢ (((𝑅 ∈ NrmRing ∧ (𝑥 ∈ 𝑈 ∧ 𝑟 ∈ ℝ+)) ∧
(1r‘𝑅) =
(0g‘𝑅))
→ ∃𝑠 ∈
ℝ+ ∀𝑦 ∈ 𝑈 ((𝑥(dist‘𝑅)𝑦) < 𝑠 → ((𝐼‘𝑥)(dist‘𝑅)(𝐼‘𝑦)) < 𝑟)) |
| 51 | | eqid 2737 |
. . . . . . 7
⊢
(norm‘𝑅) =
(norm‘𝑅) |
| 52 | | simpll 767 |
. . . . . . 7
⊢ (((𝑅 ∈ NrmRing ∧ (𝑥 ∈ 𝑈 ∧ 𝑟 ∈ ℝ+)) ∧
(1r‘𝑅)
≠ (0g‘𝑅)) → 𝑅 ∈ NrmRing) |
| 53 | 1 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝑅 ∈ NrmRing ∧ (𝑥 ∈ 𝑈 ∧ 𝑟 ∈ ℝ+)) ∧
(1r‘𝑅)
≠ (0g‘𝑅)) → 𝑅 ∈ Ring) |
| 54 | | simpr 484 |
. . . . . . . 8
⊢ (((𝑅 ∈ NrmRing ∧ (𝑥 ∈ 𝑈 ∧ 𝑟 ∈ ℝ+)) ∧
(1r‘𝑅)
≠ (0g‘𝑅)) → (1r‘𝑅) ≠
(0g‘𝑅)) |
| 55 | 19, 20 | isnzr 20514 |
. . . . . . . 8
⊢ (𝑅 ∈ NzRing ↔ (𝑅 ∈ Ring ∧
(1r‘𝑅)
≠ (0g‘𝑅))) |
| 56 | 53, 54, 55 | sylanbrc 583 |
. . . . . . 7
⊢ (((𝑅 ∈ NrmRing ∧ (𝑥 ∈ 𝑈 ∧ 𝑟 ∈ ℝ+)) ∧
(1r‘𝑅)
≠ (0g‘𝑅)) → 𝑅 ∈ NzRing) |
| 57 | | simplrl 777 |
. . . . . . 7
⊢ (((𝑅 ∈ NrmRing ∧ (𝑥 ∈ 𝑈 ∧ 𝑟 ∈ ℝ+)) ∧
(1r‘𝑅)
≠ (0g‘𝑅)) → 𝑥 ∈ 𝑈) |
| 58 | | simplrr 778 |
. . . . . . 7
⊢ (((𝑅 ∈ NrmRing ∧ (𝑥 ∈ 𝑈 ∧ 𝑟 ∈ ℝ+)) ∧
(1r‘𝑅)
≠ (0g‘𝑅)) → 𝑟 ∈ ℝ+) |
| 59 | | eqid 2737 |
. . . . . . 7
⊢ (if(1
≤ (((norm‘𝑅)‘𝑥) · 𝑟), 1, (((norm‘𝑅)‘𝑥) · 𝑟)) · (((norm‘𝑅)‘𝑥) / 2)) = (if(1 ≤ (((norm‘𝑅)‘𝑥) · 𝑟), 1, (((norm‘𝑅)‘𝑥) · 𝑟)) · (((norm‘𝑅)‘𝑥) / 2)) |
| 60 | 13, 2, 6, 51, 32, 52, 56, 57, 58, 59 | nrginvrcnlem 24712 |
. . . . . 6
⊢ (((𝑅 ∈ NrmRing ∧ (𝑥 ∈ 𝑈 ∧ 𝑟 ∈ ℝ+)) ∧
(1r‘𝑅)
≠ (0g‘𝑅)) → ∃𝑠 ∈ ℝ+ ∀𝑦 ∈ 𝑈 ((𝑥(dist‘𝑅)𝑦) < 𝑠 → ((𝐼‘𝑥)(dist‘𝑅)(𝐼‘𝑦)) < 𝑟)) |
| 61 | 50, 60 | pm2.61dane 3029 |
. . . . 5
⊢ ((𝑅 ∈ NrmRing ∧ (𝑥 ∈ 𝑈 ∧ 𝑟 ∈ ℝ+)) →
∃𝑠 ∈
ℝ+ ∀𝑦 ∈ 𝑈 ((𝑥(dist‘𝑅)𝑦) < 𝑠 → ((𝐼‘𝑥)(dist‘𝑅)(𝐼‘𝑦)) < 𝑟)) |
| 62 | 15, 17 | ovresd 7600 |
. . . . . . . . 9
⊢ (((𝑅 ∈ NrmRing ∧ (𝑥 ∈ 𝑈 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑈) → (𝑥((dist‘𝑅) ↾ (𝑈 × 𝑈))𝑦) = (𝑥(dist‘𝑅)𝑦)) |
| 63 | 62 | breq1d 5153 |
. . . . . . . 8
⊢ (((𝑅 ∈ NrmRing ∧ (𝑥 ∈ 𝑈 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑈) → ((𝑥((dist‘𝑅) ↾ (𝑈 × 𝑈))𝑦) < 𝑠 ↔ (𝑥(dist‘𝑅)𝑦) < 𝑠)) |
| 64 | | simpl 482 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝑈 ∧ 𝑟 ∈ ℝ+) → 𝑥 ∈ 𝑈) |
| 65 | | ffvelcdm 7101 |
. . . . . . . . . . . 12
⊢ ((𝐼:𝑈⟶𝑈 ∧ 𝑥 ∈ 𝑈) → (𝐼‘𝑥) ∈ 𝑈) |
| 66 | 9, 64, 65 | syl2an 596 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ NrmRing ∧ (𝑥 ∈ 𝑈 ∧ 𝑟 ∈ ℝ+)) → (𝐼‘𝑥) ∈ 𝑈) |
| 67 | 66 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ NrmRing ∧ (𝑥 ∈ 𝑈 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑈) → (𝐼‘𝑥) ∈ 𝑈) |
| 68 | 67, 30 | ovresd 7600 |
. . . . . . . . 9
⊢ (((𝑅 ∈ NrmRing ∧ (𝑥 ∈ 𝑈 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑈) → ((𝐼‘𝑥)((dist‘𝑅) ↾ (𝑈 × 𝑈))(𝐼‘𝑦)) = ((𝐼‘𝑥)(dist‘𝑅)(𝐼‘𝑦))) |
| 69 | 68 | breq1d 5153 |
. . . . . . . 8
⊢ (((𝑅 ∈ NrmRing ∧ (𝑥 ∈ 𝑈 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑈) → (((𝐼‘𝑥)((dist‘𝑅) ↾ (𝑈 × 𝑈))(𝐼‘𝑦)) < 𝑟 ↔ ((𝐼‘𝑥)(dist‘𝑅)(𝐼‘𝑦)) < 𝑟)) |
| 70 | 63, 69 | imbi12d 344 |
. . . . . . 7
⊢ (((𝑅 ∈ NrmRing ∧ (𝑥 ∈ 𝑈 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑦 ∈ 𝑈) → (((𝑥((dist‘𝑅) ↾ (𝑈 × 𝑈))𝑦) < 𝑠 → ((𝐼‘𝑥)((dist‘𝑅) ↾ (𝑈 × 𝑈))(𝐼‘𝑦)) < 𝑟) ↔ ((𝑥(dist‘𝑅)𝑦) < 𝑠 → ((𝐼‘𝑥)(dist‘𝑅)(𝐼‘𝑦)) < 𝑟))) |
| 71 | 70 | ralbidva 3176 |
. . . . . 6
⊢ ((𝑅 ∈ NrmRing ∧ (𝑥 ∈ 𝑈 ∧ 𝑟 ∈ ℝ+)) →
(∀𝑦 ∈ 𝑈 ((𝑥((dist‘𝑅) ↾ (𝑈 × 𝑈))𝑦) < 𝑠 → ((𝐼‘𝑥)((dist‘𝑅) ↾ (𝑈 × 𝑈))(𝐼‘𝑦)) < 𝑟) ↔ ∀𝑦 ∈ 𝑈 ((𝑥(dist‘𝑅)𝑦) < 𝑠 → ((𝐼‘𝑥)(dist‘𝑅)(𝐼‘𝑦)) < 𝑟))) |
| 72 | 71 | rexbidv 3179 |
. . . . 5
⊢ ((𝑅 ∈ NrmRing ∧ (𝑥 ∈ 𝑈 ∧ 𝑟 ∈ ℝ+)) →
(∃𝑠 ∈
ℝ+ ∀𝑦 ∈ 𝑈 ((𝑥((dist‘𝑅) ↾ (𝑈 × 𝑈))𝑦) < 𝑠 → ((𝐼‘𝑥)((dist‘𝑅) ↾ (𝑈 × 𝑈))(𝐼‘𝑦)) < 𝑟) ↔ ∃𝑠 ∈ ℝ+ ∀𝑦 ∈ 𝑈 ((𝑥(dist‘𝑅)𝑦) < 𝑠 → ((𝐼‘𝑥)(dist‘𝑅)(𝐼‘𝑦)) < 𝑟))) |
| 73 | 61, 72 | mpbird 257 |
. . . 4
⊢ ((𝑅 ∈ NrmRing ∧ (𝑥 ∈ 𝑈 ∧ 𝑟 ∈ ℝ+)) →
∃𝑠 ∈
ℝ+ ∀𝑦 ∈ 𝑈 ((𝑥((dist‘𝑅) ↾ (𝑈 × 𝑈))𝑦) < 𝑠 → ((𝐼‘𝑥)((dist‘𝑅) ↾ (𝑈 × 𝑈))(𝐼‘𝑦)) < 𝑟)) |
| 74 | 73 | ralrimivva 3202 |
. . 3
⊢ (𝑅 ∈ NrmRing →
∀𝑥 ∈ 𝑈 ∀𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+
∀𝑦 ∈ 𝑈 ((𝑥((dist‘𝑅) ↾ (𝑈 × 𝑈))𝑦) < 𝑠 → ((𝐼‘𝑥)((dist‘𝑅) ↾ (𝑈 × 𝑈))(𝐼‘𝑦)) < 𝑟)) |
| 75 | | xpss12 5700 |
. . . . . . 7
⊢ ((𝑈 ⊆ 𝑋 ∧ 𝑈 ⊆ 𝑋) → (𝑈 × 𝑈) ⊆ (𝑋 × 𝑋)) |
| 76 | 14, 14, 75 | mp2an 692 |
. . . . . 6
⊢ (𝑈 × 𝑈) ⊆ (𝑋 × 𝑋) |
| 77 | | resabs1 6024 |
. . . . . 6
⊢ ((𝑈 × 𝑈) ⊆ (𝑋 × 𝑋) → (((dist‘𝑅) ↾ (𝑋 × 𝑋)) ↾ (𝑈 × 𝑈)) = ((dist‘𝑅) ↾ (𝑈 × 𝑈))) |
| 78 | 76, 77 | ax-mp 5 |
. . . . 5
⊢
(((dist‘𝑅)
↾ (𝑋 × 𝑋)) ↾ (𝑈 × 𝑈)) = ((dist‘𝑅) ↾ (𝑈 × 𝑈)) |
| 79 | | eqid 2737 |
. . . . . . . 8
⊢
((dist‘𝑅)
↾ (𝑋 × 𝑋)) = ((dist‘𝑅) ↾ (𝑋 × 𝑋)) |
| 80 | 13, 79 | xmsxmet 24466 |
. . . . . . 7
⊢ (𝑅 ∈ ∞MetSp →
((dist‘𝑅) ↾
(𝑋 × 𝑋)) ∈
(∞Met‘𝑋)) |
| 81 | 24, 25, 26, 80 | 4syl 19 |
. . . . . 6
⊢ (𝑅 ∈ NrmRing →
((dist‘𝑅) ↾
(𝑋 × 𝑋)) ∈
(∞Met‘𝑋)) |
| 82 | | xmetres2 24371 |
. . . . . 6
⊢
((((dist‘𝑅)
↾ (𝑋 × 𝑋)) ∈
(∞Met‘𝑋) ∧
𝑈 ⊆ 𝑋) → (((dist‘𝑅) ↾ (𝑋 × 𝑋)) ↾ (𝑈 × 𝑈)) ∈ (∞Met‘𝑈)) |
| 83 | 81, 14, 82 | sylancl 586 |
. . . . 5
⊢ (𝑅 ∈ NrmRing →
(((dist‘𝑅) ↾
(𝑋 × 𝑋)) ↾ (𝑈 × 𝑈)) ∈ (∞Met‘𝑈)) |
| 84 | 78, 83 | eqeltrrid 2846 |
. . . 4
⊢ (𝑅 ∈ NrmRing →
((dist‘𝑅) ↾
(𝑈 × 𝑈)) ∈
(∞Met‘𝑈)) |
| 85 | | eqid 2737 |
. . . . 5
⊢
(MetOpen‘((dist‘𝑅) ↾ (𝑈 × 𝑈))) = (MetOpen‘((dist‘𝑅) ↾ (𝑈 × 𝑈))) |
| 86 | 85, 85 | metcn 24556 |
. . . 4
⊢
((((dist‘𝑅)
↾ (𝑈 × 𝑈)) ∈
(∞Met‘𝑈) ∧
((dist‘𝑅) ↾
(𝑈 × 𝑈)) ∈
(∞Met‘𝑈))
→ (𝐼 ∈
((MetOpen‘((dist‘𝑅) ↾ (𝑈 × 𝑈))) Cn (MetOpen‘((dist‘𝑅) ↾ (𝑈 × 𝑈)))) ↔ (𝐼:𝑈⟶𝑈 ∧ ∀𝑥 ∈ 𝑈 ∀𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+
∀𝑦 ∈ 𝑈 ((𝑥((dist‘𝑅) ↾ (𝑈 × 𝑈))𝑦) < 𝑠 → ((𝐼‘𝑥)((dist‘𝑅) ↾ (𝑈 × 𝑈))(𝐼‘𝑦)) < 𝑟)))) |
| 87 | 84, 84, 86 | syl2anc 584 |
. . 3
⊢ (𝑅 ∈ NrmRing → (𝐼 ∈
((MetOpen‘((dist‘𝑅) ↾ (𝑈 × 𝑈))) Cn (MetOpen‘((dist‘𝑅) ↾ (𝑈 × 𝑈)))) ↔ (𝐼:𝑈⟶𝑈 ∧ ∀𝑥 ∈ 𝑈 ∀𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+
∀𝑦 ∈ 𝑈 ((𝑥((dist‘𝑅) ↾ (𝑈 × 𝑈))𝑦) < 𝑠 → ((𝐼‘𝑥)((dist‘𝑅) ↾ (𝑈 × 𝑈))(𝐼‘𝑦)) < 𝑟)))) |
| 88 | 9, 74, 87 | mpbir2and 713 |
. 2
⊢ (𝑅 ∈ NrmRing → 𝐼 ∈
((MetOpen‘((dist‘𝑅) ↾ (𝑈 × 𝑈))) Cn (MetOpen‘((dist‘𝑅) ↾ (𝑈 × 𝑈))))) |
| 89 | | nrginvrcn.j |
. . . . . . 7
⊢ 𝐽 = (TopOpen‘𝑅) |
| 90 | 89, 13, 79 | mstopn 24462 |
. . . . . 6
⊢ (𝑅 ∈ MetSp → 𝐽 =
(MetOpen‘((dist‘𝑅) ↾ (𝑋 × 𝑋)))) |
| 91 | 24, 25, 90 | 3syl 18 |
. . . . 5
⊢ (𝑅 ∈ NrmRing → 𝐽 =
(MetOpen‘((dist‘𝑅) ↾ (𝑋 × 𝑋)))) |
| 92 | 91 | oveq1d 7446 |
. . . 4
⊢ (𝑅 ∈ NrmRing → (𝐽 ↾t 𝑈) =
((MetOpen‘((dist‘𝑅) ↾ (𝑋 × 𝑋))) ↾t 𝑈)) |
| 93 | 78 | eqcomi 2746 |
. . . . . 6
⊢
((dist‘𝑅)
↾ (𝑈 × 𝑈)) = (((dist‘𝑅) ↾ (𝑋 × 𝑋)) ↾ (𝑈 × 𝑈)) |
| 94 | | eqid 2737 |
. . . . . 6
⊢
(MetOpen‘((dist‘𝑅) ↾ (𝑋 × 𝑋))) = (MetOpen‘((dist‘𝑅) ↾ (𝑋 × 𝑋))) |
| 95 | 93, 94, 85 | metrest 24537 |
. . . . 5
⊢
((((dist‘𝑅)
↾ (𝑋 × 𝑋)) ∈
(∞Met‘𝑋) ∧
𝑈 ⊆ 𝑋) → ((MetOpen‘((dist‘𝑅) ↾ (𝑋 × 𝑋))) ↾t 𝑈) = (MetOpen‘((dist‘𝑅) ↾ (𝑈 × 𝑈)))) |
| 96 | 81, 14, 95 | sylancl 586 |
. . . 4
⊢ (𝑅 ∈ NrmRing →
((MetOpen‘((dist‘𝑅) ↾ (𝑋 × 𝑋))) ↾t 𝑈) = (MetOpen‘((dist‘𝑅) ↾ (𝑈 × 𝑈)))) |
| 97 | 92, 96 | eqtrd 2777 |
. . 3
⊢ (𝑅 ∈ NrmRing → (𝐽 ↾t 𝑈) =
(MetOpen‘((dist‘𝑅) ↾ (𝑈 × 𝑈)))) |
| 98 | 97, 97 | oveq12d 7449 |
. 2
⊢ (𝑅 ∈ NrmRing → ((𝐽 ↾t 𝑈) Cn (𝐽 ↾t 𝑈)) = ((MetOpen‘((dist‘𝑅) ↾ (𝑈 × 𝑈))) Cn (MetOpen‘((dist‘𝑅) ↾ (𝑈 × 𝑈))))) |
| 99 | 88, 98 | eleqtrrd 2844 |
1
⊢ (𝑅 ∈ NrmRing → 𝐼 ∈ ((𝐽 ↾t 𝑈) Cn (𝐽 ↾t 𝑈))) |