df-rrext

Description: Define the class of extensions of RR . This is a shorthand for listing the necessary conditions for a structure to admit a canonical embedding of RR into it. Interestingly, this is not coming from a mathematical reference, but was from the necessary conditions to build the embedding at each step ( ZZ , QQ and RR ). It would be interesting see if this is formally treated in the literature. See isrrext for a better readable version. (Contributed by Thierry Arnoux, 2-May-2018)

		Ref	Expression
	Assertion	df-rrext	$⊢ ℝExt = \{r \in (NrmRing \cap DivRing) \| ((ℤMod (r) \in NrmMod \land chr (r) = 0) \land (r \in CUnifSp \land UnifSt (r) = metUnif ({dist (r) ↾}_{({Base}_{r} \times {Base}_{r})})))\}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crrext	$class ℝExt$
1		vr	$setvar r$
2		cnrg	$class NrmRing$
3		cdr	$class DivRing$
4	2 3	cin	$class (NrmRing \cap DivRing)$
5		czlm	$class ℤMod$
6	1	cv	$setvar r$
7	6 5	cfv	$class ℤMod (r)$
8		cnlm	$class NrmMod$
9	7 8	wcel	$wff ℤMod (r) \in NrmMod$
10		cchr	$class chr$
11	6 10	cfv	$class chr (r)$
12		cc0	$class 0$
13	11 12	wceq	$wff chr (r) = 0$
14	9 13	wa	$wff (ℤMod (r) \in NrmMod \land chr (r) = 0)$
15		ccusp	$class CUnifSp$
16	6 15	wcel	$wff r \in CUnifSp$
17		cuss	$class UnifSt$
18	6 17	cfv	$class UnifSt (r)$
19		cmetu	$class metUnif$
20		cds	$class dist$
21	6 20	cfv	$class dist (r)$
22		cbs	$class Base$
23	6 22	cfv	$class {Base}_{r}$
24	23 23	cxp	$class ({Base}_{r} \times {Base}_{r})$
25	21 24	cres	$class ({dist (r) ↾}_{({Base}_{r} \times {Base}_{r})})$
26	25 19	cfv	$class metUnif ({dist (r) ↾}_{({Base}_{r} \times {Base}_{r})})$
27	18 26	wceq	$wff UnifSt (r) = metUnif ({dist (r) ↾}_{({Base}_{r} \times {Base}_{r})})$
28	16 27	wa	$wff (r \in CUnifSp \land UnifSt (r) = metUnif ({dist (r) ↾}_{({Base}_{r} \times {Base}_{r})}))$
29	14 28	wa	$wff ((ℤMod (r) \in NrmMod \land chr (r) = 0) \land (r \in CUnifSp \land UnifSt (r) = metUnif ({dist (r) ↾}_{({Base}_{r} \times {Base}_{r})})))$
30	29 1 4	crab	$class \{r \in (NrmRing \cap DivRing) \| ((ℤMod (r) \in NrmMod \land chr (r) = 0) \land (r \in CUnifSp \land UnifSt (r) = metUnif ({dist (r) ↾}_{({Base}_{r} \times {Base}_{r})})))\}$
31	0 30	wceq	$wff ℝExt = \{r \in (NrmRing \cap DivRing) \| ((ℤMod (r) \in NrmMod \land chr (r) = 0) \land (r \in CUnifSp \land UnifSt (r) = metUnif ({dist (r) ↾}_{({Base}_{r} \times {Base}_{r})})))\}$

Metamath Proof Explorer

Definition df-rrext

Detailed syntax breakdown