Step | Hyp | Ref
| Expression |
1 | | ax-1 6 |
. 2
ZeroO ZeroO |
2 | | neq0 3930 |
. . 3
ZeroO ZeroO |
3 | | nzerooringczr.u |
. . . . . . . 8
|
4 | | nzerooringczr.c |
. . . . . . . . 9
RingCat |
5 | 4 | ringccat 42024 |
. . . . . . . 8
|
6 | 3, 5 | syl 17 |
. . . . . . 7
|
7 | | iszeroi 16659 |
. . . . . . 7
ZeroO InitO TermO |
8 | 6, 7 | sylan 488 |
. . . . . 6
ZeroO
InitO
TermO |
9 | | nzerooringczr.z |
. . . . . . . . 9
NzRing |
10 | | nzerooringczr.e |
. . . . . . . . 9
|
11 | 3, 4, 9, 10 | zrtermoringc 42070 |
. . . . . . . 8
TermO |
12 | | nzerooringczr.i |
. . . . . . . . . 10
ℤring |
13 | 3, 12, 4 | irinitoringc 42069 |
. . . . . . . . 9
ℤring InitO |
14 | 6 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
InitO
ℤring InitO |
15 | | simplr 792 |
. . . . . . . . . . . . . . . . 17
InitO
ℤring InitO InitO |
16 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
InitO
ℤring InitO
ℤring InitO |
17 | 14, 15, 16 | initoeu1w 16662 |
. . . . . . . . . . . . . . . 16
InitO
ℤring InitO 𝑐 ℤring |
18 | 6 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . 22
TermO
TermO |
19 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . 22
TermO
TermO TermO |
20 | | simplr 792 |
. . . . . . . . . . . . . . . . . . . . . 22
TermO
TermO TermO |
21 | 18, 19, 20 | termoeu1w 16669 |
. . . . . . . . . . . . . . . . . . . . 21
TermO
TermO 𝑐 |
22 | | cictr 16465 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
𝑐
𝑐 ℤring
𝑐 ℤring |
23 | 6, 22 | syl3an1 1359 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
𝑐 𝑐
ℤring 𝑐 ℤring |
24 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
25 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
26 | 9 | eldifad 3586 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
27 | 10, 26 | elind 3798 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
28 | 4, 25, 3 | ringcbas 42011 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
29 | 27, 28 | eleqtrrd 2704 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
30 | | zringring 19821 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
ℤring |
31 | 30 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
ℤring |
32 | 12, 31 | elind 3798 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
ℤring |
33 | 32, 28 | eleqtrrd 2704 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
ℤring |
34 | 24, 25, 6, 29, 33 | cic 16459 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
𝑐 ℤring ℤring |
35 | | n0 3931 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
ℤring
ℤring |
36 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
37 | 25, 36, 24, 6, 29, 33 | isohom 16436 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
ℤring
ℤring |
38 | | ssn0 3976 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
ℤring
ℤring ℤring ℤring |
39 | 4, 25, 3, 36, 29, 33 | ringchom 42013 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
ℤring RingHom ℤring |
40 | 39 | neeq1d 2853 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
ℤring RingHom
ℤring
|
41 | | zringnzr 19830 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
ℤring NzRing |
42 | | nrhmzr 41873 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
NzRing
ℤring NzRing RingHom ℤring |
43 | 9, 41, 42 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
RingHom
ℤring
|
44 | | eqneqall 2805 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
RingHom ℤring
RingHom
ℤring
ZeroO |
45 | 43, 44 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
RingHom
ℤring
ZeroO |
46 | 40, 45 | sylbid 230 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
ℤring
ZeroO |
47 | 38, 46 | syl5com 31 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
ℤring
ℤring ℤring ZeroO |
48 | 47 | expcom 451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
ℤring ℤring
ℤring ZeroO |
49 | 48 | com13 88 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
ℤring ℤring
ℤring ZeroO |
50 | 37, 49 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
ℤring
ZeroO |
51 | 35, 50 | syl5bir 233 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
ℤring ZeroO |
52 | 34, 51 | sylbid 230 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
𝑐 ℤring ZeroO |
53 | 52 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
𝑐 𝑐
ℤring 𝑐 ℤring ZeroO |
54 | 23, 53 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . 24
𝑐 𝑐
ℤring ZeroO |
55 | 54 | 3exp 1264 |
. . . . . . . . . . . . . . . . . . . . . . 23
𝑐 𝑐
ℤring ZeroO |
56 | 55 | a1dd 50 |
. . . . . . . . . . . . . . . . . . . . . 22
𝑐 𝑐
ℤring ZeroO |
57 | 56 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . 21
TermO
TermO 𝑐 𝑐 ℤring ZeroO |
58 | 21, 57 | mpd 15 |
. . . . . . . . . . . . . . . . . . . 20
TermO
TermO
𝑐 ℤring ZeroO |
59 | 58 | exp31 630 |
. . . . . . . . . . . . . . . . . . 19
TermO
TermO
𝑐 ℤring ZeroO |
60 | 59 | com34 91 |
. . . . . . . . . . . . . . . . . 18
TermO
TermO
𝑐 ℤring ZeroO |
61 | 60 | com25 99 |
. . . . . . . . . . . . . . . . 17
𝑐 ℤring TermO TermO ZeroO |
62 | 61 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
InitO
ℤring InitO 𝑐
ℤring TermO TermO ZeroO |
63 | 17, 62 | mpd 15 |
. . . . . . . . . . . . . . 15
InitO
ℤring InitO
TermO
TermO ZeroO |
64 | 63 | ex 450 |
. . . . . . . . . . . . . 14
InitO ℤring InitO
TermO TermO ZeroO |
65 | 64 | com25 99 |
. . . . . . . . . . . . 13
InitO TermO TermO ℤring InitO ZeroO |
66 | 65 | expimpd 629 |
. . . . . . . . . . . 12
InitO
TermO TermO ℤring InitO ZeroO |
67 | 66 | com23 86 |
. . . . . . . . . . 11
InitO
TermO TermO ℤring InitO ZeroO |
68 | 67 | impd 447 |
. . . . . . . . . 10
InitO
TermO TermO ℤring InitO
ZeroO |
69 | 68 | com24 95 |
. . . . . . . . 9
ℤring InitO
TermO
InitO
TermO ZeroO |
70 | 13, 69 | mpd 15 |
. . . . . . . 8
TermO InitO TermO ZeroO |
71 | 11, 70 | mpd 15 |
. . . . . . 7
InitO
TermO ZeroO |
72 | 71 | adantr 481 |
. . . . . 6
ZeroO
InitO
TermO ZeroO |
73 | 8, 72 | mpd 15 |
. . . . 5
ZeroO ZeroO |
74 | 73 | expcom 451 |
. . . 4
ZeroO
ZeroO |
75 | 74 | exlimiv 1858 |
. . 3
ZeroO ZeroO |
76 | 2, 75 | sylbi 207 |
. 2
ZeroO
ZeroO |
77 | 1, 76 | pm2.61i 176 |
1
ZeroO |