Theorem isrrext 33983

Description: Express the property "𝑅 is an extension of ℝ". (Contributed by Thierry Arnoux, 2-May-2018.)

Hypotheses

Ref	Expression
isrrext.b	⊢ 𝐵 = (Base‘𝑅)
isrrext.v	⊢ 𝐷 = ((dist‘𝑅) ↾ (𝐵 × 𝐵))
isrrext.z	⊢ 𝑍 = (ℤMod‘𝑅)

Assertion

Ref	Expression
isrrext	⊢ (𝑅 ∈ ℝExt ↔ ((𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing) ∧ (𝑍 ∈ NrmMod ∧ (chr‘𝑅) = 0) ∧ (𝑅 ∈ CUnifSp ∧ (UnifSt‘𝑅) = (metUnif‘𝐷))))

Proof of Theorem isrrext

Dummy variable 𝑟 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elin 3927	. . 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 6840	. . . . . . 7 ⊢ (𝑟 = 𝑅 → (ℤMod‘𝑟) = (ℤMod‘𝑅))
4	3	eleq1d 2813	. . . . . 6 ⊢ (𝑟 = 𝑅 → ((ℤMod‘𝑟) ∈ NrmMod ↔ (ℤMod‘𝑅) ∈ NrmMod))
5		isrrext.z	. . . . . . 7 ⊢ 𝑍 = (ℤMod‘𝑅)
6	5	eleq1i 2819	. . . . . 6 ⊢ (𝑍 ∈ NrmMod ↔ (ℤMod‘𝑅) ∈ NrmMod)
7	4, 6	bitr4di 289	. . . . 5 ⊢ (𝑟 = 𝑅 → ((ℤMod‘𝑟) ∈ NrmMod ↔ 𝑍 ∈ NrmMod))
8		fveqeq2 6849	. . . . 5 ⊢ (𝑟 = 𝑅 → ((chr‘𝑟) = 0 ↔ (chr‘𝑅) = 0))
9	7, 8	anbi12d 632	. . . 4 ⊢ (𝑟 = 𝑅 → (((ℤMod‘𝑟) ∈ NrmMod ∧ (chr‘𝑟) = 0) ↔ (𝑍 ∈ NrmMod ∧ (chr‘𝑅) = 0)))
10		eleq1 2816	. . . . 5 ⊢ (𝑟 = 𝑅 → (𝑟 ∈ CUnifSp ↔ 𝑅 ∈ CUnifSp))
11		fveq2 6840	. . . . . 6 ⊢ (𝑟 = 𝑅 → (UnifSt‘𝑟) = (UnifSt‘𝑅))
12		fveq2 6840	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → (dist‘𝑟) = (dist‘𝑅))
13		fveq2 6840	. . . . . . . . . . 11 ⊢ (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅))
14		isrrext.b	. . . . . . . . . . 11 ⊢ 𝐵 = (Base‘𝑅)
15	13, 14	eqtr4di 2782	. . . . . . . . . 10 ⊢ (𝑟 = 𝑅 → (Base‘𝑟) = 𝐵)
16	15	sqxpeqd 5663	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → ((Base‘𝑟) × (Base‘𝑟)) = (𝐵 × 𝐵))
17	12, 16	reseq12d 5940	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → ((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟))) = ((dist‘𝑅) ↾ (𝐵 × 𝐵)))
18		isrrext.v	. . . . . . . 8 ⊢ 𝐷 = ((dist‘𝑅) ↾ (𝐵 × 𝐵))
19	17, 18	eqtr4di 2782	. . . . . . 7 ⊢ (𝑟 = 𝑅 → ((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟))) = 𝐷)
20	19	fveq2d 6844	. . . . . 6 ⊢ (𝑟 = 𝑅 → (metUnif‘((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟)))) = (metUnif‘𝐷))
21	11, 20	eqeq12d 2745	. . . . 5 ⊢ (𝑟 = 𝑅 → ((UnifSt‘𝑟) = (metUnif‘((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟)))) ↔ (UnifSt‘𝑅) = (metUnif‘𝐷)))
22	10, 21	anbi12d 632	. . . 4 ⊢ (𝑟 = 𝑅 → ((𝑟 ∈ CUnifSp ∧ (UnifSt‘𝑟) = (metUnif‘((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟))))) ↔ (𝑅 ∈ CUnifSp ∧ (UnifSt‘𝑅) = (metUnif‘𝐷))))
23	9, 22	anbi12d 632	. . 3 ⊢ (𝑟 = 𝑅 → ((((ℤMod‘𝑟) ∈ NrmMod ∧ (chr‘𝑟) = 0) ∧ (𝑟 ∈ CUnifSp ∧ (UnifSt‘𝑟) = (metUnif‘((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟)))))) ↔ ((𝑍 ∈ NrmMod ∧ (chr‘𝑅) = 0) ∧ (𝑅 ∈ CUnifSp ∧ (UnifSt‘𝑅) = (metUnif‘𝐷)))))
24		df-rrext 33982	. . 3 ⊢ ℝExt = {𝑟 ∈ (NrmRing ∩ DivRing) ∣ (((ℤMod‘𝑟) ∈ NrmMod ∧ (chr‘𝑟) = 0) ∧ (𝑟 ∈ CUnifSp ∧ (UnifSt‘𝑟) = (metUnif‘((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟))))))}
25	23, 24	elrab2 3659	. 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‘𝐷))))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109   ∩ cin 3910   × cxp 5629   ↾ cres 5633  ‘cfv 6499  0cc0 11044  Basecbs 17155  distcds 17205  DivRingcdr 20649  metUnifcmetu 21287  ℤModczlm 21442  chrcchr 21443  UnifStcuss 24174  CUnifSpccusp 24217  NrmRingcnrg 24500  NrmModcnlm 24501   ℝExt crrext 33977

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-xp 5637  df-res 5643  df-iota 6452  df-fv 6507  df-rrext 33982

This theorem is referenced by:  rrextnrg  33984  rrextdrg  33985  rrextnlm  33986  rrextchr  33987  rrextcusp  33988  rrextust  33991  rerrext  33992  cnrrext  33993