Metamath Proof Explorer

Theorem isrrext

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

Ref Expression
Hypotheses isrrext.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
isrrext.v ⊢ 𝐷 = ( ( dist ‘ 𝑅 ) ↾ ( 𝐵 × 𝐵 ) )
isrrext.z ⊢ 𝑍 = ( ℤMod ‘ 𝑅 )
Assertion isrrext ( 𝑅 ∈ ℝExt ↔ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing ) ∧ ( 𝑍 ∈ NrmMod ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑅 ∈ CUnifSp ∧ ( UnifSt ‘ 𝑅 ) = ( metUnif ‘ 𝐷 ) ) ) )

Proof

Step Hyp Ref Expression
1 isrrext.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 isrrext.v ⊢ 𝐷 = ( ( dist ‘ 𝑅 ) ↾ ( 𝐵 × 𝐵 ) )
3 isrrext.z ⊢ 𝑍 = ( ℤMod ‘ 𝑅 )
4 elin ⊢ ( 𝑅 ∈ ( NrmRing ∩ DivRing ) ↔ ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing ) )
5 4 anbi1i ⊢ ( ( 𝑅 ∈ ( NrmRing ∩ DivRing ) ∧ ( ( 𝑍 ∈ NrmMod ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑅 ∈ CUnifSp ∧ ( UnifSt ‘ 𝑅 ) = ( metUnif ‘ 𝐷 ) ) ) ) ↔ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing ) ∧ ( ( 𝑍 ∈ NrmMod ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑅 ∈ CUnifSp ∧ ( UnifSt ‘ 𝑅 ) = ( metUnif ‘ 𝐷 ) ) ) ) )
6 fveq2 ⊢ ( 𝑟 = 𝑅 → ( ℤMod ‘ 𝑟 ) = ( ℤMod ‘ 𝑅 ) )
7 6 eleq1d ⊢ ( 𝑟 = 𝑅 → ( ( ℤMod ‘ 𝑟 ) ∈ NrmMod ↔ ( ℤMod ‘ 𝑅 ) ∈ NrmMod ) )
8 3 eleq1i ⊢ ( 𝑍 ∈ NrmMod ↔ ( ℤMod ‘ 𝑅 ) ∈ NrmMod )
9 7 8 bitr4di ⊢ ( 𝑟 = 𝑅 → ( ( ℤMod ‘ 𝑟 ) ∈ NrmMod ↔ 𝑍 ∈ NrmMod ) )
10 fveqeq2 ⊢ ( 𝑟 = 𝑅 → ( ( chr ‘ 𝑟 ) = 0 ↔ ( chr ‘ 𝑅 ) = 0 ) )
11 9 10 anbi12d ⊢ ( 𝑟 = 𝑅 → ( ( ( ℤMod ‘ 𝑟 ) ∈ NrmMod ∧ ( chr ‘ 𝑟 ) = 0 ) ↔ ( 𝑍 ∈ NrmMod ∧ ( chr ‘ 𝑅 ) = 0 ) ) )
12 eleq1 ⊢ ( 𝑟 = 𝑅 → ( 𝑟 ∈ CUnifSp ↔ 𝑅 ∈ CUnifSp ) )
13 fveq2 ⊢ ( 𝑟 = 𝑅 → ( UnifSt ‘ 𝑟 ) = ( UnifSt ‘ 𝑅 ) )
14 fveq2 ⊢ ( 𝑟 = 𝑅 → ( dist ‘ 𝑟 ) = ( dist ‘ 𝑅 ) )
15 fveq2 ⊢ ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) = ( Base ‘ 𝑅 ) )
16 15 1 eqtr4di ⊢ ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) = 𝐵 )
17 16 sqxpeqd ⊢ ( 𝑟 = 𝑅 → ( ( Base ‘ 𝑟 ) × ( Base ‘ 𝑟 ) ) = ( 𝐵 × 𝐵 ) )
18 14 17 reseq12d ⊢ ( 𝑟 = 𝑅 → ( ( dist ‘ 𝑟 ) ↾ ( ( Base ‘ 𝑟 ) × ( Base ‘ 𝑟 ) ) ) = ( ( dist ‘ 𝑅 ) ↾ ( 𝐵 × 𝐵 ) ) )
19 18 2 eqtr4di ⊢ ( 𝑟 = 𝑅 → ( ( dist ‘ 𝑟 ) ↾ ( ( Base ‘ 𝑟 ) × ( Base ‘ 𝑟 ) ) ) = 𝐷 )
20 19 fveq2d ⊢ ( 𝑟 = 𝑅 → ( metUnif ‘ ( ( dist ‘ 𝑟 ) ↾ ( ( Base ‘ 𝑟 ) × ( Base ‘ 𝑟 ) ) ) ) = ( metUnif ‘ 𝐷 ) )
21 13 20 eqeq12d ⊢ ( 𝑟 = 𝑅 → ( ( UnifSt ‘ 𝑟 ) = ( metUnif ‘ ( ( dist ‘ 𝑟 ) ↾ ( ( Base ‘ 𝑟 ) × ( Base ‘ 𝑟 ) ) ) ) ↔ ( UnifSt ‘ 𝑅 ) = ( metUnif ‘ 𝐷 ) ) )
22 12 21 anbi12d ⊢ ( 𝑟 = 𝑅 → ( ( 𝑟 ∈ CUnifSp ∧ ( UnifSt ‘ 𝑟 ) = ( metUnif ‘ ( ( dist ‘ 𝑟 ) ↾ ( ( Base ‘ 𝑟 ) × ( Base ‘ 𝑟 ) ) ) ) ) ↔ ( 𝑅 ∈ CUnifSp ∧ ( UnifSt ‘ 𝑅 ) = ( metUnif ‘ 𝐷 ) ) ) )
23 11 22 anbi12d ⊢ ( 𝑟 = 𝑅 → ( ( ( ( ℤMod ‘ 𝑟 ) ∈ NrmMod ∧ ( chr ‘ 𝑟 ) = 0 ) ∧ ( 𝑟 ∈ CUnifSp ∧ ( UnifSt ‘ 𝑟 ) = ( metUnif ‘ ( ( dist ‘ 𝑟 ) ↾ ( ( Base ‘ 𝑟 ) × ( Base ‘ 𝑟 ) ) ) ) ) ) ↔ ( ( 𝑍 ∈ NrmMod ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑅 ∈ CUnifSp ∧ ( UnifSt ‘ 𝑅 ) = ( metUnif ‘ 𝐷 ) ) ) ) )
24 df-rrext ⊢ ℝExt = { 𝑟 ∈ ( NrmRing ∩ DivRing ) ∣ ( ( ( ℤMod ‘ 𝑟 ) ∈ NrmMod ∧ ( chr ‘ 𝑟 ) = 0 ) ∧ ( 𝑟 ∈ CUnifSp ∧ ( UnifSt ‘ 𝑟 ) = ( metUnif ‘ ( ( dist ‘ 𝑟 ) ↾ ( ( Base ‘ 𝑟 ) × ( Base ‘ 𝑟 ) ) ) ) ) ) }
25 23 24 elrab2 ⊢ ( 𝑅 ∈ ℝExt ↔ ( 𝑅 ∈ ( NrmRing ∩ DivRing ) ∧ ( ( 𝑍 ∈ NrmMod ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑅 ∈ CUnifSp ∧ ( UnifSt ‘ 𝑅 ) = ( metUnif ‘ 𝐷 ) ) ) ) )
26 3anass ⊢ ( ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing ) ∧ ( 𝑍 ∈ NrmMod ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑅 ∈ CUnifSp ∧ ( UnifSt ‘ 𝑅 ) = ( metUnif ‘ 𝐷 ) ) ) ↔ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing ) ∧ ( ( 𝑍 ∈ NrmMod ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑅 ∈ CUnifSp ∧ ( UnifSt ‘ 𝑅 ) = ( metUnif ‘ 𝐷 ) ) ) ) )
27 5 25 26 3bitr4i ⊢ ( 𝑅 ∈ ℝExt ↔ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing ) ∧ ( 𝑍 ∈ NrmMod ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑅 ∈ CUnifSp ∧ ( UnifSt ‘ 𝑅 ) = ( metUnif ‘ 𝐷 ) ) ) )