Metamath Proof Explorer


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=UnitR
unitgrp.2 G=mulGrpR𝑠U
unitgrp.3 1˙=1R
Assertion unitgrpid RRing1˙=0G

Proof

Step Hyp Ref Expression
1 unitmulcl.1 U=UnitR
2 unitgrp.2 G=mulGrpR𝑠U
3 unitgrp.3 1˙=1R
4 1 3 1unit RRing1˙U
5 eqid BaseR=BaseR
6 5 1 unitss UBaseR
7 2 5 3 ringidss RRingUBaseR1˙U1˙=0G
8 6 7 mp3an2 RRing1˙U1˙=0G
9 4 8 mpdan RRing1˙=0G