Description: The zero ring is a terminal object in the category of nonunital rings. (Contributed by AV, 17-Apr-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | zrinitorngc.u | |
|
zrinitorngc.c | |
||
zrinitorngc.z | |
||
zrinitorngc.e | |
||
Assertion | zrtermorngc | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | zrinitorngc.u | |
|
2 | zrinitorngc.c | |
|
3 | zrinitorngc.z | |
|
4 | zrinitorngc.e | |
|
5 | eqid | |
|
6 | 2 5 1 | rngcbas | |
7 | 6 | eleq2d | |
8 | elin | |
|
9 | 8 | simprbi | |
10 | 7 9 | syl6bi | |
11 | 10 | imp | |
12 | 3 | adantr | |
13 | eqid | |
|
14 | eqid | |
|
15 | eqid | |
|
16 | 13 14 15 | c0rnghm | |
17 | 11 12 16 | syl2anc | |
18 | simpr | |
|
19 | 1 | adantr | |
20 | eqid | |
|
21 | simpr | |
|
22 | eldifi | |
|
23 | ringrng | |
|
24 | 3 22 23 | 3syl | |
25 | 4 24 | elind | |
26 | 25 6 | eleqtrrd | |
27 | 26 | adantr | |
28 | 2 5 19 20 21 27 | rngchom | |
29 | 28 | eqcomd | |
30 | 29 | eleq2d | |
31 | 30 | biimpa | |
32 | 28 | eleq2d | |
33 | eqid | |
|
34 | 13 33 | rnghmf | |
35 | 32 34 | syl6bi | |
36 | 35 | adantr | |
37 | ffn | |
|
38 | 37 | adantl | |
39 | fvex | |
|
40 | 39 15 | fnmpti | |
41 | 40 | a1i | |
42 | 33 14 | 0ringbas | |
43 | 3 42 | syl | |
44 | 43 | adantr | |
45 | 44 | feq3d | |
46 | fvconst | |
|
47 | 46 | ex | |
48 | 45 47 | syl6bi | |
49 | 48 | adantr | |
50 | 49 | imp31 | |
51 | eqidd | |
|
52 | eqidd | |
|
53 | id | |
|
54 | 39 | a1i | |
55 | 51 52 53 54 | fvmptd | |
56 | 55 | adantl | |
57 | 50 56 | eqtr4d | |
58 | 38 41 57 | eqfnfvd | |
59 | 58 | ex | |
60 | 36 59 | syld | |
61 | 60 | alrimiv | |
62 | 18 31 61 | 3jca | |
63 | 17 62 | mpdan | |
64 | eleq1 | |
|
65 | 64 | eqeu | |
66 | 63 65 | syl | |
67 | 66 | ralrimiva | |
68 | 2 | rngccat | |
69 | 1 68 | syl | |
70 | 5 20 69 26 | istermo | |
71 | 67 70 | mpbird | |