Description: Deduce the unity element of a ring from its properties. (Contributed by Thierry Arnoux, 6-Sep-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ringurd.b | |
|
ringurd.p | |
||
ringurd.z | |
||
ringurd.i | |
||
ringurd.j | |
||
Assertion | ringurd | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ringurd.b | |
|
2 | ringurd.p | |
|
3 | ringurd.z | |
|
4 | ringurd.i | |
|
5 | ringurd.j | |
|
6 | eqid | |
|
7 | eqid | |
|
8 | eqid | |
|
9 | 6 7 8 | dfur2 | |
10 | 3 1 | eleqtrd | |
11 | 4 5 | jca | |
12 | 11 | ralrimiva | |
13 | 2 | adantr | |
14 | 13 | oveqd | |
15 | 14 | eqeq1d | |
16 | 13 | oveqd | |
17 | 16 | eqeq1d | |
18 | 15 17 | anbi12d | |
19 | 1 18 | raleqbidva | |
20 | 12 19 | mpbid | |
21 | 1 | eleq2d | |
22 | 13 | oveqd | |
23 | 22 | eqeq1d | |
24 | 13 | oveqd | |
25 | 24 | eqeq1d | |
26 | 23 25 | anbi12d | |
27 | 1 26 | raleqbidva | |
28 | 21 27 | anbi12d | |
29 | 4 | ralrimiva | |
30 | 29 | adantr | |
31 | simpr | |
|
32 | simpr | |
|
33 | 32 | oveq2d | |
34 | 33 32 | eqeq12d | |
35 | 31 34 | rspcdv | |
36 | 30 35 | mpd | |
37 | 36 | adantrr | |
38 | 3 | adantr | |
39 | simprr | |
|
40 | oveq2 | |
|
41 | id | |
|
42 | 40 41 | eqeq12d | |
43 | oveq1 | |
|
44 | 43 41 | eqeq12d | |
45 | 42 44 | anbi12d | |
46 | 45 | rspcva | |
47 | 46 | simprd | |
48 | 38 39 47 | syl2anc | |
49 | 37 48 | eqtr3d | |
50 | 49 | ex | |
51 | 28 50 | sylbird | |
52 | 51 | alrimiv | |
53 | eleq1 | |
|
54 | oveq1 | |
|
55 | 54 | eqeq1d | |
56 | 55 | ovanraleqv | |
57 | 53 56 | anbi12d | |
58 | 57 | eqeu | |
59 | 10 10 20 52 58 | syl121anc | |
60 | 57 | iota2 | |
61 | 3 59 60 | syl2anc | |
62 | 10 20 61 | mpbi2and | |
63 | 9 62 | eqtr2id | |