# Metamath Proof Explorer

## Theorem rngoid

Description: The multiplication operation of a unital ring has (one or more) identity elements. (Contributed by Steve Rodriguez, 9-Sep-2007) (Revised by Mario Carneiro, 22-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses ringi.1 ${⊢}{G}={1}^{st}\left({R}\right)$
ringi.2 ${⊢}{H}={2}^{nd}\left({R}\right)$
ringi.3 ${⊢}{X}=\mathrm{ran}{G}$
Assertion rngoid ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\right)\to \exists {u}\in {X}\phantom{\rule{.4em}{0ex}}\left({u}{H}{A}={A}\wedge {A}{H}{u}={A}\right)$

### Proof

Step Hyp Ref Expression
1 ringi.1 ${⊢}{G}={1}^{st}\left({R}\right)$
2 ringi.2 ${⊢}{H}={2}^{nd}\left({R}\right)$
3 ringi.3 ${⊢}{X}=\mathrm{ran}{G}$
4 1 2 3 rngoi ${⊢}{R}\in \mathrm{RingOps}\to \left(\left({G}\in \mathrm{AbelOp}\wedge {H}:{X}×{X}⟶{X}\right)\wedge \left(\forall {u}\in {X}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({u}{H}{x}\right){H}{y}={u}{H}\left({x}{H}{y}\right)\wedge {u}{H}\left({x}{G}{y}\right)=\left({u}{H}{x}\right){G}\left({u}{H}{y}\right)\wedge \left({u}{G}{x}\right){H}{y}=\left({u}{H}{y}\right){G}\left({x}{H}{y}\right)\right)\wedge \exists {u}\in {X}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left({u}{H}{x}={x}\wedge {x}{H}{u}={x}\right)\right)\right)$
5 4 simprrd ${⊢}{R}\in \mathrm{RingOps}\to \exists {u}\in {X}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left({u}{H}{x}={x}\wedge {x}{H}{u}={x}\right)$
6 r19.12 ${⊢}\exists {u}\in {X}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left({u}{H}{x}={x}\wedge {x}{H}{u}={x}\right)\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {u}\in {X}\phantom{\rule{.4em}{0ex}}\left({u}{H}{x}={x}\wedge {x}{H}{u}={x}\right)$
7 5 6 syl ${⊢}{R}\in \mathrm{RingOps}\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {u}\in {X}\phantom{\rule{.4em}{0ex}}\left({u}{H}{x}={x}\wedge {x}{H}{u}={x}\right)$
8 oveq2 ${⊢}{x}={A}\to {u}{H}{x}={u}{H}{A}$
9 id ${⊢}{x}={A}\to {x}={A}$
10 8 9 eqeq12d ${⊢}{x}={A}\to \left({u}{H}{x}={x}↔{u}{H}{A}={A}\right)$
11 oveq1 ${⊢}{x}={A}\to {x}{H}{u}={A}{H}{u}$
12 11 9 eqeq12d ${⊢}{x}={A}\to \left({x}{H}{u}={x}↔{A}{H}{u}={A}\right)$
13 10 12 anbi12d ${⊢}{x}={A}\to \left(\left({u}{H}{x}={x}\wedge {x}{H}{u}={x}\right)↔\left({u}{H}{A}={A}\wedge {A}{H}{u}={A}\right)\right)$
14 13 rexbidv ${⊢}{x}={A}\to \left(\exists {u}\in {X}\phantom{\rule{.4em}{0ex}}\left({u}{H}{x}={x}\wedge {x}{H}{u}={x}\right)↔\exists {u}\in {X}\phantom{\rule{.4em}{0ex}}\left({u}{H}{A}={A}\wedge {A}{H}{u}={A}\right)\right)$
15 14 rspccva ${⊢}\left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {u}\in {X}\phantom{\rule{.4em}{0ex}}\left({u}{H}{x}={x}\wedge {x}{H}{u}={x}\right)\wedge {A}\in {X}\right)\to \exists {u}\in {X}\phantom{\rule{.4em}{0ex}}\left({u}{H}{A}={A}\wedge {A}{H}{u}={A}\right)$
16 7 15 sylan ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\right)\to \exists {u}\in {X}\phantom{\rule{.4em}{0ex}}\left({u}{H}{A}={A}\wedge {A}{H}{u}={A}\right)$