Proof of Theorem funcringcsetclem9ALTV
Step | Hyp | Ref
| Expression |
1 | | funcringcsetcALTV.r |
. . . . . 6
RingCatALTV |
2 | | funcringcsetcALTV.b |
. . . . . 6
|
3 | | funcringcsetcALTV.u |
. . . . . . 7
WUni |
4 | 3 | adantr 481 |
. . . . . 6
WUni |
5 | | eqid 2622 |
. . . . . 6
|
6 | | simpr1 1067 |
. . . . . 6
|
7 | | simpr2 1068 |
. . . . . 6
|
8 | 1, 2, 4, 5, 6, 7 | ringchomALTV 42048 |
. . . . 5
RingHom |
9 | 8 | eleq2d 2687 |
. . . 4
RingHom |
10 | | simpr3 1069 |
. . . . . 6
|
11 | 1, 2, 4, 5, 7, 10 | ringchomALTV 42048 |
. . . . 5
RingHom |
12 | 11 | eleq2d 2687 |
. . . 4
RingHom |
13 | 9, 12 | anbi12d 747 |
. . 3
RingHom RingHom
|
14 | | rhmco 18737 |
. . . . . . . 8
RingHom RingHom
RingHom |
15 | 14 | ancoms 469 |
. . . . . . 7
RingHom RingHom
RingHom |
16 | 15 | adantl 482 |
. . . . . 6
RingHom
RingHom RingHom |
17 | | fvresi 6439 |
. . . . . 6
RingHom
RingHom
|
18 | 16, 17 | syl 17 |
. . . . 5
RingHom
RingHom RingHom
|
19 | | funcringcsetcALTV.s |
. . . . . . . . 9
|
20 | | funcringcsetcALTV.c |
. . . . . . . . 9
|
21 | | funcringcsetcALTV.f |
. . . . . . . . 9
|
22 | | funcringcsetcALTV.g |
. . . . . . . . 9
RingHom |
23 | 1, 19, 2, 20, 3, 21, 22 | funcringcsetclem5ALTV 42063 |
. . . . . . . 8
RingHom
|
24 | 23 | 3adantr2 1221 |
. . . . . . 7
RingHom
|
25 | 24 | adantr 481 |
. . . . . 6
RingHom
RingHom
RingHom |
26 | 4 | adantr 481 |
. . . . . . 7
RingHom
RingHom WUni |
27 | | eqid 2622 |
. . . . . . 7
comp comp |
28 | 6 | adantr 481 |
. . . . . . 7
RingHom
RingHom |
29 | 7 | adantr 481 |
. . . . . . 7
RingHom
RingHom |
30 | 10 | adantr 481 |
. . . . . . 7
RingHom
RingHom |
31 | | simprl 794 |
. . . . . . 7
RingHom
RingHom RingHom |
32 | | simprr 796 |
. . . . . . 7
RingHom
RingHom RingHom |
33 | 1, 2, 26, 27, 28, 29, 30, 31, 32 | ringccoALTV 42051 |
. . . . . 6
RingHom
RingHom comp |
34 | 25, 33 | fveq12d 6197 |
. . . . 5
RingHom
RingHom comp RingHom
|
35 | | eqid 2622 |
. . . . . . 7
comp comp |
36 | 1, 19, 2, 20, 3, 21 | funcringcsetclem2ALTV 42060 |
. . . . . . . . 9
|
37 | 36 | 3ad2antr1 1226 |
. . . . . . . 8
|
38 | 37 | adantr 481 |
. . . . . . 7
RingHom
RingHom |
39 | 1, 19, 2, 20, 3, 21 | funcringcsetclem2ALTV 42060 |
. . . . . . . . 9
|
40 | 39 | 3ad2antr2 1227 |
. . . . . . . 8
|
41 | 40 | adantr 481 |
. . . . . . 7
RingHom
RingHom |
42 | 1, 19, 2, 20, 3, 21 | funcringcsetclem2ALTV 42060 |
. . . . . . . . 9
|
43 | 42 | 3ad2antr3 1228 |
. . . . . . . 8
|
44 | 43 | adantr 481 |
. . . . . . 7
RingHom
RingHom |
45 | | eqid 2622 |
. . . . . . . . . . 11
|
46 | | eqid 2622 |
. . . . . . . . . . 11
|
47 | 45, 46 | rhmf 18726 |
. . . . . . . . . 10
RingHom
|
48 | 47 | ad2antrl 764 |
. . . . . . . . 9
RingHom
RingHom |
49 | 1, 19, 2, 20, 3, 21 | funcringcsetclem1ALTV 42059 |
. . . . . . . . . . . 12
|
50 | 49 | 3ad2antr1 1226 |
. . . . . . . . . . 11
|
51 | 1, 19, 2, 20, 3, 21 | funcringcsetclem1ALTV 42059 |
. . . . . . . . . . . 12
|
52 | 51 | 3ad2antr2 1227 |
. . . . . . . . . . 11
|
53 | 50, 52 | feq23d 6040 |
. . . . . . . . . 10
|
54 | 53 | adantr 481 |
. . . . . . . . 9
RingHom
RingHom
|
55 | 48, 54 | mpbird 247 |
. . . . . . . 8
RingHom
RingHom |
56 | | simpll 790 |
. . . . . . . . . 10
RingHom
RingHom |
57 | | 3simpa 1058 |
. . . . . . . . . . 11
|
58 | 57 | ad2antlr 763 |
. . . . . . . . . 10
RingHom
RingHom |
59 | 1, 19, 2, 20, 3, 21, 22 | funcringcsetclem6ALTV 42064 |
. . . . . . . . . 10
RingHom
|
60 | 56, 58, 31, 59 | syl3anc 1326 |
. . . . . . . . 9
RingHom
RingHom |
61 | 60 | feq1d 6030 |
. . . . . . . 8
RingHom
RingHom
|
62 | 55, 61 | mpbird 247 |
. . . . . . 7
RingHom
RingHom |
63 | | eqid 2622 |
. . . . . . . . . . 11
|
64 | 46, 63 | rhmf 18726 |
. . . . . . . . . 10
RingHom
|
65 | 64 | ad2antll 765 |
. . . . . . . . 9
RingHom
RingHom |
66 | 1, 19, 2, 20, 3, 21 | funcringcsetclem1ALTV 42059 |
. . . . . . . . . . . 12
|
67 | 66 | 3ad2antr3 1228 |
. . . . . . . . . . 11
|
68 | 52, 67 | feq23d 6040 |
. . . . . . . . . 10
|
69 | 68 | adantr 481 |
. . . . . . . . 9
RingHom
RingHom
|
70 | 65, 69 | mpbird 247 |
. . . . . . . 8
RingHom
RingHom |
71 | | 3simpc 1060 |
. . . . . . . . . . 11
|
72 | 71 | ad2antlr 763 |
. . . . . . . . . 10
RingHom
RingHom |
73 | 1, 19, 2, 20, 3, 21, 22 | funcringcsetclem6ALTV 42064 |
. . . . . . . . . 10
RingHom
|
74 | 56, 72, 32, 73 | syl3anc 1326 |
. . . . . . . . 9
RingHom
RingHom |
75 | 74 | feq1d 6030 |
. . . . . . . 8
RingHom
RingHom
|
76 | 70, 75 | mpbird 247 |
. . . . . . 7
RingHom
RingHom |
77 | 19, 26, 35, 38, 41, 44, 62, 76 | setcco 16733 |
. . . . . 6
RingHom
RingHom comp |
78 | 74, 60 | coeq12d 5286 |
. . . . . 6
RingHom
RingHom |
79 | 77, 78 | eqtrd 2656 |
. . . . 5
RingHom
RingHom comp |
80 | 18, 34, 79 | 3eqtr4d 2666 |
. . . 4
RingHom
RingHom comp comp |
81 | 80 | ex 450 |
. . 3
RingHom
RingHom comp comp |
82 | 13, 81 | sylbid 230 |
. 2
comp comp |
83 | 82 | 3impia 1261 |
1
comp comp |