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	ffvelcdmda	\|- ( ( ( ( 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	ffvelcdmda	\|- ( ( ( ( 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	ffvelcdmda	\|- ( ( ( ( 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	fvmptelcdm	\|- ( ( ( 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 ) ) ) ) )

Metamath Proof Explorer

Theorem psrass1lem

Proof