Theorem psrass1lemOLD

Description: Obsolete version of psrass1lem as of 7-Aug-2024. (Contributed by Mario Carneiro, 5-Jan-2015) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	psrbag.d	|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
	psrbagconf1o.s	|- S = { y e. D | y oR <_ F }
	gsumbagdiagOLD.i	|- ( ph -> I e. V )
	gsumbagdiagOLD.f	|- ( ph -> F e. D )
	gsumbagdiagOLD.b	|- B = ( Base ` G )
	gsumbagdiagOLD.g	|- ( ph -> G e. CMnd )
	gsumbagdiagOLD.x	|- ( ( ph /\ ( j e. S /\ k e. { x e. D | x oR <_ ( F oF - j ) } ) ) -> X e. B )
	psrass1lemOLD.y	|- ( k = ( n oF - j ) -> X = Y )
Assertion	psrass1lemOLD	|- ( 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.s	|- S = { y e. D | y oR <_ F }
3		gsumbagdiagOLD.i	|- ( ph -> I e. V )
4		gsumbagdiagOLD.f	|- ( ph -> F e. D )
5		gsumbagdiagOLD.b	|- B = ( Base ` G )
6		gsumbagdiagOLD.g	|- ( ph -> G e. CMnd )
7		gsumbagdiagOLD.x	|- ( ( ph /\ ( j e. S /\ k e. { x e. D | x oR <_ ( F oF - j ) } ) ) -> X e. B )
8		psrass1lemOLD.y	|- ( k = ( n oF - j ) -> X = Y )
9	1 2 3 4	gsumbagdiaglemOLD	|- ( ( 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	psrbagconclOLD	|- ( ( 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	sselid	|- ( ( 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	psrbagconf1oOLD	|- ( ( 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	psrbagfOLD	|- ( ( 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	sselid	|- ( ( ( ph /\ j e. S ) /\ m e. { x e. D | x oR <_ ( F oF - j ) } ) -> j e. D )
33	1	psrbagfOLD	|- ( ( 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	sselid	|- ( ( ( ph /\ j e. S ) /\ m e. { x e. D | x oR <_ ( F oF - j ) } ) -> m e. D )
39	1	psrbagfOLD	|- ( ( 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	psrbagconclOLD	|- ( ( 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	gsumbagdiagOLD	|- ( 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	psrbaglefiOLD	|- ( ( 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	psrbagconclOLD	|- ( ( 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	sselid	|- ( ( ph /\ m e. S ) -> ( F oF - m ) e. D )
87	1	psrbaglefiOLD	|- ( ( 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	psrbaglefiOLD	|- ( ( 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	gsumbagdiaglemOLD	|- ( ( 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	psrbagconf1oOLD	|- ( ( 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	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 ) ) )
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	eqtr3id	|- ( 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 ) ) ) ) )