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 ) )