Theorem unitgrpid

Description: The identity of the group of units of a ring is the ring unity. (Contributed by Mario Carneiro, 2-Dec-2014)

	Ref	Expression
Hypotheses	unitmulcl.1	|- U = ( Unit ` R )
	unitgrp.2	|- G = ( ( mulGrp ` R ) |`s U )
	unitgrp.3	|- .1. = ( 1r ` R )
Assertion	unitgrpid	|- ( R e. Ring -> .1. = ( 0g ` G ) )

Proof

Step	Hyp	Ref	Expression
1		unitmulcl.1	|- U = ( Unit ` R )
2		unitgrp.2	|- G = ( ( mulGrp ` R ) |`s U )
3		unitgrp.3	|- .1. = ( 1r ` R )
4	1 3	1unit	|- ( R e. Ring -> .1. e. U )
5		eqid	|- ( Base ` R ) = ( Base ` R )
6	5 1	unitss	|- U C_ ( Base ` R )
7	2 5 3	ringidss	|- ( ( R e. Ring /\ U C_ ( Base ` R ) /\ .1. e. U ) -> .1. = ( 0g ` G ) )
8	6 7	mp3an2	|- ( ( R e. Ring /\ .1. e. U ) -> .1. = ( 0g ` G ) )
9	4 8	mpdan	|- ( R e. Ring -> .1. = ( 0g ` G ) )