Theorem 1rrg

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

	Ref	Expression
Hypotheses	1rrg.1	|- .1. = ( 1r ` R )
	1rrg.e	|- E = ( RLReg ` R )
	1rrg.r	|- ( ph -> R e. Ring )
Assertion	1rrg	|- ( ph -> .1. e. E )

Proof

Step	Hyp	Ref	Expression
1		1rrg.1	|- .1. = ( 1r ` R )
2		1rrg.e	|- E = ( RLReg ` R )
3		1rrg.r	|- ( ph -> R e. Ring )
4		eqid	|- ( Unit ` R ) = ( Unit ` R )
5	2 4	unitrrg	|- ( R e. Ring -> ( Unit ` R ) C_ E )
6	4 1	1unit	|- ( R e. Ring -> .1. e. ( Unit ` R ) )
7	5 6	sseldd	|- ( R e. Ring -> .1. e. E )
8	3 7	syl	|- ( ph -> .1. e. E )