Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  isrrext Structured version   Visualization version   GIF version

Theorem isrrext 29850
 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.
StepHypRef Expression
1 elin 3779 . . 3 (𝑅 ∈ (NrmRing ∩ DivRing) ↔ (𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing))
21anbi1i 730 . 2 ((𝑅 ∈ (NrmRing ∩ DivRing) ∧ ((𝑍 ∈ NrmMod ∧ (chr‘𝑅) = 0) ∧ (𝑅 ∈ CUnifSp ∧ (UnifSt‘𝑅) = (metUnif‘𝐷)))) ↔ ((𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing) ∧ ((𝑍 ∈ NrmMod ∧ (chr‘𝑅) = 0) ∧ (𝑅 ∈ CUnifSp ∧ (UnifSt‘𝑅) = (metUnif‘𝐷)))))
3 fveq2 6153 . . . . . . 7 (𝑟 = 𝑅 → (ℤMod‘𝑟) = (ℤMod‘𝑅))
43eleq1d 2683 . . . . . 6 (𝑟 = 𝑅 → ((ℤMod‘𝑟) ∈ NrmMod ↔ (ℤMod‘𝑅) ∈ NrmMod))
5 isrrext.z . . . . . . 7 𝑍 = (ℤMod‘𝑅)
65eleq1i 2689 . . . . . 6 (𝑍 ∈ NrmMod ↔ (ℤMod‘𝑅) ∈ NrmMod)
74, 6syl6bbr 278 . . . . 5 (𝑟 = 𝑅 → ((ℤMod‘𝑟) ∈ NrmMod ↔ 𝑍 ∈ NrmMod))
8 fveq2 6153 . . . . . 6 (𝑟 = 𝑅 → (chr‘𝑟) = (chr‘𝑅))
98eqeq1d 2623 . . . . 5 (𝑟 = 𝑅 → ((chr‘𝑟) = 0 ↔ (chr‘𝑅) = 0))
107, 9anbi12d 746 . . . 4 (𝑟 = 𝑅 → (((ℤMod‘𝑟) ∈ NrmMod ∧ (chr‘𝑟) = 0) ↔ (𝑍 ∈ NrmMod ∧ (chr‘𝑅) = 0)))
11 eleq1 2686 . . . . 5 (𝑟 = 𝑅 → (𝑟 ∈ CUnifSp ↔ 𝑅 ∈ CUnifSp))
12 fveq2 6153 . . . . . 6 (𝑟 = 𝑅 → (UnifSt‘𝑟) = (UnifSt‘𝑅))
13 fveq2 6153 . . . . . . . . 9 (𝑟 = 𝑅 → (dist‘𝑟) = (dist‘𝑅))
14 fveq2 6153 . . . . . . . . . . 11 (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅))
15 isrrext.b . . . . . . . . . . 11 𝐵 = (Base‘𝑅)
1614, 15syl6eqr 2673 . . . . . . . . . 10 (𝑟 = 𝑅 → (Base‘𝑟) = 𝐵)
1716sqxpeqd 5106 . . . . . . . . 9 (𝑟 = 𝑅 → ((Base‘𝑟) × (Base‘𝑟)) = (𝐵 × 𝐵))
1813, 17reseq12d 5362 . . . . . . . 8 (𝑟 = 𝑅 → ((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟))) = ((dist‘𝑅) ↾ (𝐵 × 𝐵)))
19 isrrext.v . . . . . . . 8 𝐷 = ((dist‘𝑅) ↾ (𝐵 × 𝐵))
2018, 19syl6eqr 2673 . . . . . . 7 (𝑟 = 𝑅 → ((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟))) = 𝐷)
2120fveq2d 6157 . . . . . 6 (𝑟 = 𝑅 → (metUnif‘((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟)))) = (metUnif‘𝐷))
2212, 21eqeq12d 2636 . . . . 5 (𝑟 = 𝑅 → ((UnifSt‘𝑟) = (metUnif‘((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟)))) ↔ (UnifSt‘𝑅) = (metUnif‘𝐷)))
2311, 22anbi12d 746 . . . 4 (𝑟 = 𝑅 → ((𝑟 ∈ CUnifSp ∧ (UnifSt‘𝑟) = (metUnif‘((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟))))) ↔ (𝑅 ∈ CUnifSp ∧ (UnifSt‘𝑅) = (metUnif‘𝐷))))
2410, 23anbi12d 746 . . 3 (𝑟 = 𝑅 → ((((ℤMod‘𝑟) ∈ NrmMod ∧ (chr‘𝑟) = 0) ∧ (𝑟 ∈ CUnifSp ∧ (UnifSt‘𝑟) = (metUnif‘((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟)))))) ↔ ((𝑍 ∈ NrmMod ∧ (chr‘𝑅) = 0) ∧ (𝑅 ∈ CUnifSp ∧ (UnifSt‘𝑅) = (metUnif‘𝐷)))))
25 df-rrext 29849 . . 3 ℝExt = {𝑟 ∈ (NrmRing ∩ DivRing) ∣ (((ℤMod‘𝑟) ∈ NrmMod ∧ (chr‘𝑟) = 0) ∧ (𝑟 ∈ CUnifSp ∧ (UnifSt‘𝑟) = (metUnif‘((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟))))))}
2624, 25elrab2 3352 . 2 (𝑅 ∈ ℝExt ↔ (𝑅 ∈ (NrmRing ∩ DivRing) ∧ ((𝑍 ∈ NrmMod ∧ (chr‘𝑅) = 0) ∧ (𝑅 ∈ CUnifSp ∧ (UnifSt‘𝑅) = (metUnif‘𝐷)))))
27 3anass 1040 . 2 (((𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing) ∧ (𝑍 ∈ NrmMod ∧ (chr‘𝑅) = 0) ∧ (𝑅 ∈ CUnifSp ∧ (UnifSt‘𝑅) = (metUnif‘𝐷))) ↔ ((𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing) ∧ ((𝑍 ∈ NrmMod ∧ (chr‘𝑅) = 0) ∧ (𝑅 ∈ CUnifSp ∧ (UnifSt‘𝑅) = (metUnif‘𝐷)))))
282, 26, 273bitr4i 292 1 (𝑅 ∈ ℝExt ↔ ((𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing) ∧ (𝑍 ∈ NrmMod ∧ (chr‘𝑅) = 0) ∧ (𝑅 ∈ CUnifSp ∧ (UnifSt‘𝑅) = (metUnif‘𝐷))))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 196   ∧ wa 384   ∧ w3a 1036   = wceq 1480   ∈ wcel 1987   ∩ cin 3558   × cxp 5077   ↾ cres 5081  ‘cfv 5852  0cc0 9888  Basecbs 15792  distcds 15882  DivRingcdr 18679  metUnifcmetu 19669  ℤModczlm 19781  chrcchr 19782  UnifStcuss 21980  CUnifSpccusp 22024  NrmRingcnrg 22307  NrmModcnlm 22308   ℝExt crrext 29844 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rex 2913  df-rab 2916  df-v 3191  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-br 4619  df-opab 4679  df-xp 5085  df-res 5091  df-iota 5815  df-fv 5860  df-rrext 29849 This theorem is referenced by:  rrextnrg  29851  rrextdrg  29852  rrextnlm  29853  rrextchr  29854  rrextcusp  29855  rrextust  29858  rerrext  29859  cnrrext  29860
 Copyright terms: Public domain W3C validator