# Metamath Proof Explorer

## Theorem rngoidmlem

Description: The unit of a ring is an identity element for the multiplication. (Contributed by FL, 18-Feb-2010) (New usage is discouraged.)

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

### Proof

Step Hyp Ref Expression
1 uridm.1 ${⊢}{H}={2}^{nd}\left({R}\right)$
2 uridm.2 ${⊢}{X}=\mathrm{ran}{1}^{st}\left({R}\right)$
3 uridm.3 ${⊢}{U}=\mathrm{GId}\left({H}\right)$
4 1 rngomndo ${⊢}{R}\in \mathrm{RingOps}\to {H}\in \mathrm{MndOp}$
5 mndomgmid ${⊢}{H}\in \mathrm{MndOp}\to {H}\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)$
6 eqid ${⊢}\mathrm{ran}{H}=\mathrm{ran}{H}$
7 6 3 cmpidelt ${⊢}\left({H}\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)\wedge {A}\in \mathrm{ran}{H}\right)\to \left({U}{H}{A}={A}\wedge {A}{H}{U}={A}\right)$
8 7 ex ${⊢}{H}\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)\to \left({A}\in \mathrm{ran}{H}\to \left({U}{H}{A}={A}\wedge {A}{H}{U}={A}\right)\right)$
9 4 5 8 3syl ${⊢}{R}\in \mathrm{RingOps}\to \left({A}\in \mathrm{ran}{H}\to \left({U}{H}{A}={A}\wedge {A}{H}{U}={A}\right)\right)$
10 eqid ${⊢}{1}^{st}\left({R}\right)={1}^{st}\left({R}\right)$
11 1 10 rngorn1eq ${⊢}{R}\in \mathrm{RingOps}\to \mathrm{ran}{1}^{st}\left({R}\right)=\mathrm{ran}{H}$
12 eqtr ${⊢}\left({X}=\mathrm{ran}{1}^{st}\left({R}\right)\wedge \mathrm{ran}{1}^{st}\left({R}\right)=\mathrm{ran}{H}\right)\to {X}=\mathrm{ran}{H}$
13 simpl ${⊢}\left({X}=\mathrm{ran}{H}\wedge {R}\in \mathrm{RingOps}\right)\to {X}=\mathrm{ran}{H}$
14 13 eleq2d ${⊢}\left({X}=\mathrm{ran}{H}\wedge {R}\in \mathrm{RingOps}\right)\to \left({A}\in {X}↔{A}\in \mathrm{ran}{H}\right)$
15 14 imbi1d ${⊢}\left({X}=\mathrm{ran}{H}\wedge {R}\in \mathrm{RingOps}\right)\to \left(\left({A}\in {X}\to \left({U}{H}{A}={A}\wedge {A}{H}{U}={A}\right)\right)↔\left({A}\in \mathrm{ran}{H}\to \left({U}{H}{A}={A}\wedge {A}{H}{U}={A}\right)\right)\right)$
16 15 ex ${⊢}{X}=\mathrm{ran}{H}\to \left({R}\in \mathrm{RingOps}\to \left(\left({A}\in {X}\to \left({U}{H}{A}={A}\wedge {A}{H}{U}={A}\right)\right)↔\left({A}\in \mathrm{ran}{H}\to \left({U}{H}{A}={A}\wedge {A}{H}{U}={A}\right)\right)\right)\right)$
17 12 16 syl ${⊢}\left({X}=\mathrm{ran}{1}^{st}\left({R}\right)\wedge \mathrm{ran}{1}^{st}\left({R}\right)=\mathrm{ran}{H}\right)\to \left({R}\in \mathrm{RingOps}\to \left(\left({A}\in {X}\to \left({U}{H}{A}={A}\wedge {A}{H}{U}={A}\right)\right)↔\left({A}\in \mathrm{ran}{H}\to \left({U}{H}{A}={A}\wedge {A}{H}{U}={A}\right)\right)\right)\right)$
18 2 17 mpan ${⊢}\mathrm{ran}{1}^{st}\left({R}\right)=\mathrm{ran}{H}\to \left({R}\in \mathrm{RingOps}\to \left(\left({A}\in {X}\to \left({U}{H}{A}={A}\wedge {A}{H}{U}={A}\right)\right)↔\left({A}\in \mathrm{ran}{H}\to \left({U}{H}{A}={A}\wedge {A}{H}{U}={A}\right)\right)\right)\right)$
19 11 18 mpcom ${⊢}{R}\in \mathrm{RingOps}\to \left(\left({A}\in {X}\to \left({U}{H}{A}={A}\wedge {A}{H}{U}={A}\right)\right)↔\left({A}\in \mathrm{ran}{H}\to \left({U}{H}{A}={A}\wedge {A}{H}{U}={A}\right)\right)\right)$
20 9 19 mpbird ${⊢}{R}\in \mathrm{RingOps}\to \left({A}\in {X}\to \left({U}{H}{A}={A}\wedge {A}{H}{U}={A}\right)\right)$
21 20 imp ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\right)\to \left({U}{H}{A}={A}\wedge {A}{H}{U}={A}\right)$