Theorem isrrext 34182

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 3919	. . 3 ⊢ (𝑅 ∈ (NrmRing ∩ DivRing) ↔ (𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing))
2	1	anbi1i 625	. 2 ⊢ ((𝑅 ∈ (NrmRing ∩ DivRing) ∧ ((𝑍 ∈ NrmMod ∧ (chr‘𝑅) = 0) ∧ (𝑅 ∈ CUnifSp ∧ (UnifSt‘𝑅) = (metUnif‘𝐷)))) ↔ ((𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing) ∧ ((𝑍 ∈ NrmMod ∧ (chr‘𝑅) = 0) ∧ (𝑅 ∈ CUnifSp ∧ (UnifSt‘𝑅) = (metUnif‘𝐷)))))
3		fveq2 6842	. . . . . . 7 ⊢ (𝑟 = 𝑅 → (ℤMod‘𝑟) = (ℤMod‘𝑅))
4	3	eleq1d 2822	. . . . . 6 ⊢ (𝑟 = 𝑅 → ((ℤMod‘𝑟) ∈ NrmMod ↔ (ℤMod‘𝑅) ∈ NrmMod))
5		isrrext.z	. . . . . . 7 ⊢ 𝑍 = (ℤMod‘𝑅)
6	5	eleq1i 2828	. . . . . 6 ⊢ (𝑍 ∈ NrmMod ↔ (ℤMod‘𝑅) ∈ NrmMod)
7	4, 6	bitr4di 289	. . . . 5 ⊢ (𝑟 = 𝑅 → ((ℤMod‘𝑟) ∈ NrmMod ↔ 𝑍 ∈ NrmMod))
8		fveqeq2 6851	. . . . 5 ⊢ (𝑟 = 𝑅 → ((chr‘𝑟) = 0 ↔ (chr‘𝑅) = 0))
9	7, 8	anbi12d 633	. . . 4 ⊢ (𝑟 = 𝑅 → (((ℤMod‘𝑟) ∈ NrmMod ∧ (chr‘𝑟) = 0) ↔ (𝑍 ∈ NrmMod ∧ (chr‘𝑅) = 0)))
10		eleq1 2825	. . . . 5 ⊢ (𝑟 = 𝑅 → (𝑟 ∈ CUnifSp ↔ 𝑅 ∈ CUnifSp))
11		fveq2 6842	. . . . . 6 ⊢ (𝑟 = 𝑅 → (UnifSt‘𝑟) = (UnifSt‘𝑅))
12		fveq2 6842	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → (dist‘𝑟) = (dist‘𝑅))
13		fveq2 6842	. . . . . . . . . . 11 ⊢ (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅))
14		isrrext.b	. . . . . . . . . . 11 ⊢ 𝐵 = (Base‘𝑅)
15	13, 14	eqtr4di 2790	. . . . . . . . . 10 ⊢ (𝑟 = 𝑅 → (Base‘𝑟) = 𝐵)
16	15	sqxpeqd 5664	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → ((Base‘𝑟) × (Base‘𝑟)) = (𝐵 × 𝐵))
17	12, 16	reseq12d 5947	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → ((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟))) = ((dist‘𝑅) ↾ (𝐵 × 𝐵)))
18		isrrext.v	. . . . . . . 8 ⊢ 𝐷 = ((dist‘𝑅) ↾ (𝐵 × 𝐵))
19	17, 18	eqtr4di 2790	. . . . . . 7 ⊢ (𝑟 = 𝑅 → ((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟))) = 𝐷)
20	19	fveq2d 6846	. . . . . 6 ⊢ (𝑟 = 𝑅 → (metUnif‘((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟)))) = (metUnif‘𝐷))
21	11, 20	eqeq12d 2753	. . . . 5 ⊢ (𝑟 = 𝑅 → ((UnifSt‘𝑟) = (metUnif‘((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟)))) ↔ (UnifSt‘𝑅) = (metUnif‘𝐷)))
22	10, 21	anbi12d 633	. . . 4 ⊢ (𝑟 = 𝑅 → ((𝑟 ∈ CUnifSp ∧ (UnifSt‘𝑟) = (metUnif‘((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟))))) ↔ (𝑅 ∈ CUnifSp ∧ (UnifSt‘𝑅) = (metUnif‘𝐷))))
23	9, 22	anbi12d 633	. . 3 ⊢ (𝑟 = 𝑅 → ((((ℤMod‘𝑟) ∈ NrmMod ∧ (chr‘𝑟) = 0) ∧ (𝑟 ∈ CUnifSp ∧ (UnifSt‘𝑟) = (metUnif‘((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟)))))) ↔ ((𝑍 ∈ NrmMod ∧ (chr‘𝑅) = 0) ∧ (𝑅 ∈ CUnifSp ∧ (UnifSt‘𝑅) = (metUnif‘𝐷)))))
24		df-rrext 34181	. . 3 ⊢ ℝExt = {𝑟 ∈ (NrmRing ∩ DivRing) ∣ (((ℤMod‘𝑟) ∈ NrmMod ∧ (chr‘𝑟) = 0) ∧ (𝑟 ∈ CUnifSp ∧ (UnifSt‘𝑟) = (metUnif‘((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟))))))}
25	23, 24	elrab2 3651	. 2 ⊢ (𝑅 ∈ ℝExt ↔ (𝑅 ∈ (NrmRing ∩ DivRing) ∧ ((𝑍 ∈ NrmMod ∧ (chr‘𝑅) = 0) ∧ (𝑅 ∈ CUnifSp ∧ (UnifSt‘𝑅) = (metUnif‘𝐷)))))
26		3anass 1095	. 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 1087   = wceq 1542   ∈ wcel 2114   ∩ cin 3902   × cxp 5630   ↾ cres 5634  ‘cfv 6500  0cc0 11038  Basecbs 17148  distcds 17198  DivRingcdr 20677  metUnifcmetu 21315  ℤModczlm 21470  chrcchr 21471  UnifStcuss 24212  CUnifSpccusp 24255  NrmRingcnrg 24538  NrmModcnlm 24539   ℝExt crrext 34176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-xp 5638  df-res 5644  df-iota 6456  df-fv 6508  df-rrext 34181

This theorem is referenced by:  rrextnrg  34183  rrextdrg  34184  rrextnlm  34185  rrextchr  34186  rrextcusp  34187  rrextust  34190  rerrext  34191  cnrrext  34192