Theorem isdrng 20701

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 6886	. . . 4 ⊢ (𝑟 = 𝑅 → (Unit‘𝑟) = (Unit‘𝑅))
2		isdrng.u	. . . 4 ⊢ 𝑈 = (Unit‘𝑅)
3	1, 2	eqtr4di 2787	. . 3 ⊢ (𝑟 = 𝑅 → (Unit‘𝑟) = 𝑈)
4		fveq2 6886	. . . . 5 ⊢ (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅))
5		isdrng.b	. . . . 5 ⊢ 𝐵 = (Base‘𝑅)
6	4, 5	eqtr4di 2787	. . . 4 ⊢ (𝑟 = 𝑅 → (Base‘𝑟) = 𝐵)
7		fveq2 6886	. . . . . 6 ⊢ (𝑟 = 𝑅 → (0g‘𝑟) = (0g‘𝑅))
8		isdrng.z	. . . . . 6 ⊢ 0 = (0g‘𝑅)
9	7, 8	eqtr4di 2787	. . . . 5 ⊢ (𝑟 = 𝑅 → (0g‘𝑟) = 0 )
10	9	sneqd 4618	. . . 4 ⊢ (𝑟 = 𝑅 → {(0g‘𝑟)} = { 0 })
11	6, 10	difeq12d 4107	. . 3 ⊢ (𝑟 = 𝑅 → ((Base‘𝑟) ∖ {(0g‘𝑟)}) = (𝐵 ∖ { 0 }))
12	3, 11	eqeq12d 2750	. 2 ⊢ (𝑟 = 𝑅 → ((Unit‘𝑟) = ((Base‘𝑟) ∖ {(0g‘𝑟)}) ↔ 𝑈 = (𝐵 ∖ { 0 })))
13		df-drng 20699	. 2 ⊢ DivRing = {𝑟 ∈ Ring ∣ (Unit‘𝑟) = ((Base‘𝑟) ∖ {(0g‘𝑟)})}
14	12, 13	elrab2 3678	1 ⊢ (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧ 𝑈 = (𝐵 ∖ { 0 })))

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1539   ∈ wcel 2107   ∖ cdif 3928  {csn 4606  ‘cfv 6541  Basecbs 17229  0_gc0g 17455  Ringcrg 20198  Unitcui 20323  DivRingcdr 20697

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rab 3420  df-v 3465  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 4888  df-br 5124  df-iota 6494  df-fv 6549  df-drng 20699

This theorem is referenced by:  drngunit  20702  drngui  20703  drngring  20704  isdrng2  20711  drngprop  20712  drngid  20714  drngdomn  20717  opprdrng  20732  drngpropd  20737  fidomndrng  20742  issubdrg  20749  imadrhmcl  20766  cntzsdrg  20771  zringndrg  21441  istdrg2  24132  cvsunit  25100  cphreccllem  25148  isdrng4  33237  sradrng  33568  assafld  33623  zrhunitpreima  33936  aks5lem7  42160