Metamath Proof Explorer

Definition 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 = { 𝑟 ∈ ( NrmRing ∩ DivRing ) ∣ ( ( ( ℤMod ‘ 𝑟 ) ∈ NrmMod ∧ ( chr ‘ 𝑟 ) = 0 ) ∧ ( 𝑟 ∈ CUnifSp ∧ ( UnifSt ‘ 𝑟 ) = ( metUnif ‘ ( ( dist ‘ 𝑟 ) ↾ ( ( Base ‘ 𝑟 ) × ( Base ‘ 𝑟 ) ) ) ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 crrext ⊢ ℝExt
1 vr ⊢ 𝑟
2 cnrg ⊢ NrmRing
3 cdr ⊢ DivRing
4 2 3 cin ⊢ ( NrmRing ∩ DivRing )
5 czlm ⊢ ℤMod
6 1 cv ⊢ 𝑟
7 6 5 cfv ⊢ ( ℤMod ‘ 𝑟 )
8 cnlm ⊢ NrmMod
9 7 8 wcel ⊢ ( ℤMod ‘ 𝑟 ) ∈ NrmMod
10 cchr ⊢ chr
11 6 10 cfv ⊢ ( chr ‘ 𝑟 )
12 cc0 ⊢ 0
13 11 12 wceq ⊢ ( chr ‘ 𝑟 ) = 0
14 9 13 wa ⊢ ( ( ℤMod ‘ 𝑟 ) ∈ NrmMod ∧ ( chr ‘ 𝑟 ) = 0 )
15 ccusp ⊢ CUnifSp
16 6 15 wcel ⊢ 𝑟 ∈ CUnifSp
17 cuss ⊢ UnifSt
18 6 17 cfv ⊢ ( UnifSt ‘ 𝑟 )
19 cmetu ⊢ metUnif
20 cds ⊢ dist
21 6 20 cfv ⊢ ( dist ‘ 𝑟 )
22 cbs ⊢ Base
23 6 22 cfv ⊢ ( Base ‘ 𝑟 )
24 23 23 cxp ⊢ ( ( Base ‘ 𝑟 ) × ( Base ‘ 𝑟 ) )
25 21 24 cres ⊢ ( ( dist ‘ 𝑟 ) ↾ ( ( Base ‘ 𝑟 ) × ( Base ‘ 𝑟 ) ) )
26 25 19 cfv ⊢ ( metUnif ‘ ( ( dist ‘ 𝑟 ) ↾ ( ( Base ‘ 𝑟 ) × ( Base ‘ 𝑟 ) ) ) )
27 18 26 wceq ⊢ ( UnifSt ‘ 𝑟 ) = ( metUnif ‘ ( ( dist ‘ 𝑟 ) ↾ ( ( Base ‘ 𝑟 ) × ( Base ‘ 𝑟 ) ) ) )
28 16 27 wa ⊢ ( 𝑟 ∈ CUnifSp ∧ ( UnifSt ‘ 𝑟 ) = ( metUnif ‘ ( ( dist ‘ 𝑟 ) ↾ ( ( Base ‘ 𝑟 ) × ( Base ‘ 𝑟 ) ) ) ) )
29 14 28 wa ⊢ ( ( ( ℤMod ‘ 𝑟 ) ∈ NrmMod ∧ ( chr ‘ 𝑟 ) = 0 ) ∧ ( 𝑟 ∈ CUnifSp ∧ ( UnifSt ‘ 𝑟 ) = ( metUnif ‘ ( ( dist ‘ 𝑟 ) ↾ ( ( Base ‘ 𝑟 ) × ( Base ‘ 𝑟 ) ) ) ) ) )
30 29 1 4 crab ⊢ { 𝑟 ∈ ( NrmRing ∩ DivRing ) ∣ ( ( ( ℤMod ‘ 𝑟 ) ∈ NrmMod ∧ ( chr ‘ 𝑟 ) = 0 ) ∧ ( 𝑟 ∈ CUnifSp ∧ ( UnifSt ‘ 𝑟 ) = ( metUnif ‘ ( ( dist ‘ 𝑟 ) ↾ ( ( Base ‘ 𝑟 ) × ( Base ‘ 𝑟 ) ) ) ) ) ) }
31 0 30 wceq ⊢ ℝExt = { 𝑟 ∈ ( NrmRing ∩ DivRing ) ∣ ( ( ( ℤMod ‘ 𝑟 ) ∈ NrmMod ∧ ( chr ‘ 𝑟 ) = 0 ) ∧ ( 𝑟 ∈ CUnifSp ∧ ( UnifSt ‘ 𝑟 ) = ( metUnif ‘ ( ( dist ‘ 𝑟 ) ↾ ( ( Base ‘ 𝑟 ) × ( Base ‘ 𝑟 ) ) ) ) ) ) }