Theorem drngui 18955

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 2804	. . . . 5 ⊢ (Unit‘𝑅) = (Unit‘𝑅)
4		drngui.z	. . . . 5 ⊢ 0 = (0g‘𝑅)
5	2, 3, 4	isdrng 18953	. . . 4 ⊢ (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧ (Unit‘𝑅) = (𝐵 ∖ { 0 })))
6	1, 5	mpbi 221	. . 3 ⊢ (𝑅 ∈ Ring ∧ (Unit‘𝑅) = (𝐵 ∖ { 0 }))
7	6	simpri 475	. 2 ⊢ (Unit‘𝑅) = (𝐵 ∖ { 0 })
8	7	eqcomi 2813	1 ⊢ (𝐵 ∖ { 0 }) = (Unit‘𝑅)

Syntax hints:   ∧ wa 384   = wceq 1637   ∈ wcel 2156   ∖ cdif 3764  {csn 4368  ‘cfv 6099  Basecbs 16066  0_gc0g 16303  Ringcrg 18747  Unitcui 18839  DivRingcdr 18949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2782

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2791  df-cleq 2797  df-clel 2800  df-nfc 2935  df-ral 3099  df-rex 3100  df-rab 3103  df-v 3391  df-dif 3770  df-un 3772  df-in 3774  df-ss 3781  df-nul 4115  df-if 4278  df-sn 4369  df-pr 4371  df-op 4375  df-uni 4629  df-br 4843  df-iota 6062  df-fv 6107  df-drng 18951

This theorem is referenced by:  cnflddiv  19982  cnfldinv  19983  cnsubdrglem  20003  cnmgpabl  20013  cnmsubglem  20015  gzrngunit  20018  zringunit  20042  expghm  20050  psgninv  20133  zrhpsgnmhm  20135  amgmlem  24928  dchrghm  25193  dchrabs  25197  sum2dchr  25211  lgseisenlem4  25315  qrngdiv  25525  proot1ex  38278  amgmwlem  43117  amgmlemALT  43118