Metamath Proof Explorer


Theorem ringurd

Description: Deduce the unity element of a ring from its properties. (Contributed by Thierry Arnoux, 6-Sep-2016)

Ref Expression
Hypotheses ringurd.b φB=BaseR
ringurd.p φ·˙=R
ringurd.z φ1˙B
ringurd.i φxB1˙·˙x=x
ringurd.j φxBx·˙1˙=x
Assertion ringurd φ1˙=1R

Proof

Step Hyp Ref Expression
1 ringurd.b φB=BaseR
2 ringurd.p φ·˙=R
3 ringurd.z φ1˙B
4 ringurd.i φxB1˙·˙x=x
5 ringurd.j φxBx·˙1˙=x
6 eqid BaseR=BaseR
7 eqid R=R
8 eqid 1R=1R
9 6 7 8 dfur2 1R=ιe|eBaseRxBaseReRx=xxRe=x
10 3 1 eleqtrd φ1˙BaseR
11 4 5 jca φxB1˙·˙x=xx·˙1˙=x
12 11 ralrimiva φxB1˙·˙x=xx·˙1˙=x
13 2 adantr φxB·˙=R
14 13 oveqd φxB1˙·˙x=1˙Rx
15 14 eqeq1d φxB1˙·˙x=x1˙Rx=x
16 13 oveqd φxBx·˙1˙=xR1˙
17 16 eqeq1d φxBx·˙1˙=xxR1˙=x
18 15 17 anbi12d φxB1˙·˙x=xx·˙1˙=x1˙Rx=xxR1˙=x
19 1 18 raleqbidva φxB1˙·˙x=xx·˙1˙=xxBaseR1˙Rx=xxR1˙=x
20 12 19 mpbid φxBaseR1˙Rx=xxR1˙=x
21 1 eleq2d φeBeBaseR
22 13 oveqd φxBe·˙x=eRx
23 22 eqeq1d φxBe·˙x=xeRx=x
24 13 oveqd φxBx·˙e=xRe
25 24 eqeq1d φxBx·˙e=xxRe=x
26 23 25 anbi12d φxBe·˙x=xx·˙e=xeRx=xxRe=x
27 1 26 raleqbidva φxBe·˙x=xx·˙e=xxBaseReRx=xxRe=x
28 21 27 anbi12d φeBxBe·˙x=xx·˙e=xeBaseRxBaseReRx=xxRe=x
29 4 ralrimiva φxB1˙·˙x=x
30 29 adantr φeBxB1˙·˙x=x
31 simpr φeBeB
32 simpr φeBx=ex=e
33 32 oveq2d φeBx=e1˙·˙x=1˙·˙e
34 33 32 eqeq12d φeBx=e1˙·˙x=x1˙·˙e=e
35 31 34 rspcdv φeBxB1˙·˙x=x1˙·˙e=e
36 30 35 mpd φeB1˙·˙e=e
37 36 adantrr φeBxBe·˙x=xx·˙e=x1˙·˙e=e
38 3 adantr φeBxBe·˙x=xx·˙e=x1˙B
39 simprr φeBxBe·˙x=xx·˙e=xxBe·˙x=xx·˙e=x
40 oveq2 x=1˙e·˙x=e·˙1˙
41 id x=1˙x=1˙
42 40 41 eqeq12d x=1˙e·˙x=xe·˙1˙=1˙
43 oveq1 x=1˙x·˙e=1˙·˙e
44 43 41 eqeq12d x=1˙x·˙e=x1˙·˙e=1˙
45 42 44 anbi12d x=1˙e·˙x=xx·˙e=xe·˙1˙=1˙1˙·˙e=1˙
46 45 rspcva 1˙BxBe·˙x=xx·˙e=xe·˙1˙=1˙1˙·˙e=1˙
47 46 simprd 1˙BxBe·˙x=xx·˙e=x1˙·˙e=1˙
48 38 39 47 syl2anc φeBxBe·˙x=xx·˙e=x1˙·˙e=1˙
49 37 48 eqtr3d φeBxBe·˙x=xx·˙e=xe=1˙
50 49 ex φeBxBe·˙x=xx·˙e=xe=1˙
51 28 50 sylbird φeBaseRxBaseReRx=xxRe=xe=1˙
52 51 alrimiv φeeBaseRxBaseReRx=xxRe=xe=1˙
53 eleq1 e=1˙eBaseR1˙BaseR
54 oveq1 e=1˙eRx=1˙Rx
55 54 eqeq1d e=1˙eRx=x1˙Rx=x
56 55 ovanraleqv e=1˙xBaseReRx=xxRe=xxBaseR1˙Rx=xxR1˙=x
57 53 56 anbi12d e=1˙eBaseRxBaseReRx=xxRe=x1˙BaseRxBaseR1˙Rx=xxR1˙=x
58 57 eqeu 1˙BaseR1˙BaseRxBaseR1˙Rx=xxR1˙=xeeBaseRxBaseReRx=xxRe=xe=1˙∃!eeBaseRxBaseReRx=xxRe=x
59 10 10 20 52 58 syl121anc φ∃!eeBaseRxBaseReRx=xxRe=x
60 57 iota2 1˙B∃!eeBaseRxBaseReRx=xxRe=x1˙BaseRxBaseR1˙Rx=xxR1˙=xιe|eBaseRxBaseReRx=xxRe=x=1˙
61 3 59 60 syl2anc φ1˙BaseRxBaseR1˙Rx=xxR1˙=xιe|eBaseRxBaseReRx=xxRe=x=1˙
62 10 20 61 mpbi2and φιe|eBaseRxBaseReRx=xxRe=x=1˙
63 9 62 eqtr2id φ1˙=1R