Theorem isdrng 18751

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 6191	. . . 4 ⊢ (𝑟 = 𝑅 → (Unit‘𝑟) = (Unit‘𝑅))
2		isdrng.u	. . . 4 ⊢ 𝑈 = (Unit‘𝑅)
3	1, 2	syl6eqr 2674	. . 3 ⊢ (𝑟 = 𝑅 → (Unit‘𝑟) = 𝑈)
4		fveq2 6191	. . . . 5 ⊢ (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅))
5		isdrng.b	. . . . 5 ⊢ 𝐵 = (Base‘𝑅)
6	4, 5	syl6eqr 2674	. . . 4 ⊢ (𝑟 = 𝑅 → (Base‘𝑟) = 𝐵)
7		fveq2 6191	. . . . . 6 ⊢ (𝑟 = 𝑅 → (0g‘𝑟) = (0g‘𝑅))
8		isdrng.z	. . . . . 6 ⊢ 0 = (0g‘𝑅)
9	7, 8	syl6eqr 2674	. . . . 5 ⊢ (𝑟 = 𝑅 → (0g‘𝑟) = 0 )
10	9	sneqd 4189	. . . 4 ⊢ (𝑟 = 𝑅 → {(0g‘𝑟)} = { 0 })
11	6, 10	difeq12d 3729	. . 3 ⊢ (𝑟 = 𝑅 → ((Base‘𝑟) ∖ {(0g‘𝑟)}) = (𝐵 ∖ { 0 }))
12	3, 11	eqeq12d 2637	. 2 ⊢ (𝑟 = 𝑅 → ((Unit‘𝑟) = ((Base‘𝑟) ∖ {(0g‘𝑟)}) ↔ 𝑈 = (𝐵 ∖ { 0 })))
13		df-drng 18749	. 2 ⊢ DivRing = {𝑟 ∈ Ring ∣ (Unit‘𝑟) = ((Base‘𝑟) ∖ {(0g‘𝑟)})}
14	12, 13	elrab2 3366	1 ⊢ (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧ 𝑈 = (𝐵 ∖ { 0 })))

Syntax hints:   ↔ wb 196   ∧ wa 384   = wceq 1483   ∈ wcel 1990   ∖ cdif 3571  {csn 4177  ‘cfv 5888  Basecbs 15857  0_gc0g 16100  Ringcrg 18547  Unitcui 18639  DivRingcdr 18747

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-drng 18749

This theorem is referenced by:  drngunit  18752  drngui  18753  drngring  18754  isdrng2  18757  drngprop  18758  drngid  18761  opprdrng  18771  drngpropd  18774  issubdrg  18805  drngdomn  19303  fidomndrng  19307  zringndrg  19838  istdrg2  21981  cvsunit  22931  cphreccllem  22978  zrhunitpreima  30022  cntzsdrg  37772