Step | Hyp | Ref
| Expression |
1 | | nghmghm 22538 |
. . . 4
NGHom
|
2 | | eqid 2622 |
. . . . 5
|
3 | | eqid 2622 |
. . . . 5
|
4 | 2, 3 | ghmf 17664 |
. . . 4
|
5 | 1, 4 | syl 17 |
. . 3
NGHom
|
6 | | simprr 796 |
. . . . . 6
NGHom |
7 | | eqid 2622 |
. . . . . . . . 9
|
8 | 7 | nghmcl 22531 |
. . . . . . . 8
NGHom
|
9 | | nghmrcl1 22536 |
. . . . . . . . 9
NGHom
NrmGrp |
10 | | nghmrcl2 22537 |
. . . . . . . . 9
NGHom
NrmGrp |
11 | 7 | nmoge0 22525 |
. . . . . . . . 9
NrmGrp
NrmGrp
|
12 | 9, 10, 1, 11 | syl3anc 1326 |
. . . . . . . 8
NGHom
|
13 | 8, 12 | ge0p1rpd 11902 |
. . . . . . 7
NGHom
|
14 | 13 | adantr 481 |
. . . . . 6
NGHom |
15 | 6, 14 | rpdivcld 11889 |
. . . . 5
NGHom |
16 | | ngpms 22404 |
. . . . . . . . . . . 12
NrmGrp |
17 | 9, 16 | syl 17 |
. . . . . . . . . . 11
NGHom
|
18 | 17 | ad2antrr 762 |
. . . . . . . . . 10
NGHom
|
19 | | simplrl 800 |
. . . . . . . . . 10
NGHom
|
20 | | simpr 477 |
. . . . . . . . . 10
NGHom
|
21 | | eqid 2622 |
. . . . . . . . . . 11
|
22 | 2, 21 | mscl 22266 |
. . . . . . . . . 10
|
23 | 18, 19, 20, 22 | syl3anc 1326 |
. . . . . . . . 9
NGHom
|
24 | 6 | adantr 481 |
. . . . . . . . . 10
NGHom
|
25 | 24 | rpred 11872 |
. . . . . . . . 9
NGHom
|
26 | 13 | ad2antrr 762 |
. . . . . . . . 9
NGHom
|
27 | 23, 25, 26 | ltmuldiv2d 11920 |
. . . . . . . 8
NGHom
|
28 | | ngpms 22404 |
. . . . . . . . . . . . 13
NrmGrp |
29 | 10, 28 | syl 17 |
. . . . . . . . . . . 12
NGHom
|
30 | 29 | ad2antrr 762 |
. . . . . . . . . . 11
NGHom
|
31 | 5 | ad2antrr 762 |
. . . . . . . . . . . 12
NGHom
|
32 | 31, 19 | ffvelrnd 6360 |
. . . . . . . . . . 11
NGHom
|
33 | 31, 20 | ffvelrnd 6360 |
. . . . . . . . . . 11
NGHom
|
34 | | eqid 2622 |
. . . . . . . . . . . 12
|
35 | 3, 34 | mscl 22266 |
. . . . . . . . . . 11
|
36 | 30, 32, 33, 35 | syl3anc 1326 |
. . . . . . . . . 10
NGHom
|
37 | 8 | ad2antrr 762 |
. . . . . . . . . . 11
NGHom
|
38 | 37, 23 | remulcld 10070 |
. . . . . . . . . 10
NGHom
|
39 | 26 | rpred 11872 |
. . . . . . . . . . 11
NGHom
|
40 | 39, 23 | remulcld 10070 |
. . . . . . . . . 10
NGHom
|
41 | 7, 2, 21, 34 | nmods 22548 |
. . . . . . . . . . . 12
NGHom
|
42 | 41 | 3expa 1265 |
. . . . . . . . . . 11
NGHom
|
43 | 42 | adantlrr 757 |
. . . . . . . . . 10
NGHom
|
44 | | msxms 22259 |
. . . . . . . . . . . . 13
|
45 | 18, 44 | syl 17 |
. . . . . . . . . . . 12
NGHom
|
46 | 2, 21 | xmsge0 22268 |
. . . . . . . . . . . 12
|
47 | 45, 19, 20, 46 | syl3anc 1326 |
. . . . . . . . . . 11
NGHom
|
48 | 37 | lep1d 10955 |
. . . . . . . . . . 11
NGHom
|
49 | 37, 39, 23, 47, 48 | lemul1ad 10963 |
. . . . . . . . . 10
NGHom
|
50 | 36, 38, 40, 43, 49 | letrd 10194 |
. . . . . . . . 9
NGHom
|
51 | | lelttr 10128 |
. . . . . . . . . 10
|
52 | 36, 40, 25, 51 | syl3anc 1326 |
. . . . . . . . 9
NGHom
|
53 | 50, 52 | mpand 711 |
. . . . . . . 8
NGHom
|
54 | 27, 53 | sylbird 250 |
. . . . . . 7
NGHom
|
55 | 19, 20 | ovresd 6801 |
. . . . . . . 8
NGHom
|
56 | 55 | breq1d 4663 |
. . . . . . 7
NGHom
|
57 | 32, 33 | ovresd 6801 |
. . . . . . . 8
NGHom
|
58 | 57 | breq1d 4663 |
. . . . . . 7
NGHom
|
59 | 54, 56, 58 | 3imtr4d 283 |
. . . . . 6
NGHom
|
60 | 59 | ralrimiva 2966 |
. . . . 5
NGHom
|
61 | | breq2 4657 |
. . . . . . . 8
|
62 | 61 | imbi1d 331 |
. . . . . . 7
|
63 | 62 | ralbidv 2986 |
. . . . . 6
|
64 | 63 | rspcev 3309 |
. . . . 5
|
65 | 15, 60, 64 | syl2anc 693 |
. . . 4
NGHom
|
66 | 65 | ralrimivva 2971 |
. . 3
NGHom
|
67 | | eqid 2622 |
. . . . . 6
|
68 | 2, 67 | xmsxmet 22261 |
. . . . 5
|
69 | 17, 44, 68 | 3syl 18 |
. . . 4
NGHom
|
70 | | msxms 22259 |
. . . . 5
|
71 | | eqid 2622 |
. . . . . 6
|
72 | 3, 71 | xmsxmet 22261 |
. . . . 5
|
73 | 29, 70, 72 | 3syl 18 |
. . . 4
NGHom
|
74 | | eqid 2622 |
. . . . 5
|
75 | | eqid 2622 |
. . . . 5
|
76 | 74, 75 | metcn 22348 |
. . . 4
|
77 | 69, 73, 76 | syl2anc 693 |
. . 3
NGHom
|
78 | 5, 66, 77 | mpbir2and 957 |
. 2
NGHom
|
79 | | nghmcn.j |
. . . . 5
|
80 | 79, 2, 67 | mstopn 22257 |
. . . 4
|
81 | 17, 80 | syl 17 |
. . 3
NGHom
|
82 | | nghmcn.k |
. . . . 5
|
83 | 82, 3, 71 | mstopn 22257 |
. . . 4
|
84 | 29, 83 | syl 17 |
. . 3
NGHom
|
85 | 81, 84 | oveq12d 6668 |
. 2
NGHom
|
86 | 78, 85 | eleqtrrd 2704 |
1
NGHom
|