This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∈ 𝐸 )