Theorem drngui 20700

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

Syntax hints:   ∧ wa 395   = wceq 1540   ∈ wcel 2109   ∖ cdif 3928  {csn 4606  ‘cfv 6536  Basecbs 17233  0_gc0g 17458  Ringcrg 20198  Unitcui 20320  DivRingcdr 20694

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-iota 6489  df-fv 6544  df-drng 20696

This theorem is referenced by:  cnflddiv  21368  cnflddivOLD  21369  cnfldinv  21370  cnsubdrglem  21391  cnmgpabl  21401  cnmsubglem  21403  gzrngunit  21406  zringunit  21432  expghm  21441  psgninv  21547  zrhpsgnmhm  21549  amgmlem  26957  dchrghm  27224  dchrabs  27228  sum2dchr  27242  lgseisenlem4  27346  qrngdiv  27592  proot1ex  43187  amgmwlem  49633  amgmlemALT  49634