Step | Hyp | Ref
| Expression |
1 | | gsumdixp.b |
. . . 4
|
2 | | gsumdixp.z |
. . . 4
|
3 | | gsumdixp.r |
. . . . 5
|
4 | | ringcmn 18581 |
. . . . 5
CMnd |
5 | 3, 4 | syl 17 |
. . . 4
CMnd |
6 | | gsumdixp.i |
. . . 4
|
7 | | gsumdixp.j |
. . . . 5
|
8 | 7 | adantr 481 |
. . . 4
|
9 | 3 | adantr 481 |
. . . . 5
|
10 | | gsumdixp.x |
. . . . . . 7
|
11 | | eqid 2622 |
. . . . . . 7
|
12 | 10, 11 | fmptd 6385 |
. . . . . 6
|
13 | | simpl 473 |
. . . . . 6
|
14 | | ffvelrn 6357 |
. . . . . 6
|
15 | 12, 13, 14 | syl2an 494 |
. . . . 5
|
16 | | gsumdixp.y |
. . . . . . 7
|
17 | | eqid 2622 |
. . . . . . 7
|
18 | 16, 17 | fmptd 6385 |
. . . . . 6
|
19 | | simpr 477 |
. . . . . 6
|
20 | | ffvelrn 6357 |
. . . . . 6
|
21 | 18, 19, 20 | syl2an 494 |
. . . . 5
|
22 | | gsumdixp.t |
. . . . . 6
|
23 | 1, 22 | ringcl 18561 |
. . . . 5
|
24 | 9, 15, 21, 23 | syl3anc 1326 |
. . . 4
|
25 | | gsumdixp.xf |
. . . . . 6
finSupp |
26 | 25 | fsuppimpd 8282 |
. . . . 5
supp
|
27 | | gsumdixp.yf |
. . . . . 6
finSupp |
28 | 27 | fsuppimpd 8282 |
. . . . 5
supp
|
29 | | xpfi 8231 |
. . . . 5
supp
supp supp supp |
30 | 26, 28, 29 | syl2anc 693 |
. . . 4
supp supp |
31 | | ianor 509 |
. . . . . . 7
supp
supp supp
supp |
32 | | brxp 5147 |
. . . . . . 7
supp supp
supp supp |
33 | 31, 32 | xchnxbir 323 |
. . . . . 6
supp
supp
supp
supp |
34 | | simprl 794 |
. . . . . . . . . . 11
|
35 | | eldif 3584 |
. . . . . . . . . . . 12
supp
supp |
36 | 35 | biimpri 218 |
. . . . . . . . . . 11
supp
supp |
37 | 34, 36 | sylan 488 |
. . . . . . . . . 10
supp supp |
38 | 12 | adantr 481 |
. . . . . . . . . . 11
|
39 | | ssid 3624 |
. . . . . . . . . . . 12
supp
supp |
40 | 39 | a1i 11 |
. . . . . . . . . . 11
supp supp |
41 | 6 | adantr 481 |
. . . . . . . . . . 11
|
42 | | fvex 6201 |
. . . . . . . . . . . . 13
|
43 | 2, 42 | eqeltri 2697 |
. . . . . . . . . . . 12
|
44 | 43 | a1i 11 |
. . . . . . . . . . 11
|
45 | 38, 40, 41, 44 | suppssr 7326 |
. . . . . . . . . 10
supp |
46 | 37, 45 | syldan 487 |
. . . . . . . . 9
supp |
47 | 46 | oveq1d 6665 |
. . . . . . . 8
supp
|
48 | 1, 22, 2 | ringlz 18587 |
. . . . . . . . . 10
|
49 | 9, 21, 48 | syl2anc 693 |
. . . . . . . . 9
|
50 | 49 | adantr 481 |
. . . . . . . 8
supp |
51 | 47, 50 | eqtrd 2656 |
. . . . . . 7
supp |
52 | | simprr 796 |
. . . . . . . . . . 11
|
53 | | eldif 3584 |
. . . . . . . . . . . 12
supp
supp |
54 | 53 | biimpri 218 |
. . . . . . . . . . 11
supp
supp |
55 | 52, 54 | sylan 488 |
. . . . . . . . . 10
supp supp |
56 | 18 | adantr 481 |
. . . . . . . . . . 11
|
57 | | ssid 3624 |
. . . . . . . . . . . 12
supp
supp |
58 | 57 | a1i 11 |
. . . . . . . . . . 11
supp supp |
59 | 7 | adantr 481 |
. . . . . . . . . . 11
|
60 | 56, 58, 59, 44 | suppssr 7326 |
. . . . . . . . . 10
supp |
61 | 55, 60 | syldan 487 |
. . . . . . . . 9
supp |
62 | 61 | oveq2d 6666 |
. . . . . . . 8
supp |
63 | 1, 22, 2 | ringrz 18588 |
. . . . . . . . . 10
|
64 | 9, 15, 63 | syl2anc 693 |
. . . . . . . . 9
|
65 | 64 | adantr 481 |
. . . . . . . 8
supp
|
66 | 62, 65 | eqtrd 2656 |
. . . . . . 7
supp |
67 | 51, 66 | jaodan 826 |
. . . . . 6
supp
supp |
68 | 33, 67 | sylan2b 492 |
. . . . 5
supp supp |
69 | 68 | anasss 679 |
. . . 4
supp supp
|
70 | 1, 2, 5, 6, 8, 24,
30, 69 | gsum2d2 18373 |
. . 3
g
g g |
71 | | nffvmpt1 6199 |
. . . . . . 7
|
72 | | nfcv 2764 |
. . . . . . 7
|
73 | | nfcv 2764 |
. . . . . . 7
|
74 | 71, 72, 73 | nfov 6676 |
. . . . . 6
|
75 | | nfcv 2764 |
. . . . . . 7
|
76 | | nfcv 2764 |
. . . . . . 7
|
77 | | nffvmpt1 6199 |
. . . . . . 7
|
78 | 75, 76, 77 | nfov 6676 |
. . . . . 6
|
79 | | nfcv 2764 |
. . . . . 6
|
80 | | nfcv 2764 |
. . . . . 6
|
81 | | fveq2 6191 |
. . . . . . 7
|
82 | | fveq2 6191 |
. . . . . . 7
|
83 | 81, 82 | oveqan12d 6669 |
. . . . . 6
|
84 | 74, 78, 79, 80, 83 | cbvmpt2 6734 |
. . . . 5
|
85 | | simp2 1062 |
. . . . . . . 8
|
86 | 10 | 3adant3 1081 |
. . . . . . . 8
|
87 | 11 | fvmpt2 6291 |
. . . . . . . 8
|
88 | 85, 86, 87 | syl2anc 693 |
. . . . . . 7
|
89 | | simp3 1063 |
. . . . . . . 8
|
90 | 16 | 3adant2 1080 |
. . . . . . . 8
|
91 | 17 | fvmpt2 6291 |
. . . . . . . 8
|
92 | 89, 90, 91 | syl2anc 693 |
. . . . . . 7
|
93 | 88, 92 | oveq12d 6668 |
. . . . . 6
|
94 | 93 | mpt2eq3dva 6719 |
. . . . 5
|
95 | 84, 94 | syl5eq 2668 |
. . . 4
|
96 | 95 | oveq2d 6666 |
. . 3
g
g
|
97 | | nfcv 2764 |
. . . . . . 7
|
98 | | nfcv 2764 |
. . . . . . 7
g |
99 | | nfcv 2764 |
. . . . . . . 8
|
100 | 99, 74 | nfmpt 4746 |
. . . . . . 7
|
101 | 97, 98, 100 | nfov 6676 |
. . . . . 6
g |
102 | | nfcv 2764 |
. . . . . 6
g |
103 | 81 | oveq1d 6665 |
. . . . . . . . 9
|
104 | 103 | mpteq2dv 4745 |
. . . . . . . 8
|
105 | | nfcv 2764 |
. . . . . . . . . 10
|
106 | 105, 76, 77 | nfov 6676 |
. . . . . . . . 9
|
107 | 82 | oveq2d 6666 |
. . . . . . . . 9
|
108 | 106, 80, 107 | cbvmpt 4749 |
. . . . . . . 8
|
109 | 104, 108 | syl6eq 2672 |
. . . . . . 7
|
110 | 109 | oveq2d 6666 |
. . . . . 6
g g |
111 | 101, 102,
110 | cbvmpt 4749 |
. . . . 5
g g |
112 | 93 | 3expa 1265 |
. . . . . . . 8
|
113 | 112 | mpteq2dva 4744 |
. . . . . . 7
|
114 | 113 | oveq2d 6666 |
. . . . . 6
g g |
115 | 114 | mpteq2dva 4744 |
. . . . 5
g g |
116 | 111, 115 | syl5eq 2668 |
. . . 4
g g |
117 | 116 | oveq2d 6666 |
. . 3
g g g g |
118 | 70, 96, 117 | 3eqtr3d 2664 |
. 2
g
g g |
119 | | eqid 2622 |
. . . . 5
|
120 | 3 | adantr 481 |
. . . . 5
|
121 | 7 | adantr 481 |
. . . . 5
|
122 | 16 | adantlr 751 |
. . . . 5
|
123 | 27 | adantr 481 |
. . . . 5
finSupp
|
124 | 1, 2, 119, 22, 120, 121, 10, 122, 123 | gsummulc2 18607 |
. . . 4
g g |
125 | 124 | mpteq2dva 4744 |
. . 3
g
g |
126 | 125 | oveq2d 6666 |
. 2
g g g
g |
127 | 1, 2, 5, 7, 18, 27 | gsumcl 18316 |
. . 3
g |
128 | 1, 2, 119, 22, 3, 6, 127, 10, 25 | gsummulc1 18606 |
. 2
g g g
g |
129 | 118, 126,
128 | 3eqtrrd 2661 |
1
g g g |