Theorem drngui 20991

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

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1569   ∈ wcel 2144   ∖ cdif 4045  {csn 4584  ‘cfv 6538  Basecbs 17392  0_gc0g 17615  Ringcrg 20464  Unitcui 20590  DivRingcdr 20985

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6546  df-drng 20987

This theorem is used by:  cnflddiv  21713  cnfldinv  21714  cnsubdrglem  21729  cnmgpabl  21739  cnmsubglem  21741  gzrngunit  21744  zringunit  21777  expghm  21786  psgninv  21893  zrhpsgnmhm  21895  amgmlem  27322  dchrghm  27588  dchrabs  27592  sum2dchr  27606  lgseisenlem4  27710  qrngdiv  27956  proot1ex  44291  amgmwlem  51155  amgmlemALT  51156