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 ‘ 𝑅 )
	1rrg.e	⊢ 𝐸 = ( RLReg ‘ 𝑅 )
	1rrg.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
Assertion	1rrg	⊢ ( 𝜑 → 1 ∈ 𝐸 )

Proof

Step	Hyp	Ref	Expression
1		1rrg.1	⊢ 1 = ( 1r ‘ 𝑅 )
2		1rrg.e	⊢ 𝐸 = ( RLReg ‘ 𝑅 )
3		1rrg.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
4		eqid	⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
5	2 4	unitrrg	⊢ ( 𝑅 ∈ Ring → ( Unit ‘ 𝑅 ) ⊆ 𝐸 )
6	4 1	1unit	⊢ ( 𝑅 ∈ Ring → 1 ∈ ( Unit ‘ 𝑅 ) )
7	5 6	sseldd	⊢ ( 𝑅 ∈ Ring → 1 ∈ 𝐸 )
8	3 7	syl	⊢ ( 𝜑 → 1 ∈ 𝐸 )