Theorem drngui 20902

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

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570   ∈ wcel 2145   ∖ cdif 3899  {csn 4587  ‘cfv 6537  Basecbs 17307  0_gc0g 17530  Ringcrg 20378  Unitcui 20502  DivRingcdr 20896

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-iota 6493  df-fv 6545  df-drng 20898

This theorem is used by:  cnflddiv  21621  cnfldinv  21622  cnsubdrglem  21637  cnmgpabl  21647  cnmsubglem  21649  gzrngunit  21652  zringunit  21685  expghm  21694  psgninv  21801  zrhpsgnmhm  21803  amgmlem  27234  dchrghm  27500  dchrabs  27504  sum2dchr  27518  lgseisenlem4  27622  qrngdiv  27868  proot1ex  44045  amgmwlem  50828  amgmlemALT  50829