Theorem isdrng 17718

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 5848	. . . 4 |- ( r = R -> (Unit ` r ) = (Unit ` R ) )
2		isdrng.u	. . . 4 |- U = (Unit ` R )
3	1, 2	syl6eqr 2461	. . 3 |- ( r = R -> (Unit ` r ) = U )
4		fveq2 5848	. . . . 5 |- ( r = R -> ( Base ` r ) = ( Base ` R ) )
5		isdrng.b	. . . . 5 |- B = ( Base ` R )
6	4, 5	syl6eqr 2461	. . . 4 |- ( r = R -> ( Base ` r ) = B )
7		fveq2 5848	. . . . . 6 |- ( r = R -> ( 0g ` r ) = ( 0g ` R ) )
8		isdrng.z	. . . . . 6 |- .0. = ( 0g ` R )
9	7, 8	syl6eqr 2461	. . . . 5 |- ( r = R -> ( 0g ` r ) = .0. )
10	9	sneqd 3983	. . . 4 |- ( r = R -> { ( 0g ` r ) } = { .0. } )
11	6, 10	difeq12d 3561	. . 3 |- ( r = R -> ( ( Base ` r ) \ { ( 0g ` r ) } ) = ( B \ { .0. } ) )
12	3, 11	eqeq12d 2424	. 2 |- ( r = R -> ( (Unit ` r ) = ( ( Base ` r ) \ { ( 0g ` r ) } ) <-> U = ( B \ { .0. } ) ) )
13		df-drng 17716	. 2 |- DivRing = { r e. Ring | (Unit ` r ) = ( ( Base ` r ) \ { ( 0g ` r ) } ) }
14	12, 13	elrab2 3208	1 |- ( R e. DivRing <-> ( R e. Ring /\ U = ( B \ { .0. } ) ) )

Syntax hints:   <-> wb 184   /\ wa 367   = wceq 1405   e. wcel 1842   \ cdif 3410   {csn 3971   ` cfv 5568   Basecbs 14839   0gc0g 15052   Ringcrg 17516  Unitcui 17606   DivRingcdr 17714

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ral 2758  df-rex 2759  df-rab 2762  df-v 3060  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-sn 3972  df-pr 3974  df-op 3978  df-uni 4191  df-br 4395  df-iota 5532  df-fv 5576  df-drng 17716

This theorem is referenced by:  drngunit  17719  drngui  17720  drngring  17721  isdrng2  17724  drngprop  17725  drngid  17728  opprdrng  17738  drngpropd  17741  issubdrg  17772  drngdomn  18270  fidomndrng  18274  istdrg2  20970  cvsunit  21898  cphreccllem  21915  zrhunitpreima  28397  cntzsdrg  35495