Theorem unitgrpid

Description: The identity of the multiplicative group is 1r . (Contributed by Mario Carneiro, 2-Dec-2014)

	Ref	Expression
Hypotheses	unitmulcl.1	$$⊢U=\mathrm{Unit}\left(R\right)$$
	unitgrp.2	$$⊢G={\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U$$
	unitgrp.3	$$⊢\underset{\dot{}}{1}=1_R$$
Assertion	unitgrpid	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}=0_G$$

Proof

Step	Hyp	Ref	Expression
1		unitmulcl.1	$$⊢U=\mathrm{Unit}\left(R\right)$$
2		unitgrp.2	$$⊢G={\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U$$
3		unitgrp.3	$$⊢\underset{\dot{}}{1}=1_R$$
4	1 3	1unit	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}\in U$$
5		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
6	5 1	unitss	$$⊢U\subseteq {\mathrm{Base}}_R$$
7	2 5 3	ringidss	$$⊢\left(R\in \mathrm{Ring}\wedge U\subseteq {\mathrm{Base}}_R\wedge \underset{\dot{}}{1}\in U\right)\to \underset{\dot{}}{1}=0_G$$
8	6 7	mp3an2	$$⊢\left(R\in \mathrm{Ring}\wedge \underset{\dot{}}{1}\in U\right)\to \underset{\dot{}}{1}=0_G$$
9	4 8	mpdan	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}=0_G$$