Step | Hyp | Ref
| Expression |
1 | | elin 3758 |
. . 3
⊢ (𝑅 ∈ (NrmRing ∩ DivRing)
↔ (𝑅 ∈ NrmRing
∧ 𝑅 ∈
DivRing)) |
2 | 1 | anbi1i 727 |
. 2
⊢ ((𝑅 ∈ (NrmRing ∩ DivRing)
∧ ((𝑍 ∈ NrmMod
∧ (chr‘𝑅) = 0)
∧ (𝑅 ∈ CUnifSp
∧ (UnifSt‘𝑅) =
(metUnif‘𝐷)))) ↔
((𝑅 ∈ NrmRing ∧
𝑅 ∈ DivRing) ∧
((𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
(𝑅 ∈ CUnifSp ∧
(UnifSt‘𝑅) =
(metUnif‘𝐷))))) |
3 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → (ℤMod‘𝑟) = (ℤMod‘𝑅)) |
4 | 3 | eleq1d 2672 |
. . . . . 6
⊢ (𝑟 = 𝑅 → ((ℤMod‘𝑟) ∈ NrmMod ↔
(ℤMod‘𝑅) ∈
NrmMod)) |
5 | | isrrext.z |
. . . . . . 7
⊢ 𝑍 = (ℤMod‘𝑅) |
6 | 5 | eleq1i 2679 |
. . . . . 6
⊢ (𝑍 ∈ NrmMod ↔
(ℤMod‘𝑅) ∈
NrmMod) |
7 | 4, 6 | syl6bbr 277 |
. . . . 5
⊢ (𝑟 = 𝑅 → ((ℤMod‘𝑟) ∈ NrmMod ↔ 𝑍 ∈
NrmMod)) |
8 | | fveq2 6103 |
. . . . . 6
⊢ (𝑟 = 𝑅 → (chr‘𝑟) = (chr‘𝑅)) |
9 | 8 | eqeq1d 2612 |
. . . . 5
⊢ (𝑟 = 𝑅 → ((chr‘𝑟) = 0 ↔ (chr‘𝑅) = 0)) |
10 | 7, 9 | anbi12d 743 |
. . . 4
⊢ (𝑟 = 𝑅 → (((ℤMod‘𝑟) ∈ NrmMod ∧
(chr‘𝑟) = 0) ↔
(𝑍 ∈ NrmMod ∧
(chr‘𝑅) =
0))) |
11 | | eleq1 2676 |
. . . . 5
⊢ (𝑟 = 𝑅 → (𝑟 ∈ CUnifSp ↔ 𝑅 ∈ CUnifSp)) |
12 | | fveq2 6103 |
. . . . . 6
⊢ (𝑟 = 𝑅 → (UnifSt‘𝑟) = (UnifSt‘𝑅)) |
13 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → (dist‘𝑟) = (dist‘𝑅)) |
14 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅)) |
15 | | isrrext.b |
. . . . . . . . . . 11
⊢ 𝐵 = (Base‘𝑅) |
16 | 14, 15 | syl6eqr 2662 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 → (Base‘𝑟) = 𝐵) |
17 | 16 | sqxpeqd 5065 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → ((Base‘𝑟) × (Base‘𝑟)) = (𝐵 × 𝐵)) |
18 | 13, 17 | reseq12d 5318 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → ((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟))) = ((dist‘𝑅) ↾ (𝐵 × 𝐵))) |
19 | | isrrext.v |
. . . . . . . 8
⊢ 𝐷 = ((dist‘𝑅) ↾ (𝐵 × 𝐵)) |
20 | 18, 19 | syl6eqr 2662 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → ((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟))) = 𝐷) |
21 | 20 | fveq2d 6107 |
. . . . . 6
⊢ (𝑟 = 𝑅 → (metUnif‘((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟)))) = (metUnif‘𝐷)) |
22 | 12, 21 | eqeq12d 2625 |
. . . . 5
⊢ (𝑟 = 𝑅 → ((UnifSt‘𝑟) = (metUnif‘((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟)))) ↔ (UnifSt‘𝑅) = (metUnif‘𝐷))) |
23 | 11, 22 | anbi12d 743 |
. . . 4
⊢ (𝑟 = 𝑅 → ((𝑟 ∈ CUnifSp ∧ (UnifSt‘𝑟) =
(metUnif‘((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟))))) ↔ (𝑅 ∈ CUnifSp ∧ (UnifSt‘𝑅) = (metUnif‘𝐷)))) |
24 | 10, 23 | anbi12d 743 |
. . 3
⊢ (𝑟 = 𝑅 → ((((ℤMod‘𝑟) ∈ NrmMod ∧
(chr‘𝑟) = 0) ∧
(𝑟 ∈ CUnifSp ∧
(UnifSt‘𝑟) =
(metUnif‘((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟)))))) ↔ ((𝑍 ∈ NrmMod ∧ (chr‘𝑅) = 0) ∧ (𝑅 ∈ CUnifSp ∧ (UnifSt‘𝑅) = (metUnif‘𝐷))))) |
25 | | df-rrext 29371 |
. . 3
⊢
ℝExt = {𝑟 ∈
(NrmRing ∩ DivRing) ∣ (((ℤMod‘𝑟) ∈ NrmMod ∧ (chr‘𝑟) = 0) ∧ (𝑟 ∈ CUnifSp ∧ (UnifSt‘𝑟) =
(metUnif‘((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟))))))} |
26 | 24, 25 | elrab2 3333 |
. 2
⊢ (𝑅 ∈ ℝExt ↔ (𝑅 ∈ (NrmRing ∩ DivRing)
∧ ((𝑍 ∈ NrmMod
∧ (chr‘𝑅) = 0)
∧ (𝑅 ∈ CUnifSp
∧ (UnifSt‘𝑅) =
(metUnif‘𝐷))))) |
27 | | 3anass 1035 |
. 2
⊢ (((𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing) ∧ (𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
(𝑅 ∈ CUnifSp ∧
(UnifSt‘𝑅) =
(metUnif‘𝐷))) ↔
((𝑅 ∈ NrmRing ∧
𝑅 ∈ DivRing) ∧
((𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
(𝑅 ∈ CUnifSp ∧
(UnifSt‘𝑅) =
(metUnif‘𝐷))))) |
28 | 2, 26, 27 | 3bitr4i 291 |
1
⊢ (𝑅 ∈ ℝExt ↔
((𝑅 ∈ NrmRing ∧
𝑅 ∈ DivRing) ∧
(𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
(𝑅 ∈ CUnifSp ∧
(UnifSt‘𝑅) =
(metUnif‘𝐷)))) |