Theorem isdrng 17176

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	|- B = ( Base ` R )
isdrng.u	|- U = (Unit ` R )
isdrng.z	|- .0. = ( 0g ` R )

Assertion

Ref	Expression
isdrng	|- ( R e. DivRing <-> ( R e. Ring /\ U = ( B \ { .0. } ) ) )

Proof of Theorem isdrng

Dummy variable r is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 5857	. . . 4 |- ( r = R -> (Unit ` r ) = (Unit ` R ) )
2		isdrng.u	. . . 4 |- U = (Unit ` R )
3	1, 2	syl6eqr 2519	. . 3 |- ( r = R -> (Unit ` r ) = U )
4		fveq2 5857	. . . . 5 |- ( r = R -> ( Base ` r ) = ( Base ` R ) )
5		isdrng.b	. . . . 5 |- B = ( Base ` R )
6	4, 5	syl6eqr 2519	. . . 4 |- ( r = R -> ( Base ` r ) = B )
7		fveq2 5857	. . . . . 6 |- ( r = R -> ( 0g ` r ) = ( 0g ` R ) )
8		isdrng.z	. . . . . 6 |- .0. = ( 0g ` R )
9	7, 8	syl6eqr 2519	. . . . 5 |- ( r = R -> ( 0g ` r ) = .0. )
10	9	sneqd 4032	. . . 4 |- ( r = R -> { ( 0g ` r ) } = { .0. } )
11	6, 10	difeq12d 3616	. . 3 |- ( r = R -> ( ( Base ` r ) \ { ( 0g ` r ) } ) = ( B \ { .0. } ) )
12	3, 11	eqeq12d 2482	. 2 |- ( r = R -> ( (Unit ` r ) = ( ( Base ` r ) \ { ( 0g ` r ) } ) <-> U = ( B \ { .0. } ) ) )
13		df-drng 17174	. 2 |- DivRing = { r e. Ring | (Unit ` r ) = ( ( Base ` r ) \ { ( 0g ` r ) } ) }
14	12, 13	elrab2 3256	1 |- ( R e. DivRing <-> ( R e. Ring /\ U = ( B \ { .0. } ) ) )

Syntax hints:   <-> wb 184   /\ wa 369   = wceq 1374   e. wcel 1762   \ cdif 3466   {csn 4020   ` cfv 5579   Basecbs 14479   0gc0g 14684   Ringcrg 16979  Unitcui 17065   DivRingcdr 17172

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-br 4441  df-iota 5542  df-fv 5587  df-drng 17174

This theorem is referenced by:  drngunit  17177  drngui  17178  drngrng  17179  isdrng2  17182  drngprop  17183  drngid  17186  opprdrng  17196  drngpropd  17199  issubdrg  17230  drngdomn  17716  fidomndrng  17720  istdrg2  20408  cvsunit  21336  cphreccllem  21353  zrhunitpreima  27581  cntzsdrg  30745