This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isdrng

Description: The predicate "is a division ring". (Contributed by NM, 18-Oct-2012) (Revised by Mario Carneiro, 2-Dec-2014)

Ref Expression
Hypotheses isdrng.b 
|- B = ( Base ` R )
isdrng.u 
|- U = ( Unit ` R )
isdrng.z 
|- .0. = ( 0g ` R )
Assertion isdrng 
|- ( R e. DivRing <-> ( R e. Ring /\ U = ( B \ { .0. } ) ) )

Proof

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