Theorem isdrng 20900

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ 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:  drngunit  20901  drngui  20902  drngring  20903  isdrng4  20908  isdrng2  20912  drngprop  20913  drngid  20915  drngdomn  20918  opprdrng  20936  drngpropd  20942  fidomndrng  20946  issubdrg  20952  imadrhmcl  20969  cntzsdrg  20974  zringndrg  21687  istdrg2  24410  cvsunit  25365  cphreccllem  25412  sradrng  34100  assafld  34155  zrhunitpreima  34494  aks5lem7  43074