Theorem 1rrg

Description: The multiplicative identity is a left-regular element. (Contributed by Thierry Arnoux, 6-May-2025)

	Ref	Expression
Hypotheses	1rrg.1	$$⊢\underset{\dot{}}{1}=1_R$$
	1rrg.e	$$⊢E=\mathrm{RLReg}\left(R\right)$$
	1rrg.r	$$⊢\phi \to R\in \mathrm{Ring}$$
Assertion	1rrg	$$⊢\phi \to \underset{\dot{}}{1}\in E$$

Proof

Step	Hyp	Ref	Expression
1		1rrg.1	$$⊢\underset{\dot{}}{1}=1_R$$
2		1rrg.e	$$⊢E=\mathrm{RLReg}\left(R\right)$$
3		1rrg.r	$$⊢\phi \to R\in \mathrm{Ring}$$
4		eqid	$$⊢\mathrm{Unit}\left(R\right)=\mathrm{Unit}\left(R\right)$$
5	2 4	unitrrg	$$⊢R\in \mathrm{Ring}\to \mathrm{Unit}\left(R\right)\subseteq E$$
6	4 1	1unit	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}\in \mathrm{Unit}\left(R\right)$$
7	5 6	sseldd	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}\in E$$
8	3 7	syl	$$⊢\phi \to \underset{\dot{}}{1}\in E$$