Metamath Proof Explorer

Theorem rngoideu

Description: The unity 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=1st⁡R
ringi.2 ⊢H=2nd⁡R
ringi.3 ⊢X=ran⁡G
Assertion rngoideu ⊢R∈RingOps→∃!u∈X∀x∈XuHx=x∧xHu=x

Proof

Step Hyp Ref Expression
1 ringi.1 ⊢G=1st⁡R
2 ringi.2 ⊢H=2nd⁡R
3 ringi.3 ⊢X=ran⁡G
4 1 2 3 rngoi ⊢R∈RingOps→G∈AbelOp∧H:X×X⟶X∧∀u∈X∀x∈X∀y∈XuHxHy=uHxHy∧uHxGy=uHxGuHy∧uGxHy=uHyGxHy∧∃u∈X∀x∈XuHx=x∧xHu=x
5 4 simprrd ⊢R∈RingOps→∃u∈X∀x∈XuHx=x∧xHu=x
6 simpl ⊢uHx=x∧xHu=x→uHx=x
7 6 ralimi ⊢∀x∈XuHx=x∧xHu=x→∀x∈XuHx=x
8 oveq2 ⊢x=y→uHx=uHy
9 id ⊢x=y→x=y
10 8 9 eqeq12d ⊢x=y→uHx=x↔uHy=y
11 10 rspcv ⊢y∈X→∀x∈XuHx=x→uHy=y
12 7 11 syl5 ⊢y∈X→∀x∈XuHx=x∧xHu=x→uHy=y
13 simpr ⊢yHx=x∧xHy=x→xHy=x
14 13 ralimi ⊢∀x∈XyHx=x∧xHy=x→∀x∈XxHy=x
15 oveq1 ⊢x=u→xHy=uHy
16 id ⊢x=u→x=u
17 15 16 eqeq12d ⊢x=u→xHy=x↔uHy=u
18 17 rspcv ⊢u∈X→∀x∈XxHy=x→uHy=u
19 14 18 syl5 ⊢u∈X→∀x∈XyHx=x∧xHy=x→uHy=u
20 12 19 im2anan9r ⊢u∈X∧y∈X→∀x∈XuHx=x∧xHu=x∧∀x∈XyHx=x∧xHy=x→uHy=y∧uHy=u
21 eqtr2 ⊢uHy=y∧uHy=u→y=u
22 21 equcomd ⊢uHy=y∧uHy=u→u=y
23 20 22 syl6 ⊢u∈X∧y∈X→∀x∈XuHx=x∧xHu=x∧∀x∈XyHx=x∧xHy=x→u=y
24 23 rgen2 ⊢∀u∈X∀y∈X∀x∈XuHx=x∧xHu=x∧∀x∈XyHx=x∧xHy=x→u=y
25 oveq1 ⊢u=y→uHx=yHx
26 25 eqeq1d ⊢u=y→uHx=x↔yHx=x
27 26 ovanraleqv ⊢u=y→∀x∈XuHx=x∧xHu=x↔∀x∈XyHx=x∧xHy=x
28 27 reu4 ⊢∃!u∈X∀x∈XuHx=x∧xHu=x↔∃u∈X∀x∈XuHx=x∧xHu=x∧∀u∈X∀y∈X∀x∈XuHx=x∧xHu=x∧∀x∈XyHx=x∧xHy=x→u=y
29 5 24 28 sylanblrc ⊢R∈RingOps→∃!u∈X∀x∈XuHx=x∧xHu=x