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 | |
|
unitgrp.2 | |
||
unitgrp.3 | |
||
Assertion | unitgrpid | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | unitmulcl.1 | |
|
2 | unitgrp.2 | |
|
3 | unitgrp.3 | |
|
4 | 1 3 | 1unit | |
5 | eqid | |
|
6 | 5 1 | unitss | |
7 | 2 5 3 | ringidss | |
8 | 6 7 | mp3an2 | |
9 | 4 8 | mpdan | |