Step | Hyp | Ref
| Expression |
1 | | ax-1 6 |
. 2
β’
((ZeroOβπΆ) =
β
β (π β
(ZeroOβπΆ) =
β
)) |
2 | | neq0 4310 |
. . 3
β’ (Β¬
(ZeroOβπΆ) = β
β ββ β β (ZeroOβπΆ)) |
3 | | nzerooringczr.u |
. . . . . . . 8
β’ (π β π β π) |
4 | | nzerooringczr.c |
. . . . . . . . 9
β’ πΆ = (RingCatβπ) |
5 | 4 | ringccat 46396 |
. . . . . . . 8
β’ (π β π β πΆ β Cat) |
6 | 3, 5 | syl 17 |
. . . . . . 7
β’ (π β πΆ β Cat) |
7 | | iszeroi 17902 |
. . . . . . 7
β’ ((πΆ β Cat β§ β β (ZeroOβπΆ)) β (β β (BaseβπΆ) β§ (β β (InitOβπΆ) β§ β β (TermOβπΆ)))) |
8 | 6, 7 | sylan 581 |
. . . . . 6
β’ ((π β§ β β (ZeroOβπΆ)) β (β β (BaseβπΆ) β§ (β β (InitOβπΆ) β§ β β (TermOβπΆ)))) |
9 | | nzerooringczr.z |
. . . . . . . . 9
β’ (π β π β (Ring β
NzRing)) |
10 | | nzerooringczr.e |
. . . . . . . . 9
β’ (π β π β π) |
11 | 3, 4, 9, 10 | zrtermoringc 46442 |
. . . . . . . 8
β’ (π β π β (TermOβπΆ)) |
12 | | nzerooringczr.i |
. . . . . . . . . 10
β’ (π β β€ring
β π) |
13 | 3, 12, 4 | irinitoringc 46441 |
. . . . . . . . 9
β’ (π β β€ring
β (InitOβπΆ)) |
14 | 6 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ β β (InitOβπΆ)) β§ β€ring β
(InitOβπΆ)) β
πΆ β
Cat) |
15 | | simplr 768 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ β β (InitOβπΆ)) β§ β€ring β
(InitOβπΆ)) β
β β (InitOβπΆ)) |
16 | | simpr 486 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ β β (InitOβπΆ)) β§ β€ring β
(InitOβπΆ)) β
β€ring β (InitOβπΆ)) |
17 | 14, 15, 16 | initoeu1w 17905 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ β β (InitOβπΆ)) β§ β€ring β
(InitOβπΆ)) β
β(
βπ βπΆ)β€ring) |
18 | 6 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ β β (TermOβπΆ)) β§ π β (TermOβπΆ)) β πΆ β Cat) |
19 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ β β (TermOβπΆ)) β§ π β (TermOβπΆ)) β π β (TermOβπΆ)) |
20 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ β β (TermOβπΆ)) β§ π β (TermOβπΆ)) β β β (TermOβπΆ)) |
21 | 18, 19, 20 | termoeu1w 17912 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ β β (TermOβπΆ)) β§ π β (TermOβπΆ)) β π( βπ βπΆ)β) |
22 | | cictr 17695 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((πΆ β Cat β§ π( βπ
βπΆ)β β§ β( βπ βπΆ)β€ring) β
π(
βπ βπΆ)β€ring) |
23 | 6, 22 | syl3an1 1164 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π( βπ βπΆ)β β§ β( βπ βπΆ)β€ring) β
π(
βπ βπΆ)β€ring) |
24 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
(IsoβπΆ) =
(IsoβπΆ) |
25 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
(BaseβπΆ) =
(BaseβπΆ) |
26 | 9 | eldifad 3927 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β π β Ring) |
27 | 10, 26 | elind 4159 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β π β (π β© Ring)) |
28 | 4, 25, 3 | ringcbas 46383 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β (BaseβπΆ) = (π β© Ring)) |
29 | 27, 28 | eleqtrrd 2841 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β π β (BaseβπΆ)) |
30 | | zringring 20888 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’
β€ring β Ring |
31 | 30 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β β€ring
β Ring) |
32 | 12, 31 | elind 4159 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β β€ring
β (π β©
Ring)) |
33 | 32, 28 | eleqtrrd 2841 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β β€ring
β (BaseβπΆ)) |
34 | 24, 25, 6, 29, 33 | cic 17689 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β (π( βπ βπΆ)β€ring β
βπ π β (π(IsoβπΆ)β€ring))) |
35 | | n0 4311 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π(IsoβπΆ)β€ring) β β
β
βπ π β (π(IsoβπΆ)β€ring)) |
36 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (Hom
βπΆ) = (Hom
βπΆ) |
37 | 25, 36, 24, 6, 29, 33 | isohom 17666 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β (π(IsoβπΆ)β€ring) β (π(Hom βπΆ)β€ring)) |
38 | | ssn0 4365 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (((π(IsoβπΆ)β€ring) β (π(Hom βπΆ)β€ring) β§ (π(IsoβπΆ)β€ring) β β
)
β (π(Hom βπΆ)β€ring) β
β
) |
39 | 4, 25, 3, 36, 29, 33 | ringchom 46385 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π β (π(Hom βπΆ)β€ring) = (π RingHom
β€ring)) |
40 | 39 | neeq1d 3004 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π β ((π(Hom βπΆ)β€ring) β β
β
(π RingHom
β€ring) β β
)) |
41 | | zringnzr 20897 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’
β€ring β NzRing |
42 | | nrhmzr 46245 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ((π β (Ring β NzRing)
β§ β€ring β NzRing) β (π RingHom β€ring) =
β
) |
43 | 9, 41, 42 | sylancl 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π β (π RingHom β€ring) =
β
) |
44 | | eqneqall 2955 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((π RingHom β€ring)
= β
β ((π
RingHom β€ring) β β
β (ZeroOβπΆ) = β
)) |
45 | 43, 44 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π β ((π RingHom β€ring) β
β
β (ZeroOβπΆ) = β
)) |
46 | 40, 45 | sylbid 239 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π β ((π(Hom βπΆ)β€ring) β β
β
(ZeroOβπΆ) =
β
)) |
47 | 38, 46 | syl5com 31 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((π(IsoβπΆ)β€ring) β (π(Hom βπΆ)β€ring) β§ (π(IsoβπΆ)β€ring) β β
)
β (π β
(ZeroOβπΆ) =
β
)) |
48 | 47 | expcom 415 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π(IsoβπΆ)β€ring) β β
β
((π(IsoβπΆ)β€ring) β
(π(Hom βπΆ)β€ring) β
(π β (ZeroOβπΆ) = β
))) |
49 | 48 | com13 88 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β ((π(IsoβπΆ)β€ring) β (π(Hom βπΆ)β€ring) β ((π(IsoβπΆ)β€ring) β β
β
(ZeroOβπΆ) =
β
))) |
50 | 37, 49 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β ((π(IsoβπΆ)β€ring) β β
β
(ZeroOβπΆ) =
β
)) |
51 | 35, 50 | biimtrrid 242 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β (βπ π β (π(IsoβπΆ)β€ring) β
(ZeroOβπΆ) =
β
)) |
52 | 34, 51 | sylbid 239 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β (π( βπ βπΆ)β€ring β
(ZeroOβπΆ) =
β
)) |
53 | 52 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π( βπ βπΆ)β β§ β( βπ βπΆ)β€ring) β
(π(
βπ βπΆ)β€ring β
(ZeroOβπΆ) =
β
)) |
54 | 23, 53 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π( βπ βπΆ)β β§ β( βπ βπΆ)β€ring) β
(ZeroOβπΆ) =
β
) |
55 | 54 | 3exp 1120 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (π( βπ βπΆ)β β (β( βπ βπΆ)β€ring β
(ZeroOβπΆ) =
β
))) |
56 | 55 | a1dd 50 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (π( βπ βπΆ)β β (β β (BaseβπΆ) β (β( βπ βπΆ)β€ring β
(ZeroOβπΆ) =
β
)))) |
57 | 56 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ β β (TermOβπΆ)) β§ π β (TermOβπΆ)) β (π( βπ βπΆ)β β (β β (BaseβπΆ) β (β( βπ βπΆ)β€ring β
(ZeroOβπΆ) =
β
)))) |
58 | 21, 57 | mpd 15 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ β β (TermOβπΆ)) β§ π β (TermOβπΆ)) β (β β (BaseβπΆ) β (β( βπ βπΆ)β€ring β
(ZeroOβπΆ) =
β
))) |
59 | 58 | exp31 421 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (β β (TermOβπΆ) β (π β (TermOβπΆ) β (β β (BaseβπΆ) β (β( βπ βπΆ)β€ring β
(ZeroOβπΆ) =
β
))))) |
60 | 59 | com34 91 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (β β (TermOβπΆ) β (β β (BaseβπΆ) β (π β (TermOβπΆ) β (β( βπ βπΆ)β€ring β
(ZeroOβπΆ) =
β
))))) |
61 | 60 | com25 99 |
. . . . . . . . . . . . . . . . 17
β’ (π β (β( βπ βπΆ)β€ring β
(β β (BaseβπΆ) β (π β (TermOβπΆ) β (β β (TermOβπΆ) β (ZeroOβπΆ) = β
))))) |
62 | 61 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ β β (InitOβπΆ)) β§ β€ring β
(InitOβπΆ)) β
(β(
βπ βπΆ)β€ring β (β β (BaseβπΆ) β (π β (TermOβπΆ) β (β β (TermOβπΆ) β (ZeroOβπΆ) = β
))))) |
63 | 17, 62 | mpd 15 |
. . . . . . . . . . . . . . 15
β’ (((π β§ β β (InitOβπΆ)) β§ β€ring β
(InitOβπΆ)) β
(β β (BaseβπΆ) β (π β (TermOβπΆ) β (β β (TermOβπΆ) β (ZeroOβπΆ) = β
)))) |
64 | 63 | ex 414 |
. . . . . . . . . . . . . 14
β’ ((π β§ β β (InitOβπΆ)) β (β€ring β
(InitOβπΆ) β
(β β (BaseβπΆ) β (π β (TermOβπΆ) β (β β (TermOβπΆ) β (ZeroOβπΆ) = β
))))) |
65 | 64 | com25 99 |
. . . . . . . . . . . . 13
β’ ((π β§ β β (InitOβπΆ)) β (β β (TermOβπΆ) β (β β (BaseβπΆ) β (π β (TermOβπΆ) β (β€ring β
(InitOβπΆ) β
(ZeroOβπΆ) =
β
))))) |
66 | 65 | expimpd 455 |
. . . . . . . . . . . 12
β’ (π β ((β β (InitOβπΆ) β§ β β (TermOβπΆ)) β (β β (BaseβπΆ) β (π β (TermOβπΆ) β (β€ring β
(InitOβπΆ) β
(ZeroOβπΆ) =
β
))))) |
67 | 66 | com23 86 |
. . . . . . . . . . 11
β’ (π β (β β (BaseβπΆ) β ((β β (InitOβπΆ) β§ β β (TermOβπΆ)) β (π β (TermOβπΆ) β (β€ring β
(InitOβπΆ) β
(ZeroOβπΆ) =
β
))))) |
68 | 67 | impd 412 |
. . . . . . . . . 10
β’ (π β ((β β (BaseβπΆ) β§ (β β (InitOβπΆ) β§ β β (TermOβπΆ))) β (π β (TermOβπΆ) β (β€ring β
(InitOβπΆ) β
(ZeroOβπΆ) =
β
)))) |
69 | 68 | com24 95 |
. . . . . . . . 9
β’ (π β (β€ring
β (InitOβπΆ)
β (π β
(TermOβπΆ) β
((β β (BaseβπΆ) β§ (β β (InitOβπΆ) β§ β β (TermOβπΆ))) β (ZeroOβπΆ) = β
)))) |
70 | 13, 69 | mpd 15 |
. . . . . . . 8
β’ (π β (π β (TermOβπΆ) β ((β β (BaseβπΆ) β§ (β β (InitOβπΆ) β§ β β (TermOβπΆ))) β (ZeroOβπΆ) = β
))) |
71 | 11, 70 | mpd 15 |
. . . . . . 7
β’ (π β ((β β (BaseβπΆ) β§ (β β (InitOβπΆ) β§ β β (TermOβπΆ))) β (ZeroOβπΆ) = β
)) |
72 | 71 | adantr 482 |
. . . . . 6
β’ ((π β§ β β (ZeroOβπΆ)) β ((β β (BaseβπΆ) β§ (β β (InitOβπΆ) β§ β β (TermOβπΆ))) β (ZeroOβπΆ) = β
)) |
73 | 8, 72 | mpd 15 |
. . . . 5
β’ ((π β§ β β (ZeroOβπΆ)) β (ZeroOβπΆ) = β
) |
74 | 73 | expcom 415 |
. . . 4
β’ (β β (ZeroOβπΆ) β (π β (ZeroOβπΆ) = β
)) |
75 | 74 | exlimiv 1934 |
. . 3
β’
(ββ β β (ZeroOβπΆ) β (π β (ZeroOβπΆ) = β
)) |
76 | 2, 75 | sylbi 216 |
. 2
β’ (Β¬
(ZeroOβπΆ) = β
β (π β
(ZeroOβπΆ) =
β
)) |
77 | 1, 76 | pm2.61i 182 |
1
β’ (π β (ZeroOβπΆ) = β
) |