Theorem drngui 20648

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

Syntax hints:   ∧ wa 395   = wceq 1541   ∈ wcel 2111   ∖ cdif 3899  {csn 4576  ‘cfv 6481  Basecbs 17117  0_gc0g 17340  Ringcrg 20149  Unitcui 20271  DivRingcdr 20642

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-iota 6437  df-fv 6489  df-drng 20644

This theorem is referenced by:  cnflddiv  21335  cnflddivOLD  21336  cnfldinv  21337  cnsubdrglem  21353  cnmgpabl  21363  cnmsubglem  21365  gzrngunit  21368  zringunit  21401  expghm  21410  psgninv  21517  zrhpsgnmhm  21519  amgmlem  26925  dchrghm  27192  dchrabs  27196  sum2dchr  27210  lgseisenlem4  27314  qrngdiv  27560  proot1ex  43228  amgmwlem  49833  amgmlemALT  49834