Theorem isdrng 18034

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 5892	. . . 4 |- ( r = R -> (Unit ` r ) = (Unit ` R ) )
2		isdrng.u	. . . 4 |- U = (Unit ` R )
3	1, 2	syl6eqr 2514	. . 3 |- ( r = R -> (Unit ` r ) = U )
4		fveq2 5892	. . . . 5 |- ( r = R -> ( Base ` r ) = ( Base ` R ) )
5		isdrng.b	. . . . 5 |- B = ( Base ` R )
6	4, 5	syl6eqr 2514	. . . 4 |- ( r = R -> ( Base ` r ) = B )
7		fveq2 5892	. . . . . 6 |- ( r = R -> ( 0g ` r ) = ( 0g ` R ) )
8		isdrng.z	. . . . . 6 |- .0. = ( 0g ` R )
9	7, 8	syl6eqr 2514	. . . . 5 |- ( r = R -> ( 0g ` r ) = .0. )
10	9	sneqd 3992	. . . 4 |- ( r = R -> { ( 0g ` r ) } = { .0. } )
11	6, 10	difeq12d 3564	. . 3 |- ( r = R -> ( ( Base ` r ) \ { ( 0g ` r ) } ) = ( B \ { .0. } ) )
12	3, 11	eqeq12d 2477	. 2 |- ( r = R -> ( (Unit ` r ) = ( ( Base ` r ) \ { ( 0g ` r ) } ) <-> U = ( B \ { .0. } ) ) )
13		df-drng 18032	. 2 |- DivRing = { r e. Ring | (Unit ` r ) = ( ( Base ` r ) \ { ( 0g ` r ) } ) }
14	12, 13	elrab2 3210	1 |- ( R e. DivRing <-> ( R e. Ring /\ U = ( B \ { .0. } ) ) )

Syntax hints:   <-> wb 189   /\ wa 375   = wceq 1455   e. wcel 1898   \ cdif 3413   {csn 3980   ` cfv 5605   Basecbs 15176   0gc0g 15393   Ringcrg 17835  Unitcui 17922   DivRingcdr 18030

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4419  df-iota 5569  df-fv 5613  df-drng 18032

This theorem is referenced by:  drngunit  18035  drngui  18036  drngring  18037  isdrng2  18040  drngprop  18041  drngid  18044  opprdrng  18054  drngpropd  18057  issubdrg  18088  drngdomn  18582  fidomndrng  18586  istdrg2  21247  cvsunit  22194  cphreccllem  22211  zrhunitpreima  28833  cntzsdrg  36114