Step | Hyp | Ref
| Expression |
1 | | elin 3903 |
. . 3
⊢ (𝑅 ∈ (NrmRing ∩ DivRing)
↔ (𝑅 ∈ NrmRing
∧ 𝑅 ∈
DivRing)) |
2 | 1 | anbi1i 624 |
. 2
⊢ ((𝑅 ∈ (NrmRing ∩ DivRing)
∧ ((𝑍 ∈ NrmMod
∧ (chr‘𝑅) = 0)
∧ (𝑅 ∈ CUnifSp
∧ (UnifSt‘𝑅) =
(metUnif‘𝐷)))) ↔
((𝑅 ∈ NrmRing ∧
𝑅 ∈ DivRing) ∧
((𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
(𝑅 ∈ CUnifSp ∧
(UnifSt‘𝑅) =
(metUnif‘𝐷))))) |
3 | | fveq2 6774 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → (ℤMod‘𝑟) = (ℤMod‘𝑅)) |
4 | 3 | eleq1d 2823 |
. . . . . 6
⊢ (𝑟 = 𝑅 → ((ℤMod‘𝑟) ∈ NrmMod ↔
(ℤMod‘𝑅) ∈
NrmMod)) |
5 | | isrrext.z |
. . . . . . 7
⊢ 𝑍 = (ℤMod‘𝑅) |
6 | 5 | eleq1i 2829 |
. . . . . 6
⊢ (𝑍 ∈ NrmMod ↔
(ℤMod‘𝑅) ∈
NrmMod) |
7 | 4, 6 | bitr4di 289 |
. . . . 5
⊢ (𝑟 = 𝑅 → ((ℤMod‘𝑟) ∈ NrmMod ↔ 𝑍 ∈
NrmMod)) |
8 | | fveqeq2 6783 |
. . . . 5
⊢ (𝑟 = 𝑅 → ((chr‘𝑟) = 0 ↔ (chr‘𝑅) = 0)) |
9 | 7, 8 | anbi12d 631 |
. . . 4
⊢ (𝑟 = 𝑅 → (((ℤMod‘𝑟) ∈ NrmMod ∧
(chr‘𝑟) = 0) ↔
(𝑍 ∈ NrmMod ∧
(chr‘𝑅) =
0))) |
10 | | eleq1 2826 |
. . . . 5
⊢ (𝑟 = 𝑅 → (𝑟 ∈ CUnifSp ↔ 𝑅 ∈ CUnifSp)) |
11 | | fveq2 6774 |
. . . . . 6
⊢ (𝑟 = 𝑅 → (UnifSt‘𝑟) = (UnifSt‘𝑅)) |
12 | | fveq2 6774 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → (dist‘𝑟) = (dist‘𝑅)) |
13 | | fveq2 6774 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅)) |
14 | | isrrext.b |
. . . . . . . . . . 11
⊢ 𝐵 = (Base‘𝑅) |
15 | 13, 14 | eqtr4di 2796 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 → (Base‘𝑟) = 𝐵) |
16 | 15 | sqxpeqd 5621 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → ((Base‘𝑟) × (Base‘𝑟)) = (𝐵 × 𝐵)) |
17 | 12, 16 | reseq12d 5892 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → ((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟))) = ((dist‘𝑅) ↾ (𝐵 × 𝐵))) |
18 | | isrrext.v |
. . . . . . . 8
⊢ 𝐷 = ((dist‘𝑅) ↾ (𝐵 × 𝐵)) |
19 | 17, 18 | eqtr4di 2796 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → ((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟))) = 𝐷) |
20 | 19 | fveq2d 6778 |
. . . . . 6
⊢ (𝑟 = 𝑅 → (metUnif‘((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟)))) = (metUnif‘𝐷)) |
21 | 11, 20 | eqeq12d 2754 |
. . . . 5
⊢ (𝑟 = 𝑅 → ((UnifSt‘𝑟) = (metUnif‘((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟)))) ↔ (UnifSt‘𝑅) = (metUnif‘𝐷))) |
22 | 10, 21 | anbi12d 631 |
. . . 4
⊢ (𝑟 = 𝑅 → ((𝑟 ∈ CUnifSp ∧ (UnifSt‘𝑟) =
(metUnif‘((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟))))) ↔ (𝑅 ∈ CUnifSp ∧ (UnifSt‘𝑅) = (metUnif‘𝐷)))) |
23 | 9, 22 | anbi12d 631 |
. . 3
⊢ (𝑟 = 𝑅 → ((((ℤMod‘𝑟) ∈ NrmMod ∧
(chr‘𝑟) = 0) ∧
(𝑟 ∈ CUnifSp ∧
(UnifSt‘𝑟) =
(metUnif‘((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟)))))) ↔ ((𝑍 ∈ NrmMod ∧ (chr‘𝑅) = 0) ∧ (𝑅 ∈ CUnifSp ∧ (UnifSt‘𝑅) = (metUnif‘𝐷))))) |
24 | | df-rrext 31949 |
. . 3
⊢
ℝExt = {𝑟 ∈
(NrmRing ∩ DivRing) ∣ (((ℤMod‘𝑟) ∈ NrmMod ∧ (chr‘𝑟) = 0) ∧ (𝑟 ∈ CUnifSp ∧ (UnifSt‘𝑟) =
(metUnif‘((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟))))))} |
25 | 23, 24 | elrab2 3627 |
. 2
⊢ (𝑅 ∈ ℝExt ↔ (𝑅 ∈ (NrmRing ∩ DivRing)
∧ ((𝑍 ∈ NrmMod
∧ (chr‘𝑅) = 0)
∧ (𝑅 ∈ CUnifSp
∧ (UnifSt‘𝑅) =
(metUnif‘𝐷))))) |
26 | | 3anass 1094 |
. 2
⊢ (((𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing) ∧ (𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
(𝑅 ∈ CUnifSp ∧
(UnifSt‘𝑅) =
(metUnif‘𝐷))) ↔
((𝑅 ∈ NrmRing ∧
𝑅 ∈ DivRing) ∧
((𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
(𝑅 ∈ CUnifSp ∧
(UnifSt‘𝑅) =
(metUnif‘𝐷))))) |
27 | 2, 25, 26 | 3bitr4i 303 |
1
⊢ (𝑅 ∈ ℝExt ↔
((𝑅 ∈ NrmRing ∧
𝑅 ∈ DivRing) ∧
(𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
(𝑅 ∈ CUnifSp ∧
(UnifSt‘𝑅) =
(metUnif‘𝐷)))) |