Step | Hyp | Ref
| Expression |
1 | | mgmhmrcl 41781 |
. . . 4
MgmHom
Mgm Mgm |
2 | 1 | simprd 479 |
. . 3
MgmHom
Mgm |
3 | | mgmhmrcl 41781 |
. . . 4
MgmHom
Mgm Mgm |
4 | 3 | simpld 475 |
. . 3
MgmHom
Mgm |
5 | 2, 4 | anim12ci 591 |
. 2
MgmHom MgmHom
Mgm Mgm |
6 | | eqid 2622 |
. . . . 5
|
7 | | eqid 2622 |
. . . . 5
|
8 | 6, 7 | mgmhmf 41784 |
. . . 4
MgmHom
|
9 | | eqid 2622 |
. . . . 5
|
10 | 9, 6 | mgmhmf 41784 |
. . . 4
MgmHom
|
11 | | fco 6058 |
. . . 4
|
12 | 8, 10, 11 | syl2an 494 |
. . 3
MgmHom MgmHom
|
13 | | eqid 2622 |
. . . . . . . . . 10
|
14 | | eqid 2622 |
. . . . . . . . . 10
|
15 | 9, 13, 14 | mgmhmlin 41786 |
. . . . . . . . 9
MgmHom
|
16 | 15 | 3expb 1266 |
. . . . . . . 8
MgmHom |
17 | 16 | adantll 750 |
. . . . . . 7
MgmHom
MgmHom |
18 | 17 | fveq2d 6195 |
. . . . . 6
MgmHom
MgmHom
|
19 | | simpll 790 |
. . . . . . 7
MgmHom
MgmHom
MgmHom |
20 | 10 | ad2antlr 763 |
. . . . . . . 8
MgmHom
MgmHom |
21 | | simprl 794 |
. . . . . . . 8
MgmHom
MgmHom
|
22 | 20, 21 | ffvelrnd 6360 |
. . . . . . 7
MgmHom
MgmHom |
23 | | simprr 796 |
. . . . . . . 8
MgmHom
MgmHom |
24 | 20, 23 | ffvelrnd 6360 |
. . . . . . 7
MgmHom
MgmHom |
25 | | eqid 2622 |
. . . . . . . 8
|
26 | 6, 14, 25 | mgmhmlin 41786 |
. . . . . . 7
MgmHom
|
27 | 19, 22, 24, 26 | syl3anc 1326 |
. . . . . 6
MgmHom
MgmHom |
28 | 18, 27 | eqtrd 2656 |
. . . . 5
MgmHom
MgmHom
|
29 | 4 | adantl 482 |
. . . . . . 7
MgmHom MgmHom
Mgm |
30 | 9, 13 | mgmcl 17245 |
. . . . . . . 8
Mgm
|
31 | 30 | 3expb 1266 |
. . . . . . 7
Mgm |
32 | 29, 31 | sylan 488 |
. . . . . 6
MgmHom
MgmHom |
33 | | fvco3 6275 |
. . . . . 6
|
34 | 20, 32, 33 | syl2anc 693 |
. . . . 5
MgmHom
MgmHom |
35 | | fvco3 6275 |
. . . . . . 7
|
36 | 20, 21, 35 | syl2anc 693 |
. . . . . 6
MgmHom
MgmHom |
37 | | fvco3 6275 |
. . . . . . 7
|
38 | 20, 23, 37 | syl2anc 693 |
. . . . . 6
MgmHom
MgmHom |
39 | 36, 38 | oveq12d 6668 |
. . . . 5
MgmHom
MgmHom |
40 | 28, 34, 39 | 3eqtr4d 2666 |
. . . 4
MgmHom
MgmHom |
41 | 40 | ralrimivva 2971 |
. . 3
MgmHom MgmHom
|
42 | 12, 41 | jca 554 |
. 2
MgmHom MgmHom
|
43 | 9, 7, 13, 25 | ismgmhm 41783 |
. 2
MgmHom Mgm
Mgm
|
44 | 5, 42, 43 | sylanbrc 698 |
1
MgmHom MgmHom
MgmHom |