Theorem isrrext 34699

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 4096	. . 3 ⊢ (𝑅 ∈ (NrmRing ∩ DivRing) ↔ (𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing))
2	1	anbi1i 636	. 2 ⊢ ((𝑅 ∈ (NrmRing ∩ DivRing) ∧ ((𝑍 ∈ NrmMod ∧ (chr‘𝑅) = 0) ∧ (𝑅 ∈ CUnifSp ∧ (UnifSt‘𝑅) = (metUnif‘𝐷)))) ↔ ((𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing) ∧ ((𝑍 ∈ NrmMod ∧ (chr‘𝑅) = 0) ∧ (𝑅 ∈ CUnifSp ∧ (UnifSt‘𝑅) = (metUnif‘𝐷)))))
3		fveq2 6905	. . . . . . 7 ⊢ (𝑟 = 𝑅 → (ℤMod‘𝑟) = (ℤMod‘𝑅))
4	3	eleq1d 2849	. . . . . 6 ⊢ (𝑟 = 𝑅 → ((ℤMod‘𝑟) ∈ NrmMod ↔ (ℤMod‘𝑅) ∈ NrmMod))
5		isrrext.z	. . . . . . 7 ⊢ 𝑍 = (ℤMod‘𝑅)
6	5	eleq1i 2855	. . . . . 6 ⊢ (𝑍 ∈ NrmMod ↔ (ℤMod‘𝑅) ∈ NrmMod)
7	4, 6	bitr4di 292	. . . . 5 ⊢ (𝑟 = 𝑅 → ((ℤMod‘𝑟) ∈ NrmMod ↔ 𝑍 ∈ NrmMod))
8		fveqeq2 6914	. . . . 5 ⊢ (𝑟 = 𝑅 → ((chr‘𝑟) = 0 ↔ (chr‘𝑅) = 0))
9	7, 8	anbi12d 644	. . . 4 ⊢ (𝑟 = 𝑅 → (((ℤMod‘𝑟) ∈ NrmMod ∧ (chr‘𝑟) = 0) ↔ (𝑍 ∈ NrmMod ∧ (chr‘𝑅) = 0)))
10		eleq1 2852	. . . . 5 ⊢ (𝑟 = 𝑅 → (𝑟 ∈ CUnifSp ↔ 𝑅 ∈ CUnifSp))
11		fveq2 6905	. . . . . 6 ⊢ (𝑟 = 𝑅 → (UnifSt‘𝑟) = (UnifSt‘𝑅))
12		fveq2 6905	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → (dist‘𝑟) = (dist‘𝑅))
13		fveq2 6905	. . . . . . . . . . 11 ⊢ (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅))
14		isrrext.b	. . . . . . . . . . 11 ⊢ 𝐵 = (Base‘𝑅)
15	13, 14	eqtr4di 2816	. . . . . . . . . 10 ⊢ (𝑟 = 𝑅 → (Base‘𝑟) = 𝐵)
16	15	sqxpeqd 5687	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → ((Base‘𝑟) × (Base‘𝑟)) = (𝐵 × 𝐵))
17	12, 16	reseq12d 5981	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → ((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟))) = ((dist‘𝑅) ↾ (𝐵 × 𝐵)))
18		isrrext.v	. . . . . . . 8 ⊢ 𝐷 = ((dist‘𝑅) ↾ (𝐵 × 𝐵))
19	17, 18	eqtr4di 2816	. . . . . . 7 ⊢ (𝑟 = 𝑅 → ((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟))) = 𝐷)
20	19	fveq2d 6909	. . . . . 6 ⊢ (𝑟 = 𝑅 → (metUnif‘((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟)))) = (metUnif‘𝐷))
21	11, 20	eqeq12d 2779	. . . . 5 ⊢ (𝑟 = 𝑅 → ((UnifSt‘𝑟) = (metUnif‘((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟)))) ↔ (UnifSt‘𝑅) = (metUnif‘𝐷)))
22	10, 21	anbi12d 644	. . . 4 ⊢ (𝑟 = 𝑅 → ((𝑟 ∈ CUnifSp ∧ (UnifSt‘𝑟) = (metUnif‘((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟))))) ↔ (𝑅 ∈ CUnifSp ∧ (UnifSt‘𝑅) = (metUnif‘𝐷))))
23	9, 22	anbi12d 644	. . 3 ⊢ (𝑟 = 𝑅 → ((((ℤMod‘𝑟) ∈ NrmMod ∧ (chr‘𝑟) = 0) ∧ (𝑟 ∈ CUnifSp ∧ (UnifSt‘𝑟) = (metUnif‘((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟)))))) ↔ ((𝑍 ∈ NrmMod ∧ (chr‘𝑅) = 0) ∧ (𝑅 ∈ CUnifSp ∧ (UnifSt‘𝑅) = (metUnif‘𝐷)))))
24		df-rrext 34698	. . 3 ⊢ ℝExt = {𝑟 ∈ (NrmRing ∩ DivRing) ∣ (((ℤMod‘𝑟) ∈ NrmMod ∧ (chr‘𝑟) = 0) ∧ (𝑟 ∈ CUnifSp ∧ (UnifSt‘𝑟) = (metUnif‘((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟))))))}
25	23, 24	elrab2 3652	. 2 ⊢ (𝑅 ∈ ℝExt ↔ (𝑅 ∈ (NrmRing ∩ DivRing) ∧ ((𝑍 ∈ NrmMod ∧ (chr‘𝑅) = 0) ∧ (𝑅 ∈ CUnifSp ∧ (UnifSt‘𝑅) = (metUnif‘𝐷)))))
26		3anass 1111	. 2 ⊢ (((𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing) ∧ (𝑍 ∈ NrmMod ∧ (chr‘𝑅) = 0) ∧ (𝑅 ∈ CUnifSp ∧ (UnifSt‘𝑅) = (metUnif‘𝐷))) ↔ ((𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing) ∧ ((𝑍 ∈ NrmMod ∧ (chr‘𝑅) = 0) ∧ (𝑅 ∈ CUnifSp ∧ (UnifSt‘𝑅) = (metUnif‘𝐷)))))
27	2, 25, 26	3bitr4i 306	1 ⊢ (𝑅 ∈ ℝExt ↔ ((𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing) ∧ (𝑍 ∈ NrmMod ∧ (chr‘𝑅) = 0) ∧ (𝑅 ∈ CUnifSp ∧ (UnifSt‘𝑅) = (metUnif‘𝐷))))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2147   ∩ cin 4092   × cxp 5653   ↾ cres 5657  ‘cfv 6555  0cc0 11224  Basecbs 17413  distcds 17463  DivRingcdr 21007  metUnifcmetu 21696  ℤModczlm 21833  chrcchr 21834  UnifStcuss 24599  CUnifSpccusp 24642  NrmRingcnrg 24925  NrmModcnlm 24926   ℝExt crrext 34693

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-xp 5661  df-res 5667  df-iota 6509  df-fv 6563  df-rrext 34698

This theorem is used by:  rrextnrg  34700  rrextdrg  34701  rrextnlm  34702  rrextchr  34703  rrextcusp  34704  rrextust  34707  rerrext  34708  cnrrext  34709