Step | Hyp | Ref
| Expression |
1 | | eldprdi.1 |
. . . . 5
DProd
|
2 | | eldprdi.2 |
. . . . 5
|
3 | 1, 2 | dprddomcld 18400 |
. . . 4
|
4 | | eldprdi.w |
. . . . 5
finSupp |
5 | | eldprdi.3 |
. . . . 5
|
6 | 4, 1, 2, 5 | dprdfcl 18412 |
. . . 4
|
7 | | dprdfadd.4 |
. . . . 5
|
8 | 4, 1, 2, 7 | dprdfcl 18412 |
. . . 4
|
9 | | eqid 2622 |
. . . . . 6
|
10 | 4, 1, 2, 5, 9 | dprdff 18411 |
. . . . 5
|
11 | 10 | feqmptd 6249 |
. . . 4
|
12 | 4, 1, 2, 7, 9 | dprdff 18411 |
. . . . 5
|
13 | 12 | feqmptd 6249 |
. . . 4
|
14 | 3, 6, 8, 11, 13 | offval2 6914 |
. . 3
|
15 | 1, 2 | dprdf2 18406 |
. . . . . 6
SubGrp |
16 | 15 | ffvelrnda 6359 |
. . . . 5
SubGrp |
17 | | dprdfadd.b |
. . . . . 6
|
18 | 17 | subgcl 17604 |
. . . . 5
SubGrp
|
19 | 16, 6, 8, 18 | syl3anc 1326 |
. . . 4
|
20 | 4, 1, 2, 5 | dprdffsupp 18413 |
. . . . . . 7
finSupp
|
21 | 4, 1, 2, 7 | dprdffsupp 18413 |
. . . . . . 7
finSupp
|
22 | 20, 21 | fsuppunfi 8295 |
. . . . . 6
supp
supp |
23 | | ssun1 3776 |
. . . . . . . . . . 11
supp supp
supp |
24 | 23 | a1i 11 |
. . . . . . . . . 10
supp supp
supp |
25 | | eldprdi.0 |
. . . . . . . . . . . 12
|
26 | | fvex 6201 |
. . . . . . . . . . . 12
|
27 | 25, 26 | eqeltri 2697 |
. . . . . . . . . . 11
|
28 | 27 | a1i 11 |
. . . . . . . . . 10
|
29 | 10, 24, 3, 28 | suppssr 7326 |
. . . . . . . . 9
supp
supp |
30 | | ssun2 3777 |
. . . . . . . . . . 11
supp supp
supp |
31 | 30 | a1i 11 |
. . . . . . . . . 10
supp supp
supp |
32 | 12, 31, 3, 28 | suppssr 7326 |
. . . . . . . . 9
supp
supp |
33 | 29, 32 | oveq12d 6668 |
. . . . . . . 8
supp
supp |
34 | | dprdgrp 18404 |
. . . . . . . . . . 11
DProd
|
35 | 1, 34 | syl 17 |
. . . . . . . . . 10
|
36 | 9, 25 | grpidcl 17450 |
. . . . . . . . . . 11
|
37 | 35, 36 | syl 17 |
. . . . . . . . . 10
|
38 | 9, 17, 25 | grplid 17452 |
. . . . . . . . . 10
|
39 | 35, 37, 38 | syl2anc 693 |
. . . . . . . . 9
|
40 | 39 | adantr 481 |
. . . . . . . 8
supp
supp
|
41 | 33, 40 | eqtrd 2656 |
. . . . . . 7
supp
supp |
42 | 41, 3 | suppss2 7329 |
. . . . . 6
supp supp
supp |
43 | | ssfi 8180 |
. . . . . 6
supp
supp supp supp
supp supp |
44 | 22, 42, 43 | syl2anc 693 |
. . . . 5
supp |
45 | | funmpt 5926 |
. . . . . . 7
|
46 | 45 | a1i 11 |
. . . . . 6
|
47 | | mptexg 6484 |
. . . . . . 7
|
48 | 3, 47 | syl 17 |
. . . . . 6
|
49 | | funisfsupp 8280 |
. . . . . 6
finSupp
supp |
50 | 46, 48, 28, 49 | syl3anc 1326 |
. . . . 5
finSupp
supp |
51 | 44, 50 | mpbird 247 |
. . . 4
finSupp
|
52 | 4, 1, 2, 19, 51 | dprdwd 18410 |
. . 3
|
53 | 14, 52 | eqeltrd 2701 |
. 2
|
54 | | eqid 2622 |
. . 3
Cntz Cntz |
55 | | grpmnd 17429 |
. . . 4
|
56 | 35, 55 | syl 17 |
. . 3
|
57 | | eqid 2622 |
. . 3
supp supp
|
58 | 4, 1, 2, 5, 54 | dprdfcntz 18414 |
. . 3
Cntz |
59 | 4, 1, 2, 7, 54 | dprdfcntz 18414 |
. . 3
Cntz |
60 | 4, 1, 2, 53, 54 | dprdfcntz 18414 |
. . 3
Cntz |
61 | 56 | adantr 481 |
. . . . . . 7
|
62 | | vex 3203 |
. . . . . . . 8
|
63 | 62 | a1i 11 |
. . . . . . 7
|
64 | | eldifi 3732 |
. . . . . . . . . . 11
|
65 | 64 | adantl 482 |
. . . . . . . . . 10
|
66 | | ffvelrn 6357 |
. . . . . . . . . 10
|
67 | 10, 65, 66 | syl2an 494 |
. . . . . . . . 9
|
68 | 67 | snssd 4340 |
. . . . . . . 8
|
69 | 9, 54 | cntzsubm 17768 |
. . . . . . . 8
Cntz SubMnd |
70 | 61, 68, 69 | syl2anc 693 |
. . . . . . 7
Cntz SubMnd |
71 | 12 | adantr 481 |
. . . . . . . . . 10
|
72 | | ffn 6045 |
. . . . . . . . . 10
|
73 | 71, 72 | syl 17 |
. . . . . . . . 9
|
74 | | simprl 794 |
. . . . . . . . 9
|
75 | | fnssres 6004 |
. . . . . . . . 9
|
76 | 73, 74, 75 | syl2anc 693 |
. . . . . . . 8
|
77 | | fvres 6207 |
. . . . . . . . . . 11
|
78 | 77 | adantl 482 |
. . . . . . . . . 10
|
79 | 1 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
DProd |
80 | 2 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
|
81 | 79, 80 | dprdf2 18406 |
. . . . . . . . . . . . . 14
SubGrp |
82 | 65 | ad2antlr 763 |
. . . . . . . . . . . . . 14
|
83 | 81, 82 | ffvelrnd 6360 |
. . . . . . . . . . . . 13
SubGrp |
84 | 9 | subgss 17595 |
. . . . . . . . . . . . 13
SubGrp
|
85 | 83, 84 | syl 17 |
. . . . . . . . . . . 12
|
86 | 5 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
|
87 | 4, 79, 80, 86 | dprdfcl 18412 |
. . . . . . . . . . . . . 14
|
88 | 82, 87 | mpdan 702 |
. . . . . . . . . . . . 13
|
89 | 88 | snssd 4340 |
. . . . . . . . . . . 12
|
90 | 9, 54 | cntz2ss 17765 |
. . . . . . . . . . . 12
Cntz
Cntz |
91 | 85, 89, 90 | syl2anc 693 |
. . . . . . . . . . 11
Cntz
Cntz |
92 | 74 | sselda 3603 |
. . . . . . . . . . . . 13
|
93 | | simpr 477 |
. . . . . . . . . . . . . 14
|
94 | | simplrr 801 |
. . . . . . . . . . . . . . 15
|
95 | 94 | eldifbd 3587 |
. . . . . . . . . . . . . 14
|
96 | | nelne2 2891 |
. . . . . . . . . . . . . 14
|
97 | 93, 95, 96 | syl2anc 693 |
. . . . . . . . . . . . 13
|
98 | 79, 80, 92, 82, 97, 54 | dprdcntz 18407 |
. . . . . . . . . . . 12
Cntz |
99 | 7 | ad2antrr 762 |
. . . . . . . . . . . . . 14
|
100 | 4, 79, 80, 99 | dprdfcl 18412 |
. . . . . . . . . . . . 13
|
101 | 92, 100 | mpdan 702 |
. . . . . . . . . . . 12
|
102 | 98, 101 | sseldd 3604 |
. . . . . . . . . . 11
Cntz |
103 | 91, 102 | sseldd 3604 |
. . . . . . . . . 10
Cntz |
104 | 78, 103 | eqeltrd 2701 |
. . . . . . . . 9
Cntz |
105 | 104 | ralrimiva 2966 |
. . . . . . . 8
Cntz |
106 | | ffnfv 6388 |
. . . . . . . 8
Cntz
Cntz |
107 | 76, 105, 106 | sylanbrc 698 |
. . . . . . 7
Cntz |
108 | | resss 5422 |
. . . . . . . . . 10
|
109 | | rnss 5354 |
. . . . . . . . . 10
|
110 | 108, 109 | ax-mp 5 |
. . . . . . . . 9
|
111 | 54 | cntzidss 17770 |
. . . . . . . . 9
Cntz
Cntz |
112 | 59, 110, 111 | sylancl 694 |
. . . . . . . 8
Cntz |
113 | 112 | adantr 481 |
. . . . . . 7
Cntz
|
114 | 21, 28 | fsuppres 8300 |
. . . . . . . 8
finSupp |
115 | 114 | adantr 481 |
. . . . . . 7
finSupp |
116 | 25, 54, 61, 63, 70, 107, 113, 115 | gsumzsubmcl 18318 |
. . . . . 6
g Cntz |
117 | 116 | snssd 4340 |
. . . . 5
g Cntz |
118 | 71, 74 | fssresd 6071 |
. . . . . . . 8
|
119 | 9, 25, 54, 61, 63, 118, 113, 115 | gsumzcl 18312 |
. . . . . . 7
g |
120 | 119 | snssd 4340 |
. . . . . 6
g |
121 | 9, 54 | cntzrec 17766 |
. . . . . 6
g
g Cntz
Cntz g |
122 | 120, 68, 121 | syl2anc 693 |
. . . . 5
g
Cntz Cntz g |
123 | 117, 122 | mpbid 222 |
. . . 4
Cntz g |
124 | | fvex 6201 |
. . . . 5
|
125 | 124 | snss 4316 |
. . . 4
Cntz g Cntz g |
126 | 123, 125 | sylibr 224 |
. . 3
Cntz g |
127 | 9, 25, 17, 54, 56, 3, 20, 21, 57, 10, 12, 58, 59, 60, 126 | gsumzaddlem 18321 |
. 2
g g g |
128 | 53, 127 | jca 554 |
1
g
g g |