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 ˙ = 1 R
1rrg.e ⊢ E = RLReg ⁡ R
1rrg.r ⊢ φ → R ∈ Ring
Assertion 1rrg ⊢ φ → 1 ˙ ∈ E

Proof

Step Hyp Ref Expression
1 1rrg.1 ⊢ 1 ˙ = 1 R
2 1rrg.e ⊢ E = RLReg ⁡ R
3 1rrg.r ⊢ φ → R ∈ Ring
4 eqid ⊢ Unit ⁡ R = Unit ⁡ R
5 2 4 unitrrg ⊢ R ∈ Ring → Unit ⁡ R ⊆ E
6 4 1 1unit ⊢ R ∈ Ring → 1 ˙ ∈ Unit ⁡ R
7 5 6 sseldd ⊢ R ∈ Ring → 1 ˙ ∈ E
8 3 7 syl ⊢ φ → 1 ˙ ∈ E