Metamath Proof Explorer

Theorem psrass1lem

Description: A group sum commutation used by psrass1 . (Contributed by Mario Carneiro, 5-Jan-2015)

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