Proof of Theorem ringcinvALTV
Step | Hyp | Ref
| Expression |
1 | | ringcsectALTV.b |
. . 3
|
2 | | ringcinvALTV.n |
. . 3
Inv |
3 | | ringcsectALTV.u |
. . . 4
|
4 | | ringcsectALTV.c |
. . . . 5
RingCatALTV |
5 | 4 | ringccatALTV 42053 |
. . . 4
|
6 | 3, 5 | syl 17 |
. . 3
|
7 | | ringcsectALTV.x |
. . 3
|
8 | | ringcsectALTV.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 | ringcsectALTV 42055 |
. . . . 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 | ringcsectALTV 42055 |
. . . . 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 |
. . . . . . . . . 10
RingHom
RingHom
|
31 | 30 | adantl 482 |
. . . . . . . . 9
RingHom
RingHom
RingHom
RingHom RingHom RingHom
|
32 | | simpr 477 |
. . . . . . . . . 10
RingHom RingHom
|
33 | 32 | ad2antrl 764 |
. . . . . . . . 9
RingHom
RingHom
RingHom
RingHom RingHom RingHom
|
34 | 31, 33 | jca 554 |
. . . . . . . 8
RingHom
RingHom
RingHom
RingHom RingHom RingHom
|
35 | 29, 34 | jca 554 |
. . . . . . 7
RingHom
RingHom
RingHom
RingHom RingHom RingHom
|
36 | 35 | adantl 482 |
. . . . . 6
RingHom
RingHom
RingHom RingHom
RingHom
RingHom
|
37 | | fcof1o 6551 |
. . . . . . 7
|
38 | | eqcom 2629 |
. . . . . . . 8
|
39 | 38 | anbi2i 730 |
. . . . . . 7
|
40 | 37, 39 | sylib 208 |
. . . . . 6
|
41 | 36, 40 | syl 17 |
. . . . 5
RingHom
RingHom
RingHom RingHom
RingHom
RingHom
|
42 | | anass 681 |
. . . . 5
RingHom
RingHom
|
43 | 25, 41, 42 | sylanbrc 698 |
. . . 4
RingHom
RingHom
RingHom RingHom
RingHom
RingHom
RingHom |
44 | 7, 8 | jca 554 |
. . . . . . 7
|
45 | 11, 15 | isrim 18733 |
. . . . . . 7
RingIso
RingHom
|
46 | 44, 45 | syl 17 |
. . . . . 6
RingIso
RingHom
|
47 | 46 | anbi1d 741 |
. . . . 5
RingIso
RingHom |
48 | 47 | adantr 481 |
. . . 4
RingHom
RingHom
RingHom RingHom
RingHom
RingHom
RingIso
RingHom |
49 | 43, 48 | mpbird 247 |
. . 3
RingHom
RingHom
RingHom RingHom
RingHom
RingHom
RingIso
|
50 | 11, 15 | rimrhm 18735 |
. . . . . 6
RingIso
RingHom |
51 | 50 | ad2antrl 764 |
. . . . 5
RingIso
RingHom |
52 | | isrim0 18723 |
. . . . . . . . . . 11
RingIso
RingHom
RingHom |
53 | 44, 52 | syl 17 |
. . . . . . . . . 10
RingIso
RingHom
RingHom |
54 | | eleq1 2689 |
. . . . . . . . . . . 12
RingHom
RingHom |
55 | 54 | eqcoms 2630 |
. . . . . . . . . . 11
RingHom
RingHom |
56 | 55 | anbi2d 740 |
. . . . . . . . . 10
RingHom
RingHom
RingHom
RingHom |
57 | 53, 56 | sylan9bbr 737 |
. . . . . . . . 9
RingIso RingHom
RingHom |
58 | | simpr 477 |
. . . . . . . . 9
RingHom RingHom
RingHom |
59 | 57, 58 | syl6bi 243 |
. . . . . . . 8
RingIso
RingHom |
60 | 59 | com12 32 |
. . . . . . 7
RingIso
RingHom
|
61 | 60 | expdimp 453 |
. . . . . 6
RingIso RingHom |
62 | 61 | impcom 446 |
. . . . 5
RingIso
RingHom |
63 | | coeq1 5279 |
. . . . . . 7
|
64 | 63 | ad2antll 765 |
. . . . . 6
RingIso
|
65 | 11, 15 | rimf1o 18734 |
. . . . . . . 8
RingIso
|
66 | 65 | ad2antrl 764 |
. . . . . . 7
RingIso
|
67 | | f1ococnv1 6165 |
. . . . . . 7
|
68 | 66, 67 | syl 17 |
. . . . . 6
RingIso
|
69 | 64, 68 | eqtrd 2656 |
. . . . 5
RingIso
|
70 | 51, 62, 69 | jca31 557 |
. . . 4
RingIso
RingHom
RingHom
|
71 | 53 | biimpcd 239 |
. . . . . . 7
RingIso
RingHom
RingHom |
72 | 71 | adantr 481 |
. . . . . 6
RingIso RingHom
RingHom |
73 | 72 | impcom 446 |
. . . . 5
RingIso
RingHom
RingHom |
74 | | eleq1 2689 |
. . . . . . 7
RingHom
RingHom
|
75 | 74 | ad2antll 765 |
. . . . . 6
RingIso
RingHom
RingHom
|
76 | 75 | anbi2d 740 |
. . . . 5
RingIso
RingHom
RingHom
RingHom
RingHom |
77 | 73, 76 | mpbird 247 |
. . . 4
RingIso
RingHom RingHom
|
78 | | coeq2 5280 |
. . . . . . 7
|
79 | 78 | ad2antll 765 |
. . . . . 6
RingIso
|
80 | | f1ococnv2 6163 |
. . . . . . 7
|
81 | 66, 80 | syl 17 |
. . . . . 6
RingIso
|
82 | 79, 81 | eqtrd 2656 |
. . . . 5
RingIso
|
83 | 77, 69, 82 | jca31 557 |
. . . 4
RingIso
RingHom
RingHom
|
84 | 70, 77, 83 | jca31 557 |
. . 3
RingIso
RingHom RingHom
RingHom
RingHom RingHom RingHom
|
85 | 49, 84 | impbida 877 |
. 2
RingHom RingHom
RingHom
RingHom RingHom RingHom
RingIso
|
86 | 10, 23, 85 | 3bitrd 294 |
1
RingIso |