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