Description: The identity of the multiplicative group is 1r . (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 ) ) |
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 ) ) |