Theorem isdrng 20678

Description: The predicate "is a division ring". (Contributed by NM, 18-Oct-2012.) (Revised by Mario Carneiro, 2-Dec-2014.)

Hypotheses

Ref	Expression
isdrng.b	⊢ 𝐵 = (Base‘𝑅)
isdrng.u	⊢ 𝑈 = (Unit‘𝑅)
isdrng.z	⊢ 0 = (0g‘𝑅)

Assertion

Ref	Expression
isdrng	⊢ (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧ 𝑈 = (𝐵 ∖ { 0 })))

Proof of Theorem isdrng

Dummy variable 𝑟 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 6842	. . . 4 ⊢ (𝑟 = 𝑅 → (Unit‘𝑟) = (Unit‘𝑅))
2		isdrng.u	. . . 4 ⊢ 𝑈 = (Unit‘𝑅)
3	1, 2	eqtr4di 2790	. . 3 ⊢ (𝑟 = 𝑅 → (Unit‘𝑟) = 𝑈)
4		fveq2 6842	. . . . 5 ⊢ (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅))
5		isdrng.b	. . . . 5 ⊢ 𝐵 = (Base‘𝑅)
6	4, 5	eqtr4di 2790	. . . 4 ⊢ (𝑟 = 𝑅 → (Base‘𝑟) = 𝐵)
7		fveq2 6842	. . . . . 6 ⊢ (𝑟 = 𝑅 → (0g‘𝑟) = (0g‘𝑅))
8		isdrng.z	. . . . . 6 ⊢ 0 = (0g‘𝑅)
9	7, 8	eqtr4di 2790	. . . . 5 ⊢ (𝑟 = 𝑅 → (0g‘𝑟) = 0 )
10	9	sneqd 4594	. . . 4 ⊢ (𝑟 = 𝑅 → {(0g‘𝑟)} = { 0 })
11	6, 10	difeq12d 4081	. . 3 ⊢ (𝑟 = 𝑅 → ((Base‘𝑟) ∖ {(0g‘𝑟)}) = (𝐵 ∖ { 0 }))
12	3, 11	eqeq12d 2753	. 2 ⊢ (𝑟 = 𝑅 → ((Unit‘𝑟) = ((Base‘𝑟) ∖ {(0g‘𝑟)}) ↔ 𝑈 = (𝐵 ∖ { 0 })))
13		df-drng 20676	. 2 ⊢ DivRing = {𝑟 ∈ Ring ∣ (Unit‘𝑟) = ((Base‘𝑟) ∖ {(0g‘𝑟)})}
14	12, 13	elrab2 3651	1 ⊢ (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧ 𝑈 = (𝐵 ∖ { 0 })))

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114   ∖ cdif 3900  {csn 4582  ‘cfv 6500  Basecbs 17148  0_gc0g 17371  Ringcrg 20180  Unitcui 20303  DivRingcdr 20674

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-drng 20676

This theorem is referenced by:  drngunit  20679  drngui  20680  drngring  20681  isdrng2  20688  drngprop  20689  drngid  20691  drngdomn  20694  opprdrng  20709  drngpropd  20714  fidomndrng  20718  issubdrg  20725  imadrhmcl  20742  cntzsdrg  20747  zringndrg  21435  istdrg2  24134  cvsunit  25099  cphreccllem  25146  isdrng4  33388  sradrng  33758  assafld  33814  zrhunitpreima  34153  aks5lem7  42564