# Metamath Proof Explorer

## Theorem rngoideu

Description: The unit element of a ring is unique. (Contributed by NM, 4-Apr-2009) (Revised by Mario Carneiro, 21-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 rngoideu ${⊢}{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)$

### 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 simpl ${⊢}\left({u}{H}{x}={x}\wedge {x}{H}{u}={x}\right)\to {u}{H}{x}={x}$
7 6 ralimi ${⊢}\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}}{u}{H}{x}={x}$
8 oveq2 ${⊢}{x}={y}\to {u}{H}{x}={u}{H}{y}$
9 id ${⊢}{x}={y}\to {x}={y}$
10 8 9 eqeq12d ${⊢}{x}={y}\to \left({u}{H}{x}={x}↔{u}{H}{y}={y}\right)$
11 10 rspcv ${⊢}{y}\in {X}\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{u}{H}{x}={x}\to {u}{H}{y}={y}\right)$
12 7 11 syl5 ${⊢}{y}\in {X}\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left({u}{H}{x}={x}\wedge {x}{H}{u}={x}\right)\to {u}{H}{y}={y}\right)$
13 simpr ${⊢}\left({y}{H}{x}={x}\wedge {x}{H}{y}={x}\right)\to {x}{H}{y}={x}$
14 13 ralimi ${⊢}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{H}{x}={x}\wedge {x}{H}{y}={x}\right)\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{x}{H}{y}={x}$
15 oveq1 ${⊢}{x}={u}\to {x}{H}{y}={u}{H}{y}$
16 id ${⊢}{x}={u}\to {x}={u}$
17 15 16 eqeq12d ${⊢}{x}={u}\to \left({x}{H}{y}={x}↔{u}{H}{y}={u}\right)$
18 17 rspcv ${⊢}{u}\in {X}\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{x}{H}{y}={x}\to {u}{H}{y}={u}\right)$
19 14 18 syl5 ${⊢}{u}\in {X}\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{H}{x}={x}\wedge {x}{H}{y}={x}\right)\to {u}{H}{y}={u}\right)$
20 12 19 im2anan9r ${⊢}\left({u}\in {X}\wedge {y}\in {X}\right)\to \left(\left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left({u}{H}{x}={x}\wedge {x}{H}{u}={x}\right)\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{H}{x}={x}\wedge {x}{H}{y}={x}\right)\right)\to \left({u}{H}{y}={y}\wedge {u}{H}{y}={u}\right)\right)$
21 eqtr2 ${⊢}\left({u}{H}{y}={y}\wedge {u}{H}{y}={u}\right)\to {y}={u}$
22 21 equcomd ${⊢}\left({u}{H}{y}={y}\wedge {u}{H}{y}={u}\right)\to {u}={y}$
23 20 22 syl6 ${⊢}\left({u}\in {X}\wedge {y}\in {X}\right)\to \left(\left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left({u}{H}{x}={x}\wedge {x}{H}{u}={x}\right)\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{H}{x}={x}\wedge {x}{H}{y}={x}\right)\right)\to {u}={y}\right)$
24 23 rgen2 ${⊢}\forall {u}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left({u}{H}{x}={x}\wedge {x}{H}{u}={x}\right)\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{H}{x}={x}\wedge {x}{H}{y}={x}\right)\right)\to {u}={y}\right)$
25 oveq1 ${⊢}{u}={y}\to {u}{H}{x}={y}{H}{x}$
26 25 eqeq1d ${⊢}{u}={y}\to \left({u}{H}{x}={x}↔{y}{H}{x}={x}\right)$
27 26 ovanraleqv ${⊢}{u}={y}\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left({u}{H}{x}={x}\wedge {x}{H}{u}={x}\right)↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{H}{x}={x}\wedge {x}{H}{y}={x}\right)\right)$
28 27 reu4 ${⊢}\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)↔\left(\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)\wedge \forall {u}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left({u}{H}{x}={x}\wedge {x}{H}{u}={x}\right)\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{H}{x}={x}\wedge {x}{H}{y}={x}\right)\right)\to {u}={y}\right)\right)$
29 5 24 28 sylanblrc ${⊢}{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)$