Step | Hyp | Ref
| Expression |
1 | | srhmsubc.c |
. . . 4
|
2 | | eleq1 2689 |
. . . . . . 7
|
3 | | srhmsubc.s |
. . . . . . 7
|
4 | 2, 3 | vtoclri 3283 |
. . . . . 6
|
5 | 4 | ssriv 3607 |
. . . . 5
|
6 | | sslin 3839 |
. . . . 5
|
7 | 5, 6 | mp1i 13 |
. . . 4
|
8 | 1, 7 | syl5eqss 3649 |
. . 3
|
9 | | ssid 3624 |
. . . . . 6
RingHom RingHom |
10 | | eqid 2622 |
. . . . . . 7
RingCat RingCat |
11 | | eqid 2622 |
. . . . . . 7
RingCat RingCat |
12 | | simpl 473 |
. . . . . . 7
|
13 | | eqid 2622 |
. . . . . . 7
RingCat RingCat |
14 | 3, 1 | srhmsubclem2 42074 |
. . . . . . . 8
RingCat |
15 | 14 | adantrr 753 |
. . . . . . 7
RingCat |
16 | 3, 1 | srhmsubclem2 42074 |
. . . . . . . 8
RingCat |
17 | 16 | adantrl 752 |
. . . . . . 7
RingCat |
18 | 10, 11, 12, 13, 15, 17 | ringchom 42013 |
. . . . . 6
RingCat RingHom |
19 | 9, 18 | syl5sseqr 3654 |
. . . . 5
RingHom RingCat |
20 | | srhmsubc.j |
. . . . . . 7
RingHom |
21 | 20 | a1i 11 |
. . . . . 6
RingHom |
22 | | oveq12 6659 |
. . . . . . 7
RingHom RingHom |
23 | 22 | adantl 482 |
. . . . . 6
RingHom RingHom |
24 | | simprl 794 |
. . . . . 6
|
25 | | simprr 796 |
. . . . . 6
|
26 | | ovexd 6680 |
. . . . . 6
RingHom |
27 | 21, 23, 24, 25, 26 | ovmpt2d 6788 |
. . . . 5
RingHom |
28 | | eqid 2622 |
. . . . . 6
f RingCat f
RingCat |
29 | 28, 11, 13, 15, 17 | homfval 16352 |
. . . . 5
f
RingCat RingCat |
30 | 19, 27, 29 | 3sstr4d 3648 |
. . . 4
f RingCat |
31 | 30 | ralrimivva 2971 |
. . 3
f RingCat |
32 | | ovex 6678 |
. . . . . 6
RingHom |
33 | 20, 32 | fnmpt2i 7239 |
. . . . 5
|
34 | 33 | a1i 11 |
. . . 4
|
35 | 28, 11 | homffn 16353 |
. . . . 5
f RingCat RingCat RingCat |
36 | | id 22 |
. . . . . . . . 9
|
37 | 10, 11, 36 | ringcbas 42011 |
. . . . . . . 8
RingCat |
38 | 37 | eqcomd 2628 |
. . . . . . 7
RingCat |
39 | 38 | sqxpeqd 5141 |
. . . . . 6
RingCat RingCat |
40 | 39 | fneq2d 5982 |
. . . . 5
f RingCat
f RingCat RingCat RingCat |
41 | 35, 40 | mpbiri 248 |
. . . 4
f RingCat |
42 | | inex1g 4801 |
. . . 4
|
43 | 34, 41, 42 | isssc 16480 |
. . 3
cat
f RingCat
f
RingCat |
44 | 8, 31, 43 | mpbir2and 957 |
. 2
cat f RingCat |
45 | 1 | elin2 3801 |
. . . . . . . 8
|
46 | 4 | adantl 482 |
. . . . . . . 8
|
47 | 45, 46 | sylbi 207 |
. . . . . . 7
|
48 | 47 | adantl 482 |
. . . . . 6
|
49 | | eqid 2622 |
. . . . . . 7
|
50 | 49 | idrhm 18731 |
. . . . . 6
RingHom |
51 | 48, 50 | syl 17 |
. . . . 5
RingHom |
52 | | eqid 2622 |
. . . . . 6
RingCat RingCat |
53 | | simpl 473 |
. . . . . 6
|
54 | 10, 11, 52, 53, 14, 49 | ringcid 42025 |
. . . . 5
RingCat |
55 | 20 | a1i 11 |
. . . . . 6
RingHom |
56 | | oveq12 6659 |
. . . . . . 7
RingHom RingHom |
57 | 56 | adantl 482 |
. . . . . 6
RingHom
RingHom |
58 | | simpr 477 |
. . . . . 6
|
59 | | ovexd 6680 |
. . . . . 6
RingHom |
60 | 55, 57, 58, 58, 59 | ovmpt2d 6788 |
. . . . 5
RingHom |
61 | 51, 54, 60 | 3eltr4d 2716 |
. . . 4
RingCat |
62 | | eqid 2622 |
. . . . . . . . 9
compRingCat compRingCat |
63 | 10 | ringccat 42024 |
. . . . . . . . . 10
RingCat |
64 | 63 | ad3antrrr 766 |
. . . . . . . . 9
RingCat |
65 | 14 | adantr 481 |
. . . . . . . . . 10
RingCat |
66 | 65 | adantr 481 |
. . . . . . . . 9
RingCat |
67 | 16 | ad2ant2r 783 |
. . . . . . . . . 10
RingCat |
68 | 67 | adantr 481 |
. . . . . . . . 9
RingCat |
69 | 3, 1 | srhmsubclem2 42074 |
. . . . . . . . . . 11
RingCat |
70 | 69 | ad2ant2rl 785 |
. . . . . . . . . 10
RingCat |
71 | 70 | adantr 481 |
. . . . . . . . 9
RingCat |
72 | 53 | adantr 481 |
. . . . . . . . . . . . . . 15
|
73 | | simpl 473 |
. . . . . . . . . . . . . . . 16
|
74 | 58, 73 | anim12i 590 |
. . . . . . . . . . . . . . 15
|
75 | 72, 74 | jca 554 |
. . . . . . . . . . . . . 14
|
76 | 3, 1, 20 | srhmsubclem3 42075 |
. . . . . . . . . . . . . 14
RingCat |
77 | 75, 76 | syl 17 |
. . . . . . . . . . . . 13
RingCat |
78 | 77 | eleq2d 2687 |
. . . . . . . . . . . 12
RingCat |
79 | 78 | biimpcd 239 |
. . . . . . . . . . 11
RingCat |
80 | 79 | adantr 481 |
. . . . . . . . . 10
RingCat |
81 | 80 | impcom 446 |
. . . . . . . . 9
RingCat |
82 | 3, 1, 20 | srhmsubclem3 42075 |
. . . . . . . . . . . . . 14
RingCat |
83 | 82 | adantlr 751 |
. . . . . . . . . . . . 13
RingCat |
84 | 83 | eleq2d 2687 |
. . . . . . . . . . . 12
RingCat |
85 | 84 | biimpd 219 |
. . . . . . . . . . 11
RingCat |
86 | 85 | adantld 483 |
. . . . . . . . . 10
RingCat |
87 | 86 | imp 445 |
. . . . . . . . 9
RingCat |
88 | 11, 13, 62, 64, 66, 68, 71, 81, 87 | catcocl 16346 |
. . . . . . . 8
compRingCat RingCat |
89 | 10, 11, 72, 13, 65, 70 | ringchom 42013 |
. . . . . . . . . 10
RingCat RingHom |
90 | 89 | eqcomd 2628 |
. . . . . . . . 9
RingHom
RingCat |
91 | 90 | adantr 481 |
. . . . . . . 8
RingHom
RingCat |
92 | 88, 91 | eleqtrrd 2704 |
. . . . . . 7
compRingCat RingHom |
93 | 20 | a1i 11 |
. . . . . . . . 9
RingHom |
94 | | oveq12 6659 |
. . . . . . . . . 10
RingHom RingHom |
95 | 94 | adantl 482 |
. . . . . . . . 9
RingHom RingHom |
96 | 58 | adantr 481 |
. . . . . . . . 9
|
97 | | simprr 796 |
. . . . . . . . 9
|
98 | | ovexd 6680 |
. . . . . . . . 9
RingHom
|
99 | 93, 95, 96, 97, 98 | ovmpt2d 6788 |
. . . . . . . 8
RingHom |
100 | 99 | adantr 481 |
. . . . . . 7
RingHom |
101 | 92, 100 | eleqtrrd 2704 |
. . . . . 6
compRingCat |
102 | 101 | ralrimivva 2971 |
. . . . 5
compRingCat |
103 | 102 | ralrimivva 2971 |
. . . 4
compRingCat |
104 | 61, 103 | jca 554 |
. . 3
RingCat
compRingCat |
105 | 104 | ralrimiva 2966 |
. 2
RingCat compRingCat |
106 | 28, 52, 62, 63, 34 | issubc2 16496 |
. 2
SubcatRingCat
cat f RingCat
RingCat compRingCat |
107 | 44, 105, 106 | mpbir2and 957 |
1
SubcatRingCat |