Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . 3
Cntz Cntz |
2 | | eqid 2622 |
. . 3
|
3 | | eqid 2622 |
. . 3
mrClsSubGrp mrClsSubGrp |
4 | | dprdss.1 |
. . . 4
DProd
|
5 | | dprdgrp 18404 |
. . . 4
DProd
|
6 | 4, 5 | syl 17 |
. . 3
|
7 | | dprdss.2 |
. . . 4
|
8 | 4, 7 | dprddomcld 18400 |
. . 3
|
9 | | dprdss.3 |
. . 3
SubGrp |
10 | | dprdss.4 |
. . . . . . 7
|
11 | 10 | ralrimiva 2966 |
. . . . . 6
|
12 | | fveq2 6191 |
. . . . . . . 8
|
13 | | fveq2 6191 |
. . . . . . . 8
|
14 | 12, 13 | sseq12d 3634 |
. . . . . . 7
|
15 | 14 | rspcv 3305 |
. . . . . 6
|
16 | 11, 15 | mpan9 486 |
. . . . 5
|
17 | 16 | 3ad2antr1 1226 |
. . . 4
|
18 | 4 | adantr 481 |
. . . . . 6
DProd |
19 | 7 | adantr 481 |
. . . . . 6
|
20 | | simpr1 1067 |
. . . . . 6
|
21 | | simpr2 1068 |
. . . . . 6
|
22 | | simpr3 1069 |
. . . . . 6
|
23 | 18, 19, 20, 21, 22, 1 | dprdcntz 18407 |
. . . . 5
Cntz |
24 | 4, 7 | dprdf2 18406 |
. . . . . . . . 9
SubGrp |
25 | 24 | adantr 481 |
. . . . . . . 8
SubGrp |
26 | 25, 21 | ffvelrnd 6360 |
. . . . . . 7
SubGrp |
27 | | eqid 2622 |
. . . . . . . 8
|
28 | 27 | subgss 17595 |
. . . . . . 7
SubGrp
|
29 | 26, 28 | syl 17 |
. . . . . 6
|
30 | 11 | adantr 481 |
. . . . . . 7
|
31 | | fveq2 6191 |
. . . . . . . . 9
|
32 | | fveq2 6191 |
. . . . . . . . 9
|
33 | 31, 32 | sseq12d 3634 |
. . . . . . . 8
|
34 | 33 | rspcv 3305 |
. . . . . . 7
|
35 | 21, 30, 34 | sylc 65 |
. . . . . 6
|
36 | 27, 1 | cntz2ss 17765 |
. . . . . 6
Cntz Cntz |
37 | 29, 35, 36 | syl2anc 693 |
. . . . 5
Cntz Cntz |
38 | 23, 37 | sstrd 3613 |
. . . 4
Cntz |
39 | 17, 38 | sstrd 3613 |
. . 3
Cntz |
40 | 6 | adantr 481 |
. . . . . . 7
|
41 | 27 | subgacs 17629 |
. . . . . . 7
SubGrp ACS |
42 | | acsmre 16313 |
. . . . . . 7
SubGrp ACS SubGrp Moore |
43 | 40, 41, 42 | 3syl 18 |
. . . . . 6
SubGrp Moore |
44 | | difss 3737 |
. . . . . . . . 9
|
45 | 11 | adantr 481 |
. . . . . . . . 9
|
46 | | ssralv 3666 |
. . . . . . . . 9
|
47 | 44, 45, 46 | mpsyl 68 |
. . . . . . . 8
|
48 | | ss2iun 4536 |
. . . . . . . 8
|
49 | 47, 48 | syl 17 |
. . . . . . 7
|
50 | 9 | adantr 481 |
. . . . . . . 8
SubGrp |
51 | | ffun 6048 |
. . . . . . . 8
SubGrp |
52 | | funiunfv 6506 |
. . . . . . . 8
|
53 | 50, 51, 52 | 3syl 18 |
. . . . . . 7
|
54 | 24 | adantr 481 |
. . . . . . . 8
SubGrp |
55 | | ffun 6048 |
. . . . . . . 8
SubGrp |
56 | | funiunfv 6506 |
. . . . . . . 8
|
57 | 54, 55, 56 | 3syl 18 |
. . . . . . 7
|
58 | 49, 53, 57 | 3sstr3d 3647 |
. . . . . 6
|
59 | | imassrn 5477 |
. . . . . . . 8
|
60 | | frn 6053 |
. . . . . . . . . 10
SubGrp SubGrp |
61 | 54, 60 | syl 17 |
. . . . . . . . 9
SubGrp |
62 | | mresspw 16252 |
. . . . . . . . . 10
SubGrp Moore SubGrp |
63 | 43, 62 | syl 17 |
. . . . . . . . 9
SubGrp |
64 | 61, 63 | sstrd 3613 |
. . . . . . . 8
|
65 | 59, 64 | syl5ss 3614 |
. . . . . . 7
|
66 | | sspwuni 4611 |
. . . . . . 7
|
67 | 65, 66 | sylib 208 |
. . . . . 6
|
68 | 43, 3, 58, 67 | mrcssd 16284 |
. . . . 5
mrClsSubGrp mrClsSubGrp |
69 | | ss2in 3840 |
. . . . 5
mrClsSubGrp mrClsSubGrp mrClsSubGrp
mrClsSubGrp
|
70 | 16, 68, 69 | syl2anc 693 |
. . . 4
mrClsSubGrp mrClsSubGrp |
71 | 4 | adantr 481 |
. . . . 5
DProd |
72 | 7 | adantr 481 |
. . . . 5
|
73 | | simpr 477 |
. . . . 5
|
74 | 71, 72, 73, 2, 3 | dprddisj 18408 |
. . . 4
mrClsSubGrp |
75 | 70, 74 | sseqtrd 3641 |
. . 3
mrClsSubGrp |
76 | 1, 2, 3, 6, 8, 9, 39, 75 | dmdprdd 18398 |
. 2
DProd
|
77 | 4 | a1d 25 |
. . . . 5
DProd DProd |
78 | | ss2ixp 7921 |
. . . . . . 7
|
79 | 11, 78 | syl 17 |
. . . . . 6
|
80 | | rabss2 3685 |
. . . . . 6
finSupp
finSupp |
81 | | ssrexv 3667 |
. . . . . 6
finSupp finSupp
finSupp g
finSupp g |
82 | 79, 80, 81 | 3syl 18 |
. . . . 5
finSupp g
finSupp g |
83 | 77, 82 | anim12d 586 |
. . . 4
DProd
finSupp g
DProd
finSupp g |
84 | | fdm 6051 |
. . . . 5
SubGrp |
85 | | eqid 2622 |
. . . . . 6
finSupp
finSupp |
86 | 2, 85 | eldprd 18403 |
. . . . 5
DProd
DProd
finSupp g |
87 | 9, 84, 86 | 3syl 18 |
. . . 4
DProd
DProd
finSupp g |
88 | | eqid 2622 |
. . . . . 6
finSupp
finSupp |
89 | 2, 88 | eldprd 18403 |
. . . . 5
DProd
DProd
finSupp g |
90 | 7, 89 | syl 17 |
. . . 4
DProd
DProd
finSupp g |
91 | 83, 87, 90 | 3imtr4d 283 |
. . 3
DProd DProd |
92 | 91 | ssrdv 3609 |
. 2
DProd DProd |
93 | 76, 92 | jca 554 |
1
DProd
DProd
DProd |