Metamath Proof Explorer

Theorem psrass1lem

Description: A group sum commutation used by psrass1 . (Contributed by Mario Carneiro, 5-Jan-2015) Remove a sethood hypothesis. (Revised by SN, 7-Aug-2024)

Ref Expression
Hypotheses gsumbagdiag.d 
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
gsumbagdiag.s 
|- S = { y e. D | y oR <_ F }
gsumbagdiag.f 
|- ( ph -> F e. D )
gsumbagdiag.b 
|- B = ( Base ` G )
gsumbagdiag.g 
|- ( ph -> G e. CMnd )
gsumbagdiag.x 
|- ( ( ph /\ ( j e. S /\ k e. { x e. D | x oR <_ ( F oF - j ) } ) ) -> X e. B )
psrass1lem.y 
|- ( k = ( n oF - j ) -> X = Y )
Assertion psrass1lem 
|- ( 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 ) ) ) ) )

Proof

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 eqtrid 
 |-  ( 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 ) ) ) ) )