Step |
Hyp |
Ref |
Expression |
1 |
|
gsumbagdiag.d |
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |
2 |
|
gsumbagdiag.s |
|- S = { y e. D | y oR <_ F } |
3 |
|
gsumbagdiag.f |
|- ( ph -> F e. D ) |
4 |
|
gsumbagdiag.b |
|- B = ( Base ` G ) |
5 |
|
gsumbagdiag.g |
|- ( ph -> G e. CMnd ) |
6 |
|
gsumbagdiag.x |
|- ( ( ph /\ ( j e. S /\ k e. { x e. D | x oR <_ ( F oF - j ) } ) ) -> X e. B ) |
7 |
|
psrass1lem.y |
|- ( k = ( n oF - j ) -> X = Y ) |
8 |
1 2 3
|
gsumbagdiaglem |
|- ( ( ph /\ ( m e. S /\ j e. { x e. D | x oR <_ ( F oF - m ) } ) ) -> ( j e. S /\ m e. { x e. D | x oR <_ ( F oF - j ) } ) ) |
9 |
6
|
anassrs |
|- ( ( ( ph /\ j e. S ) /\ k e. { x e. D | x oR <_ ( F oF - j ) } ) -> X e. B ) |
10 |
9
|
fmpttd |
|- ( ( ph /\ j e. S ) -> ( k e. { x e. D | x oR <_ ( F oF - j ) } |-> X ) : { x e. D | x oR <_ ( F oF - j ) } --> B ) |
11 |
2
|
ssrab3 |
|- S C_ D |
12 |
1 2
|
psrbagconcl |
|- ( ( F e. D /\ j e. S ) -> ( F oF - j ) e. S ) |
13 |
3 12
|
sylan |
|- ( ( ph /\ j e. S ) -> ( F oF - j ) e. S ) |
14 |
11 13
|
sselid |
|- ( ( ph /\ j e. S ) -> ( F oF - j ) e. D ) |
15 |
|
eqid |
|- { x e. D | x oR <_ ( F oF - j ) } = { x e. D | x oR <_ ( F oF - j ) } |
16 |
1 15
|
psrbagconf1o |
|- ( ( F oF - j ) e. D -> ( m e. { x e. D | x oR <_ ( F oF - j ) } |-> ( ( F oF - j ) oF - m ) ) : { x e. D | x oR <_ ( F oF - j ) } -1-1-onto-> { x e. D | x oR <_ ( F oF - j ) } ) |
17 |
14 16
|
syl |
|- ( ( ph /\ j e. S ) -> ( m e. { x e. D | x oR <_ ( F oF - j ) } |-> ( ( F oF - j ) oF - m ) ) : { x e. D | x oR <_ ( F oF - j ) } -1-1-onto-> { x e. D | x oR <_ ( F oF - j ) } ) |
18 |
|
f1of |
|- ( ( m e. { x e. D | x oR <_ ( F oF - j ) } |-> ( ( F oF - j ) oF - m ) ) : { x e. D | x oR <_ ( F oF - j ) } -1-1-onto-> { x e. D | x oR <_ ( F oF - j ) } -> ( m e. { x e. D | x oR <_ ( F oF - j ) } |-> ( ( F oF - j ) oF - m ) ) : { x e. D | x oR <_ ( F oF - j ) } --> { x e. D | x oR <_ ( F oF - j ) } ) |
19 |
17 18
|
syl |
|- ( ( ph /\ j e. S ) -> ( m e. { x e. D | x oR <_ ( F oF - j ) } |-> ( ( F oF - j ) oF - m ) ) : { x e. D | x oR <_ ( F oF - j ) } --> { x e. D | x oR <_ ( F oF - j ) } ) |
20 |
10 19
|
fcod |
|- ( ( ph /\ j e. S ) -> ( ( k e. { x e. D | x oR <_ ( F oF - j ) } |-> X ) o. ( m e. { x e. D | x oR <_ ( F oF - j ) } |-> ( ( F oF - j ) oF - m ) ) ) : { x e. D | x oR <_ ( F oF - j ) } --> B ) |
21 |
3
|
adantr |
|- ( ( ph /\ j e. S ) -> F e. D ) |
22 |
21
|
adantr |
|- ( ( ( ph /\ j e. S ) /\ m e. { x e. D | x oR <_ ( F oF - j ) } ) -> F e. D ) |
23 |
1
|
psrbagf |
|- ( F e. D -> F : I --> NN0 ) |
24 |
22 23
|
syl |
|- ( ( ( ph /\ j e. S ) /\ m e. { x e. D | x oR <_ ( F oF - j ) } ) -> F : I --> NN0 ) |
25 |
24
|
ffvelrnda |
|- ( ( ( ( ph /\ j e. S ) /\ m e. { x e. D | x oR <_ ( F oF - j ) } ) /\ z e. I ) -> ( F ` z ) e. NN0 ) |
26 |
|
simplr |
|- ( ( ( ph /\ j e. S ) /\ m e. { x e. D | x oR <_ ( F oF - j ) } ) -> j e. S ) |
27 |
11 26
|
sselid |
|- ( ( ( ph /\ j e. S ) /\ m e. { x e. D | x oR <_ ( F oF - j ) } ) -> j e. D ) |
28 |
1
|
psrbagf |
|- ( j e. D -> j : I --> NN0 ) |
29 |
27 28
|
syl |
|- ( ( ( ph /\ j e. S ) /\ m e. { x e. D | x oR <_ ( F oF - j ) } ) -> j : I --> NN0 ) |
30 |
29
|
ffvelrnda |
|- ( ( ( ( ph /\ j e. S ) /\ m e. { x e. D | x oR <_ ( F oF - j ) } ) /\ z e. I ) -> ( j ` z ) e. NN0 ) |
31 |
|
ssrab2 |
|- { x e. D | x oR <_ ( F oF - j ) } C_ D |
32 |
|
simpr |
|- ( ( ( ph /\ j e. S ) /\ m e. { x e. D | x oR <_ ( F oF - j ) } ) -> m e. { x e. D | x oR <_ ( F oF - j ) } ) |
33 |
31 32
|
sselid |
|- ( ( ( ph /\ j e. S ) /\ m e. { x e. D | x oR <_ ( F oF - j ) } ) -> m e. D ) |
34 |
1
|
psrbagf |
|- ( m e. D -> m : I --> NN0 ) |
35 |
33 34
|
syl |
|- ( ( ( ph /\ j e. S ) /\ m e. { x e. D | x oR <_ ( F oF - j ) } ) -> m : I --> NN0 ) |
36 |
35
|
ffvelrnda |
|- ( ( ( ( ph /\ j e. S ) /\ m e. { x e. D | x oR <_ ( F oF - j ) } ) /\ z e. I ) -> ( m ` z ) e. NN0 ) |
37 |
|
nn0cn |
|- ( ( F ` z ) e. NN0 -> ( F ` z ) e. CC ) |
38 |
|
nn0cn |
|- ( ( j ` z ) e. NN0 -> ( j ` z ) e. CC ) |
39 |
|
nn0cn |
|- ( ( m ` z ) e. NN0 -> ( m ` z ) e. CC ) |
40 |
|
sub32 |
|- ( ( ( F ` z ) e. CC /\ ( j ` z ) e. CC /\ ( m ` z ) e. CC ) -> ( ( ( F ` z ) - ( j ` z ) ) - ( m ` z ) ) = ( ( ( F ` z ) - ( m ` z ) ) - ( j ` z ) ) ) |
41 |
37 38 39 40
|
syl3an |
|- ( ( ( F ` z ) e. NN0 /\ ( j ` z ) e. NN0 /\ ( m ` z ) e. NN0 ) -> ( ( ( F ` z ) - ( j ` z ) ) - ( m ` z ) ) = ( ( ( F ` z ) - ( m ` z ) ) - ( j ` z ) ) ) |
42 |
25 30 36 41
|
syl3anc |
|- ( ( ( ( ph /\ j e. S ) /\ m e. { x e. D | x oR <_ ( F oF - j ) } ) /\ z e. I ) -> ( ( ( F ` z ) - ( j ` z ) ) - ( m ` z ) ) = ( ( ( F ` z ) - ( m ` z ) ) - ( j ` z ) ) ) |
43 |
42
|
mpteq2dva |
|- ( ( ( ph /\ j e. S ) /\ m e. { x e. D | x oR <_ ( F oF - j ) } ) -> ( z e. I |-> ( ( ( F ` z ) - ( j ` z ) ) - ( m ` z ) ) ) = ( z e. I |-> ( ( ( F ` z ) - ( m ` z ) ) - ( j ` z ) ) ) ) |
44 |
35
|
ffnd |
|- ( ( ( ph /\ j e. S ) /\ m e. { x e. D | x oR <_ ( F oF - j ) } ) -> m Fn I ) |
45 |
32 44
|
fndmexd |
|- ( ( ( ph /\ j e. S ) /\ m e. { x e. D | x oR <_ ( F oF - j ) } ) -> I e. _V ) |
46 |
|
ovexd |
|- ( ( ( ( ph /\ j e. S ) /\ m e. { x e. D | x oR <_ ( F oF - j ) } ) /\ z e. I ) -> ( ( F ` z ) - ( j ` z ) ) e. _V ) |
47 |
24
|
feqmptd |
|- ( ( ( ph /\ j e. S ) /\ m e. { x e. D | x oR <_ ( F oF - j ) } ) -> F = ( z e. I |-> ( F ` z ) ) ) |
48 |
29
|
feqmptd |
|- ( ( ( ph /\ j e. S ) /\ m e. { x e. D | x oR <_ ( F oF - j ) } ) -> j = ( z e. I |-> ( j ` z ) ) ) |
49 |
45 25 30 47 48
|
offval2 |
|- ( ( ( ph /\ j e. S ) /\ m e. { x e. D | x oR <_ ( F oF - j ) } ) -> ( F oF - j ) = ( z e. I |-> ( ( F ` z ) - ( j ` z ) ) ) ) |
50 |
35
|
feqmptd |
|- ( ( ( ph /\ j e. S ) /\ m e. { x e. D | x oR <_ ( F oF - j ) } ) -> m = ( z e. I |-> ( m ` z ) ) ) |
51 |
45 46 36 49 50
|
offval2 |
|- ( ( ( ph /\ j e. S ) /\ m e. { x e. D | x oR <_ ( F oF - j ) } ) -> ( ( F oF - j ) oF - m ) = ( z e. I |-> ( ( ( F ` z ) - ( j ` z ) ) - ( m ` z ) ) ) ) |
52 |
|
ovexd |
|- ( ( ( ( ph /\ j e. S ) /\ m e. { x e. D | x oR <_ ( F oF - j ) } ) /\ z e. I ) -> ( ( F ` z ) - ( m ` z ) ) e. _V ) |
53 |
45 25 36 47 50
|
offval2 |
|- ( ( ( ph /\ j e. S ) /\ m e. { x e. D | x oR <_ ( F oF - j ) } ) -> ( F oF - m ) = ( z e. I |-> ( ( F ` z ) - ( m ` z ) ) ) ) |
54 |
45 52 30 53 48
|
offval2 |
|- ( ( ( ph /\ j e. S ) /\ m e. { x e. D | x oR <_ ( F oF - j ) } ) -> ( ( F oF - m ) oF - j ) = ( z e. I |-> ( ( ( F ` z ) - ( m ` z ) ) - ( j ` z ) ) ) ) |
55 |
43 51 54
|
3eqtr4d |
|- ( ( ( ph /\ j e. S ) /\ m e. { x e. D | x oR <_ ( F oF - j ) } ) -> ( ( F oF - j ) oF - m ) = ( ( F oF - m ) oF - j ) ) |
56 |
1 15
|
psrbagconcl |
|- ( ( ( F oF - j ) e. D /\ m e. { x e. D | x oR <_ ( F oF - j ) } ) -> ( ( F oF - j ) oF - m ) e. { x e. D | x oR <_ ( F oF - j ) } ) |
57 |
14 56
|
sylan |
|- ( ( ( ph /\ j e. S ) /\ m e. { x e. D | x oR <_ ( F oF - j ) } ) -> ( ( F oF - j ) oF - m ) e. { x e. D | x oR <_ ( F oF - j ) } ) |
58 |
55 57
|
eqeltrrd |
|- ( ( ( ph /\ j e. S ) /\ m e. { x e. D | x oR <_ ( F oF - j ) } ) -> ( ( F oF - m ) oF - j ) e. { x e. D | x oR <_ ( F oF - j ) } ) |
59 |
55
|
mpteq2dva |
|- ( ( ph /\ j e. S ) -> ( m e. { x e. D | x oR <_ ( F oF - j ) } |-> ( ( F oF - j ) oF - m ) ) = ( m e. { x e. D | x oR <_ ( F oF - j ) } |-> ( ( F oF - m ) oF - j ) ) ) |
60 |
|
nfcv |
|- F/_ n X |
61 |
|
nfcsb1v |
|- F/_ k [_ n / k ]_ X |
62 |
|
csbeq1a |
|- ( k = n -> X = [_ n / k ]_ X ) |
63 |
60 61 62
|
cbvmpt |
|- ( k e. { x e. D | x oR <_ ( F oF - j ) } |-> X ) = ( n e. { x e. D | x oR <_ ( F oF - j ) } |-> [_ n / k ]_ X ) |
64 |
63
|
a1i |
|- ( ( ph /\ j e. S ) -> ( k e. { x e. D | x oR <_ ( F oF - j ) } |-> X ) = ( n e. { x e. D | x oR <_ ( F oF - j ) } |-> [_ n / k ]_ X ) ) |
65 |
|
csbeq1 |
|- ( n = ( ( F oF - m ) oF - j ) -> [_ n / k ]_ X = [_ ( ( F oF - m ) oF - j ) / k ]_ X ) |
66 |
58 59 64 65
|
fmptco |
|- ( ( ph /\ j e. S ) -> ( ( k e. { x e. D | x oR <_ ( F oF - j ) } |-> X ) o. ( m e. { x e. D | x oR <_ ( F oF - j ) } |-> ( ( F oF - j ) oF - m ) ) ) = ( m e. { x e. D | x oR <_ ( F oF - j ) } |-> [_ ( ( F oF - m ) oF - j ) / k ]_ X ) ) |
67 |
66
|
feq1d |
|- ( ( ph /\ j e. S ) -> ( ( ( k e. { x e. D | x oR <_ ( F oF - j ) } |-> X ) o. ( m e. { x e. D | x oR <_ ( F oF - j ) } |-> ( ( F oF - j ) oF - m ) ) ) : { x e. D | x oR <_ ( F oF - j ) } --> B <-> ( m e. { x e. D | x oR <_ ( F oF - j ) } |-> [_ ( ( F oF - m ) oF - j ) / k ]_ X ) : { x e. D | x oR <_ ( F oF - j ) } --> B ) ) |
68 |
20 67
|
mpbid |
|- ( ( ph /\ j e. S ) -> ( m e. { x e. D | x oR <_ ( F oF - j ) } |-> [_ ( ( F oF - m ) oF - j ) / k ]_ X ) : { x e. D | x oR <_ ( F oF - j ) } --> B ) |
69 |
68
|
fvmptelrn |
|- ( ( ( ph /\ j e. S ) /\ m e. { x e. D | x oR <_ ( F oF - j ) } ) -> [_ ( ( F oF - m ) oF - j ) / k ]_ X e. B ) |
70 |
69
|
anasss |
|- ( ( ph /\ ( j e. S /\ m e. { x e. D | x oR <_ ( F oF - j ) } ) ) -> [_ ( ( F oF - m ) oF - j ) / k ]_ X e. B ) |
71 |
8 70
|
syldan |
|- ( ( ph /\ ( m e. S /\ j e. { x e. D | x oR <_ ( F oF - m ) } ) ) -> [_ ( ( F oF - m ) oF - j ) / k ]_ X e. B ) |
72 |
1 2 3 4 5 71
|
gsumbagdiag |
|- ( ph -> ( G gsum ( m e. S , j e. { x e. D | x oR <_ ( F oF - m ) } |-> [_ ( ( F oF - m ) oF - j ) / k ]_ X ) ) = ( G gsum ( j e. S , m e. { x e. D | x oR <_ ( F oF - j ) } |-> [_ ( ( F oF - m ) oF - j ) / k ]_ X ) ) ) |
73 |
|
eqid |
|- ( 0g ` G ) = ( 0g ` G ) |
74 |
1
|
psrbaglefi |
|- ( F e. D -> { y e. D | y oR <_ F } e. Fin ) |
75 |
3 74
|
syl |
|- ( ph -> { y e. D | y oR <_ F } e. Fin ) |
76 |
2 75
|
eqeltrid |
|- ( ph -> S e. Fin ) |
77 |
1 2
|
psrbagconcl |
|- ( ( F e. D /\ m e. S ) -> ( F oF - m ) e. S ) |
78 |
3 77
|
sylan |
|- ( ( ph /\ m e. S ) -> ( F oF - m ) e. S ) |
79 |
11 78
|
sselid |
|- ( ( ph /\ m e. S ) -> ( F oF - m ) e. D ) |
80 |
1
|
psrbaglefi |
|- ( ( F oF - m ) e. D -> { x e. D | x oR <_ ( F oF - m ) } e. Fin ) |
81 |
79 80
|
syl |
|- ( ( ph /\ m e. S ) -> { x e. D | x oR <_ ( F oF - m ) } e. Fin ) |
82 |
|
xpfi |
|- ( ( S e. Fin /\ S e. Fin ) -> ( S X. S ) e. Fin ) |
83 |
76 76 82
|
syl2anc |
|- ( ph -> ( S X. S ) e. Fin ) |
84 |
|
simprl |
|- ( ( ph /\ ( m e. S /\ j e. { x e. D | x oR <_ ( F oF - m ) } ) ) -> m e. S ) |
85 |
8
|
simpld |
|- ( ( ph /\ ( m e. S /\ j e. { x e. D | x oR <_ ( F oF - m ) } ) ) -> j e. S ) |
86 |
|
brxp |
|- ( m ( S X. S ) j <-> ( m e. S /\ j e. S ) ) |
87 |
84 85 86
|
sylanbrc |
|- ( ( ph /\ ( m e. S /\ j e. { x e. D | x oR <_ ( F oF - m ) } ) ) -> m ( S X. S ) j ) |
88 |
87
|
pm2.24d |
|- ( ( ph /\ ( m e. S /\ j e. { x e. D | x oR <_ ( F oF - m ) } ) ) -> ( -. m ( S X. S ) j -> [_ ( ( F oF - m ) oF - j ) / k ]_ X = ( 0g ` G ) ) ) |
89 |
88
|
impr |
|- ( ( ph /\ ( ( m e. S /\ j e. { x e. D | x oR <_ ( F oF - m ) } ) /\ -. m ( S X. S ) j ) ) -> [_ ( ( F oF - m ) oF - j ) / k ]_ X = ( 0g ` G ) ) |
90 |
4 73 5 76 81 71 83 89
|
gsum2d2 |
|- ( ph -> ( G gsum ( m e. S , j e. { x e. D | x oR <_ ( F oF - m ) } |-> [_ ( ( F oF - m ) oF - j ) / k ]_ X ) ) = ( G gsum ( m e. S |-> ( G gsum ( j e. { x e. D | x oR <_ ( F oF - m ) } |-> [_ ( ( F oF - m ) oF - j ) / k ]_ X ) ) ) ) ) |
91 |
1
|
psrbaglefi |
|- ( ( F oF - j ) e. D -> { x e. D | x oR <_ ( F oF - j ) } e. Fin ) |
92 |
14 91
|
syl |
|- ( ( ph /\ j e. S ) -> { x e. D | x oR <_ ( F oF - j ) } e. Fin ) |
93 |
|
simprl |
|- ( ( ph /\ ( j e. S /\ m e. { x e. D | x oR <_ ( F oF - j ) } ) ) -> j e. S ) |
94 |
1 2 3
|
gsumbagdiaglem |
|- ( ( ph /\ ( j e. S /\ m e. { x e. D | x oR <_ ( F oF - j ) } ) ) -> ( m e. S /\ j e. { x e. D | x oR <_ ( F oF - m ) } ) ) |
95 |
94
|
simpld |
|- ( ( ph /\ ( j e. S /\ m e. { x e. D | x oR <_ ( F oF - j ) } ) ) -> m e. S ) |
96 |
|
brxp |
|- ( j ( S X. S ) m <-> ( j e. S /\ m e. S ) ) |
97 |
93 95 96
|
sylanbrc |
|- ( ( ph /\ ( j e. S /\ m e. { x e. D | x oR <_ ( F oF - j ) } ) ) -> j ( S X. S ) m ) |
98 |
97
|
pm2.24d |
|- ( ( ph /\ ( j e. S /\ m e. { x e. D | x oR <_ ( F oF - j ) } ) ) -> ( -. j ( S X. S ) m -> [_ ( ( F oF - m ) oF - j ) / k ]_ X = ( 0g ` G ) ) ) |
99 |
98
|
impr |
|- ( ( ph /\ ( ( j e. S /\ m e. { x e. D | x oR <_ ( F oF - j ) } ) /\ -. j ( S X. S ) m ) ) -> [_ ( ( F oF - m ) oF - j ) / k ]_ X = ( 0g ` G ) ) |
100 |
4 73 5 76 92 70 83 99
|
gsum2d2 |
|- ( ph -> ( G gsum ( j e. S , m e. { x e. D | x oR <_ ( F oF - j ) } |-> [_ ( ( F oF - m ) oF - j ) / k ]_ X ) ) = ( G gsum ( j e. S |-> ( G gsum ( m e. { x e. D | x oR <_ ( F oF - j ) } |-> [_ ( ( F oF - m ) oF - j ) / k ]_ X ) ) ) ) ) |
101 |
72 90 100
|
3eqtr3d |
|- ( ph -> ( G gsum ( m e. S |-> ( G gsum ( j e. { x e. D | x oR <_ ( F oF - m ) } |-> [_ ( ( F oF - m ) oF - j ) / k ]_ X ) ) ) ) = ( G gsum ( j e. S |-> ( G gsum ( m e. { x e. D | x oR <_ ( F oF - j ) } |-> [_ ( ( F oF - m ) oF - j ) / k ]_ X ) ) ) ) ) |
102 |
5
|
adantr |
|- ( ( ph /\ m e. S ) -> G e. CMnd ) |
103 |
71
|
anassrs |
|- ( ( ( ph /\ m e. S ) /\ j e. { x e. D | x oR <_ ( F oF - m ) } ) -> [_ ( ( F oF - m ) oF - j ) / k ]_ X e. B ) |
104 |
103
|
fmpttd |
|- ( ( ph /\ m e. S ) -> ( j e. { x e. D | x oR <_ ( F oF - m ) } |-> [_ ( ( F oF - m ) oF - j ) / k ]_ X ) : { x e. D | x oR <_ ( F oF - m ) } --> B ) |
105 |
|
ovex |
|- ( NN0 ^m I ) e. _V |
106 |
1 105
|
rabex2 |
|- D e. _V |
107 |
106
|
a1i |
|- ( ( ph /\ m e. S ) -> D e. _V ) |
108 |
|
rabexg |
|- ( D e. _V -> { x e. D | x oR <_ ( F oF - m ) } e. _V ) |
109 |
|
mptexg |
|- ( { x e. D | x oR <_ ( F oF - m ) } e. _V -> ( j e. { x e. D | x oR <_ ( F oF - m ) } |-> [_ ( ( F oF - m ) oF - j ) / k ]_ X ) e. _V ) |
110 |
107 108 109
|
3syl |
|- ( ( ph /\ m e. S ) -> ( j e. { x e. D | x oR <_ ( F oF - m ) } |-> [_ ( ( F oF - m ) oF - j ) / k ]_ X ) e. _V ) |
111 |
|
funmpt |
|- Fun ( j e. { x e. D | x oR <_ ( F oF - m ) } |-> [_ ( ( F oF - m ) oF - j ) / k ]_ X ) |
112 |
111
|
a1i |
|- ( ( ph /\ m e. S ) -> Fun ( j e. { x e. D | x oR <_ ( F oF - m ) } |-> [_ ( ( F oF - m ) oF - j ) / k ]_ X ) ) |
113 |
|
fvexd |
|- ( ( ph /\ m e. S ) -> ( 0g ` G ) e. _V ) |
114 |
|
suppssdm |
|- ( ( j e. { x e. D | x oR <_ ( F oF - m ) } |-> [_ ( ( F oF - m ) oF - j ) / k ]_ X ) supp ( 0g ` G ) ) C_ dom ( j e. { x e. D | x oR <_ ( F oF - m ) } |-> [_ ( ( F oF - m ) oF - j ) / k ]_ X ) |
115 |
|
eqid |
|- ( j e. { x e. D | x oR <_ ( F oF - m ) } |-> [_ ( ( F oF - m ) oF - j ) / k ]_ X ) = ( j e. { x e. D | x oR <_ ( F oF - m ) } |-> [_ ( ( F oF - m ) oF - j ) / k ]_ X ) |
116 |
115
|
dmmptss |
|- dom ( j e. { x e. D | x oR <_ ( F oF - m ) } |-> [_ ( ( F oF - m ) oF - j ) / k ]_ X ) C_ { x e. D | x oR <_ ( F oF - m ) } |
117 |
114 116
|
sstri |
|- ( ( j e. { x e. D | x oR <_ ( F oF - m ) } |-> [_ ( ( F oF - m ) oF - j ) / k ]_ X ) supp ( 0g ` G ) ) C_ { x e. D | x oR <_ ( F oF - m ) } |
118 |
117
|
a1i |
|- ( ( ph /\ m e. S ) -> ( ( j e. { x e. D | x oR <_ ( F oF - m ) } |-> [_ ( ( F oF - m ) oF - j ) / k ]_ X ) supp ( 0g ` G ) ) C_ { x e. D | x oR <_ ( F oF - m ) } ) |
119 |
|
suppssfifsupp |
|- ( ( ( ( j e. { x e. D | x oR <_ ( F oF - m ) } |-> [_ ( ( F oF - m ) oF - j ) / k ]_ X ) e. _V /\ Fun ( j e. { x e. D | x oR <_ ( F oF - m ) } |-> [_ ( ( F oF - m ) oF - j ) / k ]_ X ) /\ ( 0g ` G ) e. _V ) /\ ( { x e. D | x oR <_ ( F oF - m ) } e. Fin /\ ( ( j e. { x e. D | x oR <_ ( F oF - m ) } |-> [_ ( ( F oF - m ) oF - j ) / k ]_ X ) supp ( 0g ` G ) ) C_ { x e. D | x oR <_ ( F oF - m ) } ) ) -> ( j e. { x e. D | x oR <_ ( F oF - m ) } |-> [_ ( ( F oF - m ) oF - j ) / k ]_ X ) finSupp ( 0g ` G ) ) |
120 |
110 112 113 81 118 119
|
syl32anc |
|- ( ( ph /\ m e. S ) -> ( j e. { x e. D | x oR <_ ( F oF - m ) } |-> [_ ( ( F oF - m ) oF - j ) / k ]_ X ) finSupp ( 0g ` G ) ) |
121 |
4 73 102 81 104 120
|
gsumcl |
|- ( ( ph /\ m e. S ) -> ( G gsum ( j e. { x e. D | x oR <_ ( F oF - m ) } |-> [_ ( ( F oF - m ) oF - j ) / k ]_ X ) ) e. B ) |
122 |
121
|
fmpttd |
|- ( ph -> ( m e. S |-> ( G gsum ( j e. { x e. D | x oR <_ ( F oF - m ) } |-> [_ ( ( F oF - m ) oF - j ) / k ]_ X ) ) ) : S --> B ) |
123 |
1 2
|
psrbagconf1o |
|- ( F e. D -> ( m e. S |-> ( F oF - m ) ) : S -1-1-onto-> S ) |
124 |
3 123
|
syl |
|- ( ph -> ( m e. S |-> ( F oF - m ) ) : S -1-1-onto-> S ) |
125 |
|
f1ocnv |
|- ( ( m e. S |-> ( F oF - m ) ) : S -1-1-onto-> S -> `' ( m e. S |-> ( F oF - m ) ) : S -1-1-onto-> S ) |
126 |
|
f1of |
|- ( `' ( m e. S |-> ( F oF - m ) ) : S -1-1-onto-> S -> `' ( m e. S |-> ( F oF - m ) ) : S --> S ) |
127 |
124 125 126
|
3syl |
|- ( ph -> `' ( m e. S |-> ( F oF - m ) ) : S --> S ) |
128 |
122 127
|
fcod |
|- ( ph -> ( ( m e. S |-> ( G gsum ( j e. { x e. D | x oR <_ ( F oF - m ) } |-> [_ ( ( F oF - m ) oF - j ) / k ]_ X ) ) ) o. `' ( m e. S |-> ( F oF - m ) ) ) : S --> B ) |
129 |
|
coass |
|- ( ( ( n e. S |-> ( G gsum ( j e. { x e. D | x oR <_ n } |-> Y ) ) ) o. ( m e. S |-> ( F oF - m ) ) ) o. `' ( m e. S |-> ( F oF - m ) ) ) = ( ( n e. S |-> ( G gsum ( j e. { x e. D | x oR <_ n } |-> Y ) ) ) o. ( ( m e. S |-> ( F oF - m ) ) o. `' ( m e. S |-> ( F oF - m ) ) ) ) |
130 |
|
f1ococnv2 |
|- ( ( m e. S |-> ( F oF - m ) ) : S -1-1-onto-> S -> ( ( m e. S |-> ( F oF - m ) ) o. `' ( m e. S |-> ( F oF - m ) ) ) = ( _I |` S ) ) |
131 |
124 130
|
syl |
|- ( ph -> ( ( m e. S |-> ( F oF - m ) ) o. `' ( m e. S |-> ( F oF - m ) ) ) = ( _I |` S ) ) |
132 |
131
|
coeq2d |
|- ( ph -> ( ( n e. S |-> ( G gsum ( j e. { x e. D | x oR <_ n } |-> Y ) ) ) o. ( ( m e. S |-> ( F oF - m ) ) o. `' ( m e. S |-> ( F oF - m ) ) ) ) = ( ( n e. S |-> ( G gsum ( j e. { x e. D | x oR <_ n } |-> Y ) ) ) o. ( _I |` S ) ) ) |
133 |
129 132
|
syl5eq |
|- ( ph -> ( ( ( n e. S |-> ( G gsum ( j e. { x e. D | x oR <_ n } |-> Y ) ) ) o. ( m e. S |-> ( F oF - m ) ) ) o. `' ( m e. S |-> ( F oF - m ) ) ) = ( ( n e. S |-> ( G gsum ( j e. { x e. D | x oR <_ n } |-> Y ) ) ) o. ( _I |` S ) ) ) |
134 |
|
eqidd |
|- ( ph -> ( m e. S |-> ( F oF - m ) ) = ( m e. S |-> ( F oF - m ) ) ) |
135 |
|
eqidd |
|- ( ph -> ( n e. S |-> ( G gsum ( j e. { x e. D | x oR <_ n } |-> Y ) ) ) = ( n e. S |-> ( G gsum ( j e. { x e. D | x oR <_ n } |-> Y ) ) ) ) |
136 |
|
breq2 |
|- ( n = ( F oF - m ) -> ( x oR <_ n <-> x oR <_ ( F oF - m ) ) ) |
137 |
136
|
rabbidv |
|- ( n = ( F oF - m ) -> { x e. D | x oR <_ n } = { x e. D | x oR <_ ( F oF - m ) } ) |
138 |
|
ovex |
|- ( n oF - j ) e. _V |
139 |
138 7
|
csbie |
|- [_ ( n oF - j ) / k ]_ X = Y |
140 |
|
oveq1 |
|- ( n = ( F oF - m ) -> ( n oF - j ) = ( ( F oF - m ) oF - j ) ) |
141 |
140
|
csbeq1d |
|- ( n = ( F oF - m ) -> [_ ( n oF - j ) / k ]_ X = [_ ( ( F oF - m ) oF - j ) / k ]_ X ) |
142 |
139 141
|
eqtr3id |
|- ( n = ( F oF - m ) -> Y = [_ ( ( F oF - m ) oF - j ) / k ]_ X ) |
143 |
137 142
|
mpteq12dv |
|- ( n = ( F oF - m ) -> ( j e. { x e. D | x oR <_ n } |-> Y ) = ( j e. { x e. D | x oR <_ ( F oF - m ) } |-> [_ ( ( F oF - m ) oF - j ) / k ]_ X ) ) |
144 |
143
|
oveq2d |
|- ( n = ( F oF - m ) -> ( G gsum ( j e. { x e. D | x oR <_ n } |-> Y ) ) = ( G gsum ( j e. { x e. D | x oR <_ ( F oF - m ) } |-> [_ ( ( F oF - m ) oF - j ) / k ]_ X ) ) ) |
145 |
78 134 135 144
|
fmptco |
|- ( ph -> ( ( n e. S |-> ( G gsum ( j e. { x e. D | x oR <_ n } |-> Y ) ) ) o. ( m e. S |-> ( F oF - m ) ) ) = ( m e. S |-> ( G gsum ( j e. { x e. D | x oR <_ ( F oF - m ) } |-> [_ ( ( F oF - m ) oF - j ) / k ]_ X ) ) ) ) |
146 |
145
|
coeq1d |
|- ( ph -> ( ( ( n e. S |-> ( G gsum ( j e. { x e. D | x oR <_ n } |-> Y ) ) ) o. ( m e. S |-> ( F oF - m ) ) ) o. `' ( m e. S |-> ( F oF - m ) ) ) = ( ( m e. S |-> ( G gsum ( j e. { x e. D | x oR <_ ( F oF - m ) } |-> [_ ( ( F oF - m ) oF - j ) / k ]_ X ) ) ) o. `' ( m e. S |-> ( F oF - m ) ) ) ) |
147 |
|
coires1 |
|- ( ( n e. S |-> ( G gsum ( j e. { x e. D | x oR <_ n } |-> Y ) ) ) o. ( _I |` S ) ) = ( ( n e. S |-> ( G gsum ( j e. { x e. D | x oR <_ n } |-> Y ) ) ) |` S ) |
148 |
|
ssid |
|- S C_ S |
149 |
|
resmpt |
|- ( S C_ S -> ( ( n e. S |-> ( G gsum ( j e. { x e. D | x oR <_ n } |-> Y ) ) ) |` S ) = ( n e. S |-> ( G gsum ( j e. { x e. D | x oR <_ n } |-> Y ) ) ) ) |
150 |
148 149
|
ax-mp |
|- ( ( n e. S |-> ( G gsum ( j e. { x e. D | x oR <_ n } |-> Y ) ) ) |` S ) = ( n e. S |-> ( G gsum ( j e. { x e. D | x oR <_ n } |-> Y ) ) ) |
151 |
147 150
|
eqtri |
|- ( ( n e. S |-> ( G gsum ( j e. { x e. D | x oR <_ n } |-> Y ) ) ) o. ( _I |` S ) ) = ( n e. S |-> ( G gsum ( j e. { x e. D | x oR <_ n } |-> Y ) ) ) |
152 |
151
|
a1i |
|- ( ph -> ( ( n e. S |-> ( G gsum ( j e. { x e. D | x oR <_ n } |-> Y ) ) ) o. ( _I |` S ) ) = ( n e. S |-> ( G gsum ( j e. { x e. D | x oR <_ n } |-> Y ) ) ) ) |
153 |
133 146 152
|
3eqtr3d |
|- ( ph -> ( ( m e. S |-> ( G gsum ( j e. { x e. D | x oR <_ ( F oF - m ) } |-> [_ ( ( F oF - m ) oF - j ) / k ]_ X ) ) ) o. `' ( m e. S |-> ( F oF - m ) ) ) = ( n e. S |-> ( G gsum ( j e. { x e. D | x oR <_ n } |-> Y ) ) ) ) |
154 |
153
|
feq1d |
|- ( ph -> ( ( ( m e. S |-> ( G gsum ( j e. { x e. D | x oR <_ ( F oF - m ) } |-> [_ ( ( F oF - m ) oF - j ) / k ]_ X ) ) ) o. `' ( m e. S |-> ( F oF - m ) ) ) : S --> B <-> ( n e. S |-> ( G gsum ( j e. { x e. D | x oR <_ n } |-> Y ) ) ) : S --> B ) ) |
155 |
128 154
|
mpbid |
|- ( ph -> ( n e. S |-> ( G gsum ( j e. { x e. D | x oR <_ n } |-> Y ) ) ) : S --> B ) |
156 |
|
rabexg |
|- ( D e. _V -> { y e. D | y oR <_ F } e. _V ) |
157 |
106 156
|
mp1i |
|- ( ph -> { y e. D | y oR <_ F } e. _V ) |
158 |
2 157
|
eqeltrid |
|- ( ph -> S e. _V ) |
159 |
158
|
mptexd |
|- ( ph -> ( n e. S |-> ( G gsum ( j e. { x e. D | x oR <_ n } |-> Y ) ) ) e. _V ) |
160 |
|
funmpt |
|- Fun ( n e. S |-> ( G gsum ( j e. { x e. D | x oR <_ n } |-> Y ) ) ) |
161 |
160
|
a1i |
|- ( ph -> Fun ( n e. S |-> ( G gsum ( j e. { x e. D | x oR <_ n } |-> Y ) ) ) ) |
162 |
|
fvexd |
|- ( ph -> ( 0g ` G ) e. _V ) |
163 |
|
suppssdm |
|- ( ( n e. S |-> ( G gsum ( j e. { x e. D | x oR <_ n } |-> Y ) ) ) supp ( 0g ` G ) ) C_ dom ( n e. S |-> ( G gsum ( j e. { x e. D | x oR <_ n } |-> Y ) ) ) |
164 |
|
eqid |
|- ( n e. S |-> ( G gsum ( j e. { x e. D | x oR <_ n } |-> Y ) ) ) = ( n e. S |-> ( G gsum ( j e. { x e. D | x oR <_ n } |-> Y ) ) ) |
165 |
164
|
dmmptss |
|- dom ( n e. S |-> ( G gsum ( j e. { x e. D | x oR <_ n } |-> Y ) ) ) C_ S |
166 |
163 165
|
sstri |
|- ( ( n e. S |-> ( G gsum ( j e. { x e. D | x oR <_ n } |-> Y ) ) ) supp ( 0g ` G ) ) C_ S |
167 |
166
|
a1i |
|- ( ph -> ( ( n e. S |-> ( G gsum ( j e. { x e. D | x oR <_ n } |-> Y ) ) ) supp ( 0g ` G ) ) C_ S ) |
168 |
|
suppssfifsupp |
|- ( ( ( ( n e. S |-> ( G gsum ( j e. { x e. D | x oR <_ n } |-> Y ) ) ) e. _V /\ Fun ( n e. S |-> ( G gsum ( j e. { x e. D | x oR <_ n } |-> Y ) ) ) /\ ( 0g ` G ) e. _V ) /\ ( S e. Fin /\ ( ( n e. S |-> ( G gsum ( j e. { x e. D | x oR <_ n } |-> Y ) ) ) supp ( 0g ` G ) ) C_ S ) ) -> ( n e. S |-> ( G gsum ( j e. { x e. D | x oR <_ n } |-> Y ) ) ) finSupp ( 0g ` G ) ) |
169 |
159 161 162 76 167 168
|
syl32anc |
|- ( ph -> ( n e. S |-> ( G gsum ( j e. { x e. D | x oR <_ n } |-> Y ) ) ) finSupp ( 0g ` G ) ) |
170 |
4 73 5 76 155 169 124
|
gsumf1o |
|- ( ph -> ( G gsum ( n e. S |-> ( G gsum ( j e. { x e. D | x oR <_ n } |-> Y ) ) ) ) = ( G gsum ( ( n e. S |-> ( G gsum ( j e. { x e. D | x oR <_ n } |-> Y ) ) ) o. ( m e. S |-> ( F oF - m ) ) ) ) ) |
171 |
145
|
oveq2d |
|- ( ph -> ( G gsum ( ( n e. S |-> ( G gsum ( j e. { x e. D | x oR <_ n } |-> Y ) ) ) o. ( m e. S |-> ( F oF - m ) ) ) ) = ( G gsum ( m e. S |-> ( G gsum ( j e. { x e. D | x oR <_ ( F oF - m ) } |-> [_ ( ( F oF - m ) oF - j ) / k ]_ X ) ) ) ) ) |
172 |
170 171
|
eqtrd |
|- ( ph -> ( G gsum ( n e. S |-> ( G gsum ( j e. { x e. D | x oR <_ n } |-> Y ) ) ) ) = ( G gsum ( m e. S |-> ( G gsum ( j e. { x e. D | x oR <_ ( F oF - m ) } |-> [_ ( ( F oF - m ) oF - j ) / k ]_ X ) ) ) ) ) |
173 |
5
|
adantr |
|- ( ( ph /\ j e. S ) -> G e. CMnd ) |
174 |
106
|
a1i |
|- ( ( ph /\ j e. S ) -> D e. _V ) |
175 |
|
rabexg |
|- ( D e. _V -> { x e. D | x oR <_ ( F oF - j ) } e. _V ) |
176 |
|
mptexg |
|- ( { x e. D | x oR <_ ( F oF - j ) } e. _V -> ( k e. { x e. D | x oR <_ ( F oF - j ) } |-> X ) e. _V ) |
177 |
174 175 176
|
3syl |
|- ( ( ph /\ j e. S ) -> ( k e. { x e. D | x oR <_ ( F oF - j ) } |-> X ) e. _V ) |
178 |
|
funmpt |
|- Fun ( k e. { x e. D | x oR <_ ( F oF - j ) } |-> X ) |
179 |
178
|
a1i |
|- ( ( ph /\ j e. S ) -> Fun ( k e. { x e. D | x oR <_ ( F oF - j ) } |-> X ) ) |
180 |
|
fvexd |
|- ( ( ph /\ j e. S ) -> ( 0g ` G ) e. _V ) |
181 |
|
suppssdm |
|- ( ( k e. { x e. D | x oR <_ ( F oF - j ) } |-> X ) supp ( 0g ` G ) ) C_ dom ( k e. { x e. D | x oR <_ ( F oF - j ) } |-> X ) |
182 |
|
eqid |
|- ( k e. { x e. D | x oR <_ ( F oF - j ) } |-> X ) = ( k e. { x e. D | x oR <_ ( F oF - j ) } |-> X ) |
183 |
182
|
dmmptss |
|- dom ( k e. { x e. D | x oR <_ ( F oF - j ) } |-> X ) C_ { x e. D | x oR <_ ( F oF - j ) } |
184 |
181 183
|
sstri |
|- ( ( k e. { x e. D | x oR <_ ( F oF - j ) } |-> X ) supp ( 0g ` G ) ) C_ { x e. D | x oR <_ ( F oF - j ) } |
185 |
184
|
a1i |
|- ( ( ph /\ j e. S ) -> ( ( k e. { x e. D | x oR <_ ( F oF - j ) } |-> X ) supp ( 0g ` G ) ) C_ { x e. D | x oR <_ ( F oF - j ) } ) |
186 |
|
suppssfifsupp |
|- ( ( ( ( k e. { x e. D | x oR <_ ( F oF - j ) } |-> X ) e. _V /\ Fun ( k e. { x e. D | x oR <_ ( F oF - j ) } |-> X ) /\ ( 0g ` G ) e. _V ) /\ ( { x e. D | x oR <_ ( F oF - j ) } e. Fin /\ ( ( k e. { x e. D | x oR <_ ( F oF - j ) } |-> X ) supp ( 0g ` G ) ) C_ { x e. D | x oR <_ ( F oF - j ) } ) ) -> ( k e. { x e. D | x oR <_ ( F oF - j ) } |-> X ) finSupp ( 0g ` G ) ) |
187 |
177 179 180 92 185 186
|
syl32anc |
|- ( ( ph /\ j e. S ) -> ( k e. { x e. D | x oR <_ ( F oF - j ) } |-> X ) finSupp ( 0g ` G ) ) |
188 |
4 73 173 92 10 187 17
|
gsumf1o |
|- ( ( ph /\ j e. S ) -> ( G gsum ( k e. { x e. D | x oR <_ ( F oF - j ) } |-> X ) ) = ( G gsum ( ( k e. { x e. D | x oR <_ ( F oF - j ) } |-> X ) o. ( m e. { x e. D | x oR <_ ( F oF - j ) } |-> ( ( F oF - j ) oF - m ) ) ) ) ) |
189 |
66
|
oveq2d |
|- ( ( ph /\ j e. S ) -> ( G gsum ( ( k e. { x e. D | x oR <_ ( F oF - j ) } |-> X ) o. ( m e. { x e. D | x oR <_ ( F oF - j ) } |-> ( ( F oF - j ) oF - m ) ) ) ) = ( G gsum ( m e. { x e. D | x oR <_ ( F oF - j ) } |-> [_ ( ( F oF - m ) oF - j ) / k ]_ X ) ) ) |
190 |
188 189
|
eqtrd |
|- ( ( ph /\ j e. S ) -> ( G gsum ( k e. { x e. D | x oR <_ ( F oF - j ) } |-> X ) ) = ( G gsum ( m e. { x e. D | x oR <_ ( F oF - j ) } |-> [_ ( ( F oF - m ) oF - j ) / k ]_ X ) ) ) |
191 |
190
|
mpteq2dva |
|- ( ph -> ( j e. S |-> ( G gsum ( k e. { x e. D | x oR <_ ( F oF - j ) } |-> X ) ) ) = ( j e. S |-> ( G gsum ( m e. { x e. D | x oR <_ ( F oF - j ) } |-> [_ ( ( F oF - m ) oF - j ) / k ]_ X ) ) ) ) |
192 |
191
|
oveq2d |
|- ( ph -> ( G gsum ( j e. S |-> ( G gsum ( k e. { x e. D | x oR <_ ( F oF - j ) } |-> X ) ) ) ) = ( G gsum ( j e. S |-> ( G gsum ( m e. { x e. D | x oR <_ ( F oF - j ) } |-> [_ ( ( F oF - m ) oF - j ) / k ]_ X ) ) ) ) ) |
193 |
101 172 192
|
3eqtr4d |
|- ( ph -> ( G gsum ( n e. S |-> ( G gsum ( j e. { x e. D | x oR <_ n } |-> Y ) ) ) ) = ( G gsum ( j e. S |-> ( G gsum ( k e. { x e. D | x oR <_ ( F oF - j ) } |-> X ) ) ) ) ) |