Step | Hyp | Ref
| Expression |
1 | | elex 3212 |
. . . . 5
SubGrp
|
2 | 1 | a1i 11 |
. . . 4
SubGrp
|
3 | | fex 6490 |
. . . . . . 7
SubGrp |
4 | 3 | expcom 451 |
. . . . . 6
SubGrp |
5 | 4 | adantr 481 |
. . . . 5
SubGrp |
6 | 5 | adantrd 484 |
. . . 4
SubGrp
|
7 | | df-sbc 3436 |
. . . . . 6
SubGrp
SubGrp
|
8 | | simpr 477 |
. . . . . . 7
|
9 | | simpr 477 |
. . . . . . . . . 10
|
10 | 9 | dmeqd 5326 |
. . . . . . . . . . 11
|
11 | | simplr 792 |
. . . . . . . . . . 11
|
12 | 10, 11 | eqtrd 2656 |
. . . . . . . . . 10
|
13 | 9, 12 | feq12d 6033 |
. . . . . . . . 9
SubGrp
SubGrp |
14 | 12 | difeq1d 3727 |
. . . . . . . . . . . 12
|
15 | 9 | fveq1d 6193 |
. . . . . . . . . . . . 13
|
16 | 9 | fveq1d 6193 |
. . . . . . . . . . . . . 14
|
17 | 16 | fveq2d 6195 |
. . . . . . . . . . . . 13
|
18 | 15, 17 | sseq12d 3634 |
. . . . . . . . . . . 12
|
19 | 14, 18 | raleqbidv 3152 |
. . . . . . . . . . 11
|
20 | 9, 14 | imaeq12d 5467 |
. . . . . . . . . . . . . . 15
|
21 | 20 | unieqd 4446 |
. . . . . . . . . . . . . 14
|
22 | 21 | fveq2d 6195 |
. . . . . . . . . . . . 13
|
23 | 15, 22 | ineq12d 3815 |
. . . . . . . . . . . 12
|
24 | 23 | eqeq1d 2624 |
. . . . . . . . . . 11
|
25 | 19, 24 | anbi12d 747 |
. . . . . . . . . 10
|
26 | 12, 25 | raleqbidv 3152 |
. . . . . . . . 9
|
27 | 13, 26 | anbi12d 747 |
. . . . . . . 8
SubGrp
SubGrp
|
28 | 27 | adantlr 751 |
. . . . . . 7
SubGrp
SubGrp
|
29 | 8, 28 | sbcied 3472 |
. . . . . 6
SubGrp
SubGrp
|
30 | 7, 29 | syl5bbr 274 |
. . . . 5
SubGrp
SubGrp
|
31 | 30 | ex 450 |
. . . 4
SubGrp
SubGrp
|
32 | 2, 6, 31 | pm5.21ndd 369 |
. . 3
SubGrp
SubGrp
|
33 | 32 | anbi2d 740 |
. 2
SubGrp
SubGrp
|
34 | | df-br 4654 |
. . 3
DProd
DProd |
35 | | fvex 6201 |
. . . . . . . . . . 11
|
36 | 35 | rgenw 2924 |
. . . . . . . . . 10
|
37 | | ixpexg 7932 |
. . . . . . . . . 10
|
38 | 36, 37 | ax-mp 5 |
. . . . . . . . 9
|
39 | 38 | mptrabex 6488 |
. . . . . . . 8
finSupp g |
40 | 39 | rnex 7100 |
. . . . . . 7
finSupp g |
41 | 40 | rgen2w 2925 |
. . . . . 6
SubGrp
Cntz
mrClsSubGrp
finSupp
g |
42 | | df-dprd 18394 |
. . . . . . 7
DProd SubGrp
Cntz
mrClsSubGrp
finSupp
g |
43 | 42 | fmpt2x 7236 |
. . . . . 6
SubGrp
Cntz
mrClsSubGrp
finSupp
g DProd
SubGrp
Cntz
mrClsSubGrp |
44 | 41, 43 | mpbi 220 |
. . . . 5
DProd
SubGrp
Cntz
mrClsSubGrp |
45 | 44 | fdmi 6052 |
. . . 4
DProd
SubGrp
Cntz
mrClsSubGrp |
46 | 45 | eleq2i 2693 |
. . 3
DProd
SubGrp
Cntz
mrClsSubGrp |
47 | | fveq2 6191 |
. . . . . . 7
SubGrp SubGrp |
48 | 47 | feq3d 6032 |
. . . . . 6
SubGrp
SubGrp |
49 | | fveq2 6191 |
. . . . . . . . . . . 12
Cntz Cntz |
50 | | dmdprd.z |
. . . . . . . . . . . 12
Cntz |
51 | 49, 50 | syl6eqr 2674 |
. . . . . . . . . . 11
Cntz |
52 | 51 | fveq1d 6193 |
. . . . . . . . . 10
Cntz |
53 | 52 | sseq2d 3633 |
. . . . . . . . 9
Cntz |
54 | 53 | ralbidv 2986 |
. . . . . . . 8
Cntz
|
55 | 47 | fveq2d 6195 |
. . . . . . . . . . . 12
mrClsSubGrp mrClsSubGrp |
56 | | dmdprd.k |
. . . . . . . . . . . 12
mrClsSubGrp |
57 | 55, 56 | syl6eqr 2674 |
. . . . . . . . . . 11
mrClsSubGrp |
58 | 57 | fveq1d 6193 |
. . . . . . . . . 10
mrClsSubGrp |
59 | 58 | ineq2d 3814 |
. . . . . . . . 9
mrClsSubGrp |
60 | | fveq2 6191 |
. . . . . . . . . . 11
|
61 | | dmdprd.0 |
. . . . . . . . . . 11
|
62 | 60, 61 | syl6eqr 2674 |
. . . . . . . . . 10
|
63 | 62 | sneqd 4189 |
. . . . . . . . 9
|
64 | 59, 63 | eqeq12d 2637 |
. . . . . . . 8
mrClsSubGrp |
65 | 54, 64 | anbi12d 747 |
. . . . . . 7
Cntz
mrClsSubGrp
|
66 | 65 | ralbidv 2986 |
. . . . . 6
Cntz
mrClsSubGrp
|
67 | 48, 66 | anbi12d 747 |
. . . . 5
SubGrp
Cntz
mrClsSubGrp
SubGrp
|
68 | 67 | abbidv 2741 |
. . . 4
SubGrp
Cntz
mrClsSubGrp SubGrp
|
69 | 68 | opeliunxp2 5260 |
. . 3
SubGrp
Cntz
mrClsSubGrp
SubGrp
|
70 | 34, 46, 69 | 3bitri 286 |
. 2
DProd
SubGrp
|
71 | | 3anass 1042 |
. 2
SubGrp
SubGrp
|
72 | 33, 70, 71 | 3bitr4g 303 |
1
DProd SubGrp
|