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

Metamath Proof Explorer

Theorem drngid

Description: A division ring's unity is the identity element of its multiplicative group. (Contributed by NM, 7-Sep-2011)

Ref Expression
Hypotheses drngid.b 
|- B = ( Base ` R )
drngid.z 
|- .0. = ( 0g ` R )
drngid.u 
|- .1. = ( 1r ` R )
drngid.g 
|- G = ( ( mulGrp ` R ) |`s ( B \ { .0. } ) )
Assertion drngid 
|- ( R e. DivRing -> .1. = ( 0g ` G ) )

Proof

Step Hyp Ref Expression
1 drngid.b 
 |-  B = ( Base ` R )
2 drngid.z 
 |-  .0. = ( 0g ` R )
3 drngid.u 
 |-  .1. = ( 1r ` R )
4 drngid.g 
 |-  G = ( ( mulGrp ` R ) |`s ( B \ { .0. } ) )
5 drngring 
 |-  ( R e. DivRing -> R e. Ring )
6 eqid 
 |-  ( Unit ` R ) = ( Unit ` R )
7 eqid 
 |-  ( ( mulGrp ` R ) |`s ( Unit ` R ) ) = ( ( mulGrp ` R ) |`s ( Unit ` R ) )
8 6 7 3 unitgrpid 
 |-  ( R e. Ring -> .1. = ( 0g ` ( ( mulGrp ` R ) |`s ( Unit ` R ) ) ) )
9 5 8 syl 
 |-  ( R e. DivRing -> .1. = ( 0g ` ( ( mulGrp ` R ) |`s ( Unit ` R ) ) ) )
10 1 6 2 isdrng 
 |-  ( R e. DivRing <-> ( R e. Ring /\ ( Unit ` R ) = ( B \ { .0. } ) ) )
11 10 simprbi 
 |-  ( R e. DivRing -> ( Unit ` R ) = ( B \ { .0. } ) )
12 11 oveq2d 
 |-  ( R e. DivRing -> ( ( mulGrp ` R ) |`s ( Unit ` R ) ) = ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) )
13 12 4 eqtr4di 
 |-  ( R e. DivRing -> ( ( mulGrp ` R ) |`s ( Unit ` R ) ) = G )
14 13 fveq2d 
 |-  ( R e. DivRing -> ( 0g ` ( ( mulGrp ` R ) |`s ( Unit ` R ) ) ) = ( 0g ` G ) )
15 9 14 eqtrd 
 |-  ( R e. DivRing -> .1. = ( 0g ` G ) )