Step | Hyp | Ref
| Expression |
1 | | simpl 473 |
. 2
DProd
DProd |
2 | | reldmdprd 18396 |
. . . . . 6
DProd |
3 | 2 | brrelex2i 5159 |
. . . . 5
DProd
|
4 | 3 | adantr 481 |
. . . 4
DProd
|
5 | 2 | brrelexi 5158 |
. . . . . 6
DProd |
6 | | breq1 4656 |
. . . . . . . 8
DProd
DProd |
7 | | oveq1 6657 |
. . . . . . . . 9
DProd DProd |
8 | | fveq2 6191 |
. . . . . . . . . . . . . 14
|
9 | | dprdval.0 |
. . . . . . . . . . . . . 14
|
10 | 8, 9 | syl6eqr 2674 |
. . . . . . . . . . . . 13
|
11 | 10 | breq2d 4665 |
. . . . . . . . . . . 12
finSupp
finSupp |
12 | 11 | rabbidv 3189 |
. . . . . . . . . . 11
finSupp finSupp
|
13 | | oveq1 6657 |
. . . . . . . . . . 11
g g |
14 | 12, 13 | mpteq12dv 4733 |
. . . . . . . . . 10
finSupp g finSupp
g |
15 | 14 | rneqd 5353 |
. . . . . . . . 9
finSupp g
finSupp
g |
16 | 7, 15 | eqeq12d 2637 |
. . . . . . . 8
DProd
finSupp g
DProd finSupp g |
17 | 6, 16 | imbi12d 334 |
. . . . . . 7
DProd DProd
finSupp g DProd DProd
finSupp
g |
18 | | df-br 4654 |
. . . . . . . . 9
DProd
DProd |
19 | | fvex 6201 |
. . . . . . . . . . . . . . . . 17
|
20 | 19 | rgenw 2924 |
. . . . . . . . . . . . . . . 16
|
21 | | ixpexg 7932 |
. . . . . . . . . . . . . . . 16
|
22 | 20, 21 | ax-mp 5 |
. . . . . . . . . . . . . . 15
|
23 | 22 | mptrabex 6488 |
. . . . . . . . . . . . . 14
finSupp g |
24 | 23 | rnex 7100 |
. . . . . . . . . . . . 13
finSupp g |
25 | 24 | rgen2w 2925 |
. . . . . . . . . . . 12
SubGrp
Cntz
mrClsSubGrp
finSupp
g |
26 | | df-dprd 18394 |
. . . . . . . . . . . . 13
DProd SubGrp
Cntz
mrClsSubGrp
finSupp
g |
27 | 26 | fmpt2x 7236 |
. . . . . . . . . . . 12
SubGrp
Cntz
mrClsSubGrp
finSupp
g DProd
SubGrp
Cntz
mrClsSubGrp |
28 | 25, 27 | mpbi 220 |
. . . . . . . . . . 11
DProd
SubGrp
Cntz
mrClsSubGrp |
29 | 28 | fdmi 6052 |
. . . . . . . . . 10
DProd
SubGrp
Cntz
mrClsSubGrp |
30 | 29 | eleq2i 2693 |
. . . . . . . . 9
DProd
SubGrp
Cntz
mrClsSubGrp |
31 | | opeliunxp 5170 |
. . . . . . . . 9
SubGrp
Cntz
mrClsSubGrp
SubGrp
Cntz
mrClsSubGrp |
32 | 18, 30, 31 | 3bitri 286 |
. . . . . . . 8
DProd
SubGrp
Cntz
mrClsSubGrp |
33 | 26 | ovmpt4g 6783 |
. . . . . . . . 9
SubGrp
Cntz
mrClsSubGrp
finSupp g DProd
finSupp
g |
34 | 24, 33 | mp3an3 1413 |
. . . . . . . 8
SubGrp
Cntz
mrClsSubGrp
DProd finSupp g |
35 | 32, 34 | sylbi 207 |
. . . . . . 7
DProd DProd
finSupp
g |
36 | 17, 35 | vtoclg 3266 |
. . . . . 6
DProd DProd finSupp
g |
37 | 5, 36 | mpcom 38 |
. . . . 5
DProd DProd finSupp
g |
38 | 37 | sbcth 3450 |
. . . 4
DProd DProd finSupp
g |
39 | 4, 38 | syl 17 |
. . 3
DProd
DProd DProd
finSupp
g |
40 | | simpr 477 |
. . . . . 6
DProd
|
41 | 40 | breq2d 4665 |
. . . . 5
DProd
DProd DProd
|
42 | 40 | oveq2d 6666 |
. . . . . 6
DProd
DProd DProd |
43 | 40 | dmeqd 5326 |
. . . . . . . . . . . . 13
DProd
|
44 | | simplr 792 |
. . . . . . . . . . . . 13
DProd
|
45 | 43, 44 | eqtrd 2656 |
. . . . . . . . . . . 12
DProd
|
46 | 45 | ixpeq1d 7920 |
. . . . . . . . . . 11
DProd
|
47 | 40 | fveq1d 6193 |
. . . . . . . . . . . 12
DProd
|
48 | 47 | ixpeq2dv 7924 |
. . . . . . . . . . 11
DProd
|
49 | 46, 48 | eqtrd 2656 |
. . . . . . . . . 10
DProd
|
50 | 49 | rabeqdv 3194 |
. . . . . . . . 9
DProd
finSupp finSupp |
51 | | dprdval.w |
. . . . . . . . 9
finSupp |
52 | 50, 51 | syl6eqr 2674 |
. . . . . . . 8
DProd
finSupp |
53 | | eqidd 2623 |
. . . . . . . 8
DProd
g g |
54 | 52, 53 | mpteq12dv 4733 |
. . . . . . 7
DProd
finSupp
g g |
55 | 54 | rneqd 5353 |
. . . . . 6
DProd
finSupp g g |
56 | 42, 55 | eqeq12d 2637 |
. . . . 5
DProd
DProd finSupp
g
DProd g |
57 | 41, 56 | imbi12d 334 |
. . . 4
DProd
DProd DProd finSupp
g DProd DProd
g |
58 | 4, 57 | sbcied 3472 |
. . 3
DProd
DProd DProd finSupp
g DProd DProd
g |
59 | 39, 58 | mpbid 222 |
. 2
DProd
DProd DProd g |
60 | 1, 59 | mpd 15 |
1
DProd
DProd g |