Theorem drngui 19589

Description: The set of units of a division ring. (Contributed by Mario Carneiro, 2-Dec-2014.)

Hypotheses

Ref	Expression
drngui.b	⊢ 𝐵 = (Base‘𝑅)
drngui.z	⊢ 0 = (0g‘𝑅)
drngui.r	⊢ 𝑅 ∈ DivRing

Assertion

Ref	Expression
drngui	⊢ (𝐵 ∖ { 0 }) = (Unit‘𝑅)

Proof of Theorem drngui

Step	Hyp	Ref	Expression
1		drngui.r	. . . 4 ⊢ 𝑅 ∈ DivRing
2		drngui.b	. . . . 5 ⊢ 𝐵 = (Base‘𝑅)
3		eqid 2758	. . . . 5 ⊢ (Unit‘𝑅) = (Unit‘𝑅)
4		drngui.z	. . . . 5 ⊢ 0 = (0g‘𝑅)
5	2, 3, 4	isdrng 19587	. . . 4 ⊢ (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧ (Unit‘𝑅) = (𝐵 ∖ { 0 })))
6	1, 5	mpbi 233	. . 3 ⊢ (𝑅 ∈ Ring ∧ (Unit‘𝑅) = (𝐵 ∖ { 0 }))
7	6	simpri 489	. 2 ⊢ (Unit‘𝑅) = (𝐵 ∖ { 0 })
8	7	eqcomi 2767	1 ⊢ (𝐵 ∖ { 0 }) = (Unit‘𝑅)

Syntax hints:   ∧ wa 399   = wceq 1538   ∈ wcel 2111   ∖ cdif 3857  {csn 4525  ‘cfv 6340  Basecbs 16554  0_gc0g 16784  Ringcrg 19378  Unitcui 19473  DivRingcdr 19583

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-rab 3079  df-v 3411  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-br 5037  df-iota 6299  df-fv 6348  df-drng 19585

This theorem is referenced by:  cnflddiv  20209  cnfldinv  20210  cnsubdrglem  20230  cnmgpabl  20240  cnmsubglem  20242  gzrngunit  20245  zringunit  20269  expghm  20278  psgninv  20360  zrhpsgnmhm  20362  amgmlem  25687  dchrghm  25952  dchrabs  25956  sum2dchr  25970  lgseisenlem4  26074  qrngdiv  26320  proot1ex  40553  amgmwlem  45815  amgmlemALT  45816