# Metamath Proof Explorer

## Theorem rngo1cl

Description: The unit of a ring belongs to the base set. (Contributed by FL, 12-Feb-2010) (New usage is discouraged.)

Ref Expression
Hypotheses ring1cl.1 ${⊢}{X}=\mathrm{ran}{1}^{st}\left({R}\right)$
ring1cl.2 ${⊢}{H}={2}^{nd}\left({R}\right)$
ring1cl.3 ${⊢}{U}=\mathrm{GId}\left({H}\right)$
Assertion rngo1cl ${⊢}{R}\in \mathrm{RingOps}\to {U}\in {X}$

### Proof

Step Hyp Ref Expression
1 ring1cl.1 ${⊢}{X}=\mathrm{ran}{1}^{st}\left({R}\right)$
2 ring1cl.2 ${⊢}{H}={2}^{nd}\left({R}\right)$
3 ring1cl.3 ${⊢}{U}=\mathrm{GId}\left({H}\right)$
4 2 rngomndo ${⊢}{R}\in \mathrm{RingOps}\to {H}\in \mathrm{MndOp}$
5 2 eleq1i ${⊢}{H}\in \mathrm{MndOp}↔{2}^{nd}\left({R}\right)\in \mathrm{MndOp}$
6 mndoismgmOLD ${⊢}{2}^{nd}\left({R}\right)\in \mathrm{MndOp}\to {2}^{nd}\left({R}\right)\in \mathrm{Magma}$
7 mndoisexid ${⊢}{2}^{nd}\left({R}\right)\in \mathrm{MndOp}\to {2}^{nd}\left({R}\right)\in \mathrm{ExId}$
8 6 7 jca ${⊢}{2}^{nd}\left({R}\right)\in \mathrm{MndOp}\to \left({2}^{nd}\left({R}\right)\in \mathrm{Magma}\wedge {2}^{nd}\left({R}\right)\in \mathrm{ExId}\right)$
9 5 8 sylbi ${⊢}{H}\in \mathrm{MndOp}\to \left({2}^{nd}\left({R}\right)\in \mathrm{Magma}\wedge {2}^{nd}\left({R}\right)\in \mathrm{ExId}\right)$
10 4 9 syl ${⊢}{R}\in \mathrm{RingOps}\to \left({2}^{nd}\left({R}\right)\in \mathrm{Magma}\wedge {2}^{nd}\left({R}\right)\in \mathrm{ExId}\right)$
11 elin ${⊢}{2}^{nd}\left({R}\right)\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)↔\left({2}^{nd}\left({R}\right)\in \mathrm{Magma}\wedge {2}^{nd}\left({R}\right)\in \mathrm{ExId}\right)$
12 10 11 sylibr ${⊢}{R}\in \mathrm{RingOps}\to {2}^{nd}\left({R}\right)\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)$
13 eqid ${⊢}\mathrm{ran}{2}^{nd}\left({R}\right)=\mathrm{ran}{2}^{nd}\left({R}\right)$
14 2 fveq2i ${⊢}\mathrm{GId}\left({H}\right)=\mathrm{GId}\left({2}^{nd}\left({R}\right)\right)$
15 3 14 eqtri ${⊢}{U}=\mathrm{GId}\left({2}^{nd}\left({R}\right)\right)$
16 13 15 iorlid ${⊢}{2}^{nd}\left({R}\right)\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)\to {U}\in \mathrm{ran}{2}^{nd}\left({R}\right)$
17 12 16 syl ${⊢}{R}\in \mathrm{RingOps}\to {U}\in \mathrm{ran}{2}^{nd}\left({R}\right)$
18 eqid ${⊢}{2}^{nd}\left({R}\right)={2}^{nd}\left({R}\right)$
19 eqid ${⊢}{1}^{st}\left({R}\right)={1}^{st}\left({R}\right)$
20 18 19 rngorn1eq ${⊢}{R}\in \mathrm{RingOps}\to \mathrm{ran}{1}^{st}\left({R}\right)=\mathrm{ran}{2}^{nd}\left({R}\right)$
21 eqtr ${⊢}\left({X}=\mathrm{ran}{1}^{st}\left({R}\right)\wedge \mathrm{ran}{1}^{st}\left({R}\right)=\mathrm{ran}{2}^{nd}\left({R}\right)\right)\to {X}=\mathrm{ran}{2}^{nd}\left({R}\right)$
22 21 eleq2d ${⊢}\left({X}=\mathrm{ran}{1}^{st}\left({R}\right)\wedge \mathrm{ran}{1}^{st}\left({R}\right)=\mathrm{ran}{2}^{nd}\left({R}\right)\right)\to \left({U}\in {X}↔{U}\in \mathrm{ran}{2}^{nd}\left({R}\right)\right)$
23 1 20 22 sylancr ${⊢}{R}\in \mathrm{RingOps}\to \left({U}\in {X}↔{U}\in \mathrm{ran}{2}^{nd}\left({R}\right)\right)$
24 17 23 mpbird ${⊢}{R}\in \mathrm{RingOps}\to {U}\in {X}$