Theorem rrextchr 34164

Description: The ring characteristic of an extension of ℝ is zero. (Contributed by Thierry Arnoux, 2-May-2018.)

Assertion

Ref	Expression
rrextchr	⊢ (𝑅 ∈ ℝExt → (chr‘𝑅) = 0)

Proof of Theorem rrextchr

Step	Hyp	Ref	Expression
1		eqid 2737	. . . 4 ⊢ (Base‘𝑅) = (Base‘𝑅)
2		eqid 2737	. . . 4 ⊢ ((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅))) = ((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))
3		eqid 2737	. . . 4 ⊢ (ℤMod‘𝑅) = (ℤMod‘𝑅)
4	1, 2, 3	isrrext 34160	. . 3 ⊢ (𝑅 ∈ ℝExt ↔ ((𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing) ∧ ((ℤMod‘𝑅) ∈ NrmMod ∧ (chr‘𝑅) = 0) ∧ (𝑅 ∈ CUnifSp ∧ (UnifSt‘𝑅) = (metUnif‘((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))))))
5	4	simp2bi 1147	. 2 ⊢ (𝑅 ∈ ℝExt → ((ℤMod‘𝑅) ∈ NrmMod ∧ (chr‘𝑅) = 0))
6	5	simprd 495	1 ⊢ (𝑅 ∈ ℝExt → (chr‘𝑅) = 0)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114   × cxp 5622   ↾ cres 5626  ‘cfv 6492  0cc0 11029  Basecbs 17170  distcds 17220  DivRingcdr 20697  metUnifcmetu 21335  ℤModczlm 21490  chrcchr 21491  UnifStcuss 24228  CUnifSpccusp 24271  NrmRingcnrg 24554  NrmModcnlm 24555   ℝExt crrext 34154

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-xp 5630  df-res 5636  df-iota 6448  df-fv 6500  df-rrext 34159

This theorem is referenced by:  rrhfe  34172  rrhcne  34173  rrhqima  34174  rrh0  34175  sitgclg  34502