Proof of Theorem ringcinv
Step | Hyp | Ref
| Expression |
1 | | ringcsect.b |
. . 3
|
2 | | ringcinv.n |
. . 3
Inv |
3 | | ringcsect.u |
. . . 4
|
4 | | ringcsect.c |
. . . . 5
RingCat |
5 | 4 | ringccat 42024 |
. . . 4
|
6 | 3, 5 | syl 17 |
. . 3
|
7 | | ringcsect.x |
. . 3
|
8 | | ringcsect.y |
. . 3
|
9 | | eqid 2622 |
. . 3
Sect Sect |
10 | 1, 2, 6, 7, 8, 9 | isinv 16420 |
. 2
Sect Sect |
11 | | eqid 2622 |
. . . . . 6
|
12 | 4, 1, 3, 7, 8, 11,
9 | ringcsect 42031 |
. . . . 5
Sect
RingHom
RingHom
|
13 | | df-3an 1039 |
. . . . 5
RingHom RingHom
RingHom RingHom
|
14 | 12, 13 | syl6bb 276 |
. . . 4
Sect
RingHom RingHom
|
15 | | eqid 2622 |
. . . . . 6
|
16 | 4, 1, 3, 8, 7, 15,
9 | ringcsect 42031 |
. . . . 5
Sect
RingHom
RingHom
|
17 | | 3ancoma 1045 |
. . . . . 6
RingHom RingHom
RingHom
RingHom
|
18 | | df-3an 1039 |
. . . . . 6
RingHom RingHom
RingHom RingHom
|
19 | 17, 18 | bitri 264 |
. . . . 5
RingHom RingHom
RingHom RingHom
|
20 | 16, 19 | syl6bb 276 |
. . . 4
Sect
RingHom RingHom
|
21 | 14, 20 | anbi12d 747 |
. . 3
Sect Sect RingHom
RingHom
RingHom
RingHom
|
22 | | anandi 871 |
. . 3
RingHom
RingHom
RingHom
RingHom
RingHom RingHom
RingHom
RingHom RingHom RingHom
|
23 | 21, 22 | syl6bb 276 |
. 2
Sect Sect RingHom RingHom
RingHom
RingHom RingHom RingHom
|
24 | | simplrl 800 |
. . . . . 6
RingHom
RingHom
RingHom
RingHom RingHom RingHom
RingHom |
25 | 24 | adantl 482 |
. . . . 5
RingHom
RingHom
RingHom RingHom
RingHom
RingHom
RingHom |
26 | 11, 15 | rhmf 18726 |
. . . . . . . . . 10
RingHom
|
27 | 15, 11 | rhmf 18726 |
. . . . . . . . . 10
RingHom
|
28 | 26, 27 | anim12i 590 |
. . . . . . . . 9
RingHom RingHom
|
29 | 28 | ad2antlr 763 |
. . . . . . . 8
RingHom
RingHom
RingHom
RingHom RingHom RingHom
|
30 | | simpr 477 |
. . . . . . . . 9
RingHom
RingHom
|
31 | 30 | adantl 482 |
. . . . . . . 8
RingHom
RingHom
RingHom
RingHom RingHom RingHom
|
32 | | simpr 477 |
. . . . . . . . 9
RingHom RingHom
|
33 | 32 | ad2antrl 764 |
. . . . . . . 8
RingHom
RingHom
RingHom
RingHom RingHom RingHom
|
34 | 29, 31, 33 | jca32 558 |
. . . . . . 7
RingHom
RingHom
RingHom
RingHom RingHom RingHom
|
35 | 34 | adantl 482 |
. . . . . 6
RingHom
RingHom
RingHom RingHom
RingHom
RingHom
|
36 | | fcof1o 6551 |
. . . . . . 7
|
37 | | eqcom 2629 |
. . . . . . . 8
|
38 | 37 | anbi2i 730 |
. . . . . . 7
|
39 | 36, 38 | sylib 208 |
. . . . . 6
|
40 | 35, 39 | syl 17 |
. . . . 5
RingHom
RingHom
RingHom RingHom
RingHom
RingHom
|
41 | | anass 681 |
. . . . 5
RingHom
RingHom
|
42 | 25, 40, 41 | sylanbrc 698 |
. . . 4
RingHom
RingHom
RingHom RingHom
RingHom
RingHom
RingHom |
43 | 11, 15 | isrim 18733 |
. . . . . . 7
RingIso
RingHom
|
44 | 7, 8, 43 | syl2anc 693 |
. . . . . 6
RingIso
RingHom
|
45 | 44 | anbi1d 741 |
. . . . 5
RingIso
RingHom |
46 | 45 | adantr 481 |
. . . 4
RingHom
RingHom
RingHom RingHom
RingHom
RingHom
RingIso
RingHom |
47 | 42, 46 | mpbird 247 |
. . 3
RingHom
RingHom
RingHom RingHom
RingHom
RingHom
RingIso
|
48 | 11, 15 | rimrhm 18735 |
. . . . . 6
RingIso
RingHom |
49 | 48 | ad2antrl 764 |
. . . . 5
RingIso
RingHom |
50 | | isrim0 18723 |
. . . . . . . . . . 11
RingIso
RingHom
RingHom |
51 | 7, 8, 50 | syl2anc 693 |
. . . . . . . . . 10
RingIso
RingHom
RingHom |
52 | | eleq1 2689 |
. . . . . . . . . . . 12
RingHom
RingHom |
53 | 52 | eqcoms 2630 |
. . . . . . . . . . 11
RingHom
RingHom |
54 | 53 | anbi2d 740 |
. . . . . . . . . 10
RingHom
RingHom
RingHom
RingHom |
55 | 51, 54 | sylan9bbr 737 |
. . . . . . . . 9
RingIso RingHom
RingHom |
56 | | simpr 477 |
. . . . . . . . 9
RingHom RingHom
RingHom |
57 | 55, 56 | syl6bi 243 |
. . . . . . . 8
RingIso
RingHom |
58 | 57 | com12 32 |
. . . . . . 7
RingIso
RingHom
|
59 | 58 | expdimp 453 |
. . . . . 6
RingIso RingHom |
60 | 59 | impcom 446 |
. . . . 5
RingIso
RingHom |
61 | | coeq1 5279 |
. . . . . . 7
|
62 | 61 | ad2antll 765 |
. . . . . 6
RingIso
|
63 | 11, 15 | rimf1o 18734 |
. . . . . . . 8
RingIso
|
64 | 63 | ad2antrl 764 |
. . . . . . 7
RingIso
|
65 | | f1ococnv1 6165 |
. . . . . . 7
|
66 | 64, 65 | syl 17 |
. . . . . 6
RingIso
|
67 | 62, 66 | eqtrd 2656 |
. . . . 5
RingIso
|
68 | 49, 60, 67 | jca31 557 |
. . . 4
RingIso
RingHom
RingHom
|
69 | 51 | biimpcd 239 |
. . . . . . 7
RingIso
RingHom
RingHom |
70 | 69 | adantr 481 |
. . . . . 6
RingIso RingHom
RingHom |
71 | 70 | impcom 446 |
. . . . 5
RingIso
RingHom
RingHom |
72 | | eleq1 2689 |
. . . . . . 7
RingHom
RingHom
|
73 | 72 | ad2antll 765 |
. . . . . 6
RingIso
RingHom
RingHom
|
74 | 73 | anbi2d 740 |
. . . . 5
RingIso
RingHom
RingHom
RingHom
RingHom |
75 | 71, 74 | mpbird 247 |
. . . 4
RingIso
RingHom RingHom
|
76 | | coeq2 5280 |
. . . . . . 7
|
77 | 76 | ad2antll 765 |
. . . . . 6
RingIso
|
78 | | f1ococnv2 6163 |
. . . . . . 7
|
79 | 64, 78 | syl 17 |
. . . . . 6
RingIso
|
80 | 77, 79 | eqtrd 2656 |
. . . . 5
RingIso
|
81 | 75, 67, 80 | jca31 557 |
. . . 4
RingIso
RingHom
RingHom
|
82 | 68, 75, 81 | jca31 557 |
. . 3
RingIso
RingHom RingHom
RingHom
RingHom RingHom RingHom
|
83 | 47, 82 | impbida 877 |
. 2
RingHom RingHom
RingHom
RingHom RingHom RingHom
RingIso
|
84 | 10, 23, 83 | 3bitrd 294 |
1
RingIso |