Theorem gsumhashmul

Description: Express a group sum by grouping by nonzero values. (Contributed by Thierry Arnoux, 22-Jun-2024)

	Ref	Expression
Hypotheses	gsumhashmul.b	|- B = ( Base ` G )
	gsumhashmul.z	|- .0. = ( 0g ` G )
	gsumhashmul.x	|- .x. = ( .g ` G )
	gsumhashmul.g	|- ( ph -> G e. CMnd )
	gsumhashmul.f	|- ( ph -> F : A --> B )
	gsumhashmul.1	|- ( ph -> F finSupp .0. )
Assertion	gsumhashmul	|- ( ph -> ( G gsum F ) = ( G gsum ( x e. ( ran F \ { .0. } ) |-> ( ( # ` ( `' F " { x } ) ) .x. x ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		gsumhashmul.b	|- B = ( Base ` G )
2		gsumhashmul.z	|- .0. = ( 0g ` G )
3		gsumhashmul.x	|- .x. = ( .g ` G )
4		gsumhashmul.g	|- ( ph -> G e. CMnd )
5		gsumhashmul.f	|- ( ph -> F : A --> B )
6		gsumhashmul.1	|- ( ph -> F finSupp .0. )
7		suppssdm	|- ( F supp .0. ) C_ dom F
8	7 5	fssdm	|- ( ph -> ( F supp .0. ) C_ A )
9	5 8	feqresmpt	|- ( ph -> ( F |` ( F supp .0. ) ) = ( x e. ( F supp .0. ) |-> ( F ` x ) ) )
10	9	oveq2d	|- ( ph -> ( G gsum ( F |` ( F supp .0. ) ) ) = ( G gsum ( x e. ( F supp .0. ) |-> ( F ` x ) ) ) )
11		relfsupp	|- Rel finSupp
12	11	brrelex1i	|- ( F finSupp .0. -> F e. _V )
13	6 12	syl	|- ( ph -> F e. _V )
14	5	ffnd	|- ( ph -> F Fn A )
15	13 14	fndmexd	|- ( ph -> A e. _V )
16		ssidd	|- ( ph -> ( F supp .0. ) C_ ( F supp .0. ) )
17	1 2 4 15 5 16 6	gsumres	|- ( ph -> ( G gsum ( F |` ( F supp .0. ) ) ) = ( G gsum F ) )
18		nfcv	|- F/_ x ( F ` ( 1st ` z ) )
19		fveq2	|- ( x = ( 1st ` z ) -> ( F ` x ) = ( F ` ( 1st ` z ) ) )
20	6	fsuppimpd	|- ( ph -> ( F supp .0. ) e. Fin )
21		ssidd	|- ( ph -> B C_ B )
22	5	adantr	|- ( ( ph /\ x e. ( F supp .0. ) ) -> F : A --> B )
23	8	sselda	|- ( ( ph /\ x e. ( F supp .0. ) ) -> x e. A )
24	22 23	ffvelrnd	|- ( ( ph /\ x e. ( F supp .0. ) ) -> ( F ` x ) e. B )
25	5	ffund	|- ( ph -> Fun F )
26		funrel	|- ( Fun F -> Rel F )
27		reldif	|- ( Rel F -> Rel ( F \ ( _V X. { .0. } ) ) )
28	25 26 27	3syl	|- ( ph -> Rel ( F \ ( _V X. { .0. } ) ) )
29		1stdm	|- ( ( Rel ( F \ ( _V X. { .0. } ) ) /\ z e. ( F \ ( _V X. { .0. } ) ) ) -> ( 1st ` z ) e. dom ( F \ ( _V X. { .0. } ) ) )
30	28 29	sylan	|- ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) -> ( 1st ` z ) e. dom ( F \ ( _V X. { .0. } ) ) )
31	2	fvexi	|- .0. e. _V
32	31	a1i	|- ( ph -> .0. e. _V )
33		fressupp	|- ( ( Fun F /\ F e. _V /\ .0. e. _V ) -> ( F |` ( F supp .0. ) ) = ( F \ ( _V X. { .0. } ) ) )
34	25 13 32 33	syl3anc	|- ( ph -> ( F |` ( F supp .0. ) ) = ( F \ ( _V X. { .0. } ) ) )
35	34	dmeqd	|- ( ph -> dom ( F |` ( F supp .0. ) ) = dom ( F \ ( _V X. { .0. } ) ) )
36	7	a1i	|- ( ph -> ( F supp .0. ) C_ dom F )
37		ssdmres	|- ( ( F supp .0. ) C_ dom F <-> dom ( F |` ( F supp .0. ) ) = ( F supp .0. ) )
38	36 37	sylib	|- ( ph -> dom ( F |` ( F supp .0. ) ) = ( F supp .0. ) )
39	35 38	eqtr3d	|- ( ph -> dom ( F \ ( _V X. { .0. } ) ) = ( F supp .0. ) )
40	39	adantr	|- ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) -> dom ( F \ ( _V X. { .0. } ) ) = ( F supp .0. ) )
41	30 40	eleqtrd	|- ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) -> ( 1st ` z ) e. ( F supp .0. ) )
42	25	funresd	|- ( ph -> Fun ( F |` ( F supp .0. ) ) )
43	42	adantr	|- ( ( ph /\ x e. ( F supp .0. ) ) -> Fun ( F |` ( F supp .0. ) ) )
44	38	eleq2d	|- ( ph -> ( x e. dom ( F |` ( F supp .0. ) ) <-> x e. ( F supp .0. ) ) )
45	44	biimpar	|- ( ( ph /\ x e. ( F supp .0. ) ) -> x e. dom ( F |` ( F supp .0. ) ) )
46		simpr	|- ( ( ph /\ x e. ( F supp .0. ) ) -> x e. ( F supp .0. ) )
47	46	fvresd	|- ( ( ph /\ x e. ( F supp .0. ) ) -> ( ( F |` ( F supp .0. ) ) ` x ) = ( F ` x ) )
48		funopfvb	|- ( ( Fun ( F |` ( F supp .0. ) ) /\ x e. dom ( F |` ( F supp .0. ) ) ) -> ( ( ( F |` ( F supp .0. ) ) ` x ) = ( F ` x ) <-> <. x , ( F ` x ) >. e. ( F |` ( F supp .0. ) ) ) )
49	48	biimpa	|- ( ( ( Fun ( F |` ( F supp .0. ) ) /\ x e. dom ( F |` ( F supp .0. ) ) ) /\ ( ( F |` ( F supp .0. ) ) ` x ) = ( F ` x ) ) -> <. x , ( F ` x ) >. e. ( F |` ( F supp .0. ) ) )
50	43 45 47 49	syl21anc	|- ( ( ph /\ x e. ( F supp .0. ) ) -> <. x , ( F ` x ) >. e. ( F |` ( F supp .0. ) ) )
51	34	adantr	|- ( ( ph /\ x e. ( F supp .0. ) ) -> ( F |` ( F supp .0. ) ) = ( F \ ( _V X. { .0. } ) ) )
52	50 51	eleqtrd	|- ( ( ph /\ x e. ( F supp .0. ) ) -> <. x , ( F ` x ) >. e. ( F \ ( _V X. { .0. } ) ) )
53		eqeq2	|- ( v = <. x , ( F ` x ) >. -> ( z = v <-> z = <. x , ( F ` x ) >. ) )
54	53	bibi2d	|- ( v = <. x , ( F ` x ) >. -> ( ( x = ( 1st ` z ) <-> z = v ) <-> ( x = ( 1st ` z ) <-> z = <. x , ( F ` x ) >. ) ) )
55	54	ralbidv	|- ( v = <. x , ( F ` x ) >. -> ( A. z e. ( F \ ( _V X. { .0. } ) ) ( x = ( 1st ` z ) <-> z = v ) <-> A. z e. ( F \ ( _V X. { .0. } ) ) ( x = ( 1st ` z ) <-> z = <. x , ( F ` x ) >. ) ) )
56	55	adantl	|- ( ( ( ph /\ x e. ( F supp .0. ) ) /\ v = <. x , ( F ` x ) >. ) -> ( A. z e. ( F \ ( _V X. { .0. } ) ) ( x = ( 1st ` z ) <-> z = v ) <-> A. z e. ( F \ ( _V X. { .0. } ) ) ( x = ( 1st ` z ) <-> z = <. x , ( F ` x ) >. ) ) )
57		fvexd	|- ( ( ( ( ph /\ x e. ( F supp .0. ) ) /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ x = ( 1st ` z ) ) -> ( 2nd ` z ) e. _V )
58	28	ad3antrrr	|- ( ( ( ( ph /\ x e. ( F supp .0. ) ) /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ x = ( 1st ` z ) ) -> Rel ( F \ ( _V X. { .0. } ) ) )
59		simplr	|- ( ( ( ( ph /\ x e. ( F supp .0. ) ) /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ x = ( 1st ` z ) ) -> z e. ( F \ ( _V X. { .0. } ) ) )
60		1st2nd	|- ( ( Rel ( F \ ( _V X. { .0. } ) ) /\ z e. ( F \ ( _V X. { .0. } ) ) ) -> z = <. ( 1st ` z ) , ( 2nd ` z ) >. )
61	58 59 60	syl2anc	|- ( ( ( ( ph /\ x e. ( F supp .0. ) ) /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ x = ( 1st ` z ) ) -> z = <. ( 1st ` z ) , ( 2nd ` z ) >. )
62		opeq1	|- ( x = ( 1st ` z ) -> <. x , ( 2nd ` z ) >. = <. ( 1st ` z ) , ( 2nd ` z ) >. )
63	62	adantl	|- ( ( ( ( ph /\ x e. ( F supp .0. ) ) /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ x = ( 1st ` z ) ) -> <. x , ( 2nd ` z ) >. = <. ( 1st ` z ) , ( 2nd ` z ) >. )
64	61 63	eqtr4d	|- ( ( ( ( ph /\ x e. ( F supp .0. ) ) /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ x = ( 1st ` z ) ) -> z = <. x , ( 2nd ` z ) >. )
65		difssd	|- ( ( ph /\ x e. ( F supp .0. ) ) -> ( F \ ( _V X. { .0. } ) ) C_ F )
66	65	sselda	|- ( ( ( ph /\ x e. ( F supp .0. ) ) /\ z e. ( F \ ( _V X. { .0. } ) ) ) -> z e. F )
67	66	adantr	|- ( ( ( ( ph /\ x e. ( F supp .0. ) ) /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ x = ( 1st ` z ) ) -> z e. F )
68	64 67	eqeltrrd	|- ( ( ( ( ph /\ x e. ( F supp .0. ) ) /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ x = ( 1st ` z ) ) -> <. x , ( 2nd ` z ) >. e. F )
69	64 68	jca	|- ( ( ( ( ph /\ x e. ( F supp .0. ) ) /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ x = ( 1st ` z ) ) -> ( z = <. x , ( 2nd ` z ) >. /\ <. x , ( 2nd ` z ) >. e. F ) )
70		opeq2	|- ( y = ( 2nd ` z ) -> <. x , y >. = <. x , ( 2nd ` z ) >. )
71	70	eqeq2d	|- ( y = ( 2nd ` z ) -> ( z = <. x , y >. <-> z = <. x , ( 2nd ` z ) >. ) )
72	70	eleq1d	|- ( y = ( 2nd ` z ) -> ( <. x , y >. e. F <-> <. x , ( 2nd ` z ) >. e. F ) )
73	71 72	anbi12d	|- ( y = ( 2nd ` z ) -> ( ( z = <. x , y >. /\ <. x , y >. e. F ) <-> ( z = <. x , ( 2nd ` z ) >. /\ <. x , ( 2nd ` z ) >. e. F ) ) )
74	57 69 73	spcedv	|- ( ( ( ( ph /\ x e. ( F supp .0. ) ) /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ x = ( 1st ` z ) ) -> E. y ( z = <. x , y >. /\ <. x , y >. e. F ) )
75		vex	|- x e. _V
76	75	elsnres	|- ( z e. ( F |` { x } ) <-> E. y ( z = <. x , y >. /\ <. x , y >. e. F ) )
77	74 76	sylibr	|- ( ( ( ( ph /\ x e. ( F supp .0. ) ) /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ x = ( 1st ` z ) ) -> z e. ( F |` { x } ) )
78	14	ad3antrrr	|- ( ( ( ( ph /\ x e. ( F supp .0. ) ) /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ x = ( 1st ` z ) ) -> F Fn A )
79	23	ad2antrr	|- ( ( ( ( ph /\ x e. ( F supp .0. ) ) /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ x = ( 1st ` z ) ) -> x e. A )
80		fnressn	|- ( ( F Fn A /\ x e. A ) -> ( F |` { x } ) = { <. x , ( F ` x ) >. } )
81	78 79 80	syl2anc	|- ( ( ( ( ph /\ x e. ( F supp .0. ) ) /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ x = ( 1st ` z ) ) -> ( F |` { x } ) = { <. x , ( F ` x ) >. } )
82	77 81	eleqtrd	|- ( ( ( ( ph /\ x e. ( F supp .0. ) ) /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ x = ( 1st ` z ) ) -> z e. { <. x , ( F ` x ) >. } )
83		elsni	|- ( z e. { <. x , ( F ` x ) >. } -> z = <. x , ( F ` x ) >. )
84	82 83	syl	|- ( ( ( ( ph /\ x e. ( F supp .0. ) ) /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ x = ( 1st ` z ) ) -> z = <. x , ( F ` x ) >. )
85		simpr	|- ( ( ( ( ph /\ x e. ( F supp .0. ) ) /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ z = <. x , ( F ` x ) >. ) -> z = <. x , ( F ` x ) >. )
86	85	fveq2d	|- ( ( ( ( ph /\ x e. ( F supp .0. ) ) /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ z = <. x , ( F ` x ) >. ) -> ( 1st ` z ) = ( 1st ` <. x , ( F ` x ) >. ) )
87		fvex	|- ( F ` x ) e. _V
88	75 87	op1st	|- ( 1st ` <. x , ( F ` x ) >. ) = x
89	86 88	eqtr2di	|- ( ( ( ( ph /\ x e. ( F supp .0. ) ) /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ z = <. x , ( F ` x ) >. ) -> x = ( 1st ` z ) )
90	84 89	impbida	|- ( ( ( ph /\ x e. ( F supp .0. ) ) /\ z e. ( F \ ( _V X. { .0. } ) ) ) -> ( x = ( 1st ` z ) <-> z = <. x , ( F ` x ) >. ) )
91	90	ralrimiva	|- ( ( ph /\ x e. ( F supp .0. ) ) -> A. z e. ( F \ ( _V X. { .0. } ) ) ( x = ( 1st ` z ) <-> z = <. x , ( F ` x ) >. ) )
92	52 56 91	rspcedvd	|- ( ( ph /\ x e. ( F supp .0. ) ) -> E. v e. ( F \ ( _V X. { .0. } ) ) A. z e. ( F \ ( _V X. { .0. } ) ) ( x = ( 1st ` z ) <-> z = v ) )
93		reu6	|- ( E! z e. ( F \ ( _V X. { .0. } ) ) x = ( 1st ` z ) <-> E. v e. ( F \ ( _V X. { .0. } ) ) A. z e. ( F \ ( _V X. { .0. } ) ) ( x = ( 1st ` z ) <-> z = v ) )
94	92 93	sylibr	|- ( ( ph /\ x e. ( F supp .0. ) ) -> E! z e. ( F \ ( _V X. { .0. } ) ) x = ( 1st ` z ) )
95	18 1 2 19 4 20 21 24 41 94	gsummptf1o	|- ( ph -> ( G gsum ( x e. ( F supp .0. ) |-> ( F ` x ) ) ) = ( G gsum ( z e. ( F \ ( _V X. { .0. } ) ) |-> ( F ` ( 1st ` z ) ) ) ) )
96	10 17 95	3eqtr3d	|- ( ph -> ( G gsum F ) = ( G gsum ( z e. ( F \ ( _V X. { .0. } ) ) |-> ( F ` ( 1st ` z ) ) ) ) )
97		simpr	|- ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) -> z e. ( F \ ( _V X. { .0. } ) ) )
98	97	eldifad	|- ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) -> z e. F )
99		funfv1st2nd	|- ( ( Fun F /\ z e. F ) -> ( F ` ( 1st ` z ) ) = ( 2nd ` z ) )
100	25 98 99	syl2an2r	|- ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) -> ( F ` ( 1st ` z ) ) = ( 2nd ` z ) )
101	100	mpteq2dva	|- ( ph -> ( z e. ( F \ ( _V X. { .0. } ) ) |-> ( F ` ( 1st ` z ) ) ) = ( z e. ( F \ ( _V X. { .0. } ) ) |-> ( 2nd ` z ) ) )
102	101	oveq2d	|- ( ph -> ( G gsum ( z e. ( F \ ( _V X. { .0. } ) ) |-> ( F ` ( 1st ` z ) ) ) ) = ( G gsum ( z e. ( F \ ( _V X. { .0. } ) ) |-> ( 2nd ` z ) ) ) )
103	96 102	eqtrd	|- ( ph -> ( G gsum F ) = ( G gsum ( z e. ( F \ ( _V X. { .0. } ) ) |-> ( 2nd ` z ) ) ) )
104		nfcv	|- F/_ z ( 1st ` t )
105		fvex	|- ( 2nd ` t ) e. _V
106		fvex	|- ( 1st ` t ) e. _V
107	105 106	op2ndd	|- ( z = <. ( 2nd ` t ) , ( 1st ` t ) >. -> ( 2nd ` z ) = ( 1st ` t ) )
108		resfnfinfin	|- ( ( F Fn A /\ ( F supp .0. ) e. Fin ) -> ( F |` ( F supp .0. ) ) e. Fin )
109	14 20 108	syl2anc	|- ( ph -> ( F |` ( F supp .0. ) ) e. Fin )
110	34 109	eqeltrrd	|- ( ph -> ( F \ ( _V X. { .0. } ) ) e. Fin )
111	34	rneqd	|- ( ph -> ran ( F |` ( F supp .0. ) ) = ran ( F \ ( _V X. { .0. } ) ) )
112		rnresss	|- ran ( F |` ( F supp .0. ) ) C_ ran F
113	5	frnd	|- ( ph -> ran F C_ B )
114	112 113	sstrid	|- ( ph -> ran ( F |` ( F supp .0. ) ) C_ B )
115	111 114	eqsstrrd	|- ( ph -> ran ( F \ ( _V X. { .0. } ) ) C_ B )
116		2ndrn	|- ( ( Rel ( F \ ( _V X. { .0. } ) ) /\ z e. ( F \ ( _V X. { .0. } ) ) ) -> ( 2nd ` z ) e. ran ( F \ ( _V X. { .0. } ) ) )
117	28 116	sylan	|- ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) -> ( 2nd ` z ) e. ran ( F \ ( _V X. { .0. } ) ) )
118		relcnv	|- Rel `' F
119		reldif	|- ( Rel `' F -> Rel ( `' F \ ( { .0. } X. _V ) ) )
120	118 119	mp1i	|- ( ph -> Rel ( `' F \ ( { .0. } X. _V ) ) )
121		1st2nd	|- ( ( Rel ( `' F \ ( { .0. } X. _V ) ) /\ t e. ( `' F \ ( { .0. } X. _V ) ) ) -> t = <. ( 1st ` t ) , ( 2nd ` t ) >. )
122	120 121	sylan	|- ( ( ph /\ t e. ( `' F \ ( { .0. } X. _V ) ) ) -> t = <. ( 1st ` t ) , ( 2nd ` t ) >. )
123		cnvdif	|- `' ( F \ ( _V X. { .0. } ) ) = ( `' F \ `' ( _V X. { .0. } ) )
124		cnvxp	|- `' ( _V X. { .0. } ) = ( { .0. } X. _V )
125	124	difeq2i	|- ( `' F \ `' ( _V X. { .0. } ) ) = ( `' F \ ( { .0. } X. _V ) )
126	123 125	eqtri	|- `' ( F \ ( _V X. { .0. } ) ) = ( `' F \ ( { .0. } X. _V ) )
127	126	eqimss2i	|- ( `' F \ ( { .0. } X. _V ) ) C_ `' ( F \ ( _V X. { .0. } ) )
128	127	a1i	|- ( ph -> ( `' F \ ( { .0. } X. _V ) ) C_ `' ( F \ ( _V X. { .0. } ) ) )
129	128	sselda	|- ( ( ph /\ t e. ( `' F \ ( { .0. } X. _V ) ) ) -> t e. `' ( F \ ( _V X. { .0. } ) ) )
130	122 129	eqeltrrd	|- ( ( ph /\ t e. ( `' F \ ( { .0. } X. _V ) ) ) -> <. ( 1st ` t ) , ( 2nd ` t ) >. e. `' ( F \ ( _V X. { .0. } ) ) )
131	106 105	opelcnv	|- ( <. ( 1st ` t ) , ( 2nd ` t ) >. e. `' ( F \ ( _V X. { .0. } ) ) <-> <. ( 2nd ` t ) , ( 1st ` t ) >. e. ( F \ ( _V X. { .0. } ) ) )
132	130 131	sylib	|- ( ( ph /\ t e. ( `' F \ ( { .0. } X. _V ) ) ) -> <. ( 2nd ` t ) , ( 1st ` t ) >. e. ( F \ ( _V X. { .0. } ) ) )
133	28	adantr	|- ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) -> Rel ( F \ ( _V X. { .0. } ) ) )
134		eqidd	|- ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) -> U. `' { z } = U. `' { z } )
135		cnvf1olem	|- ( ( Rel ( F \ ( _V X. { .0. } ) ) /\ ( z e. ( F \ ( _V X. { .0. } ) ) /\ U. `' { z } = U. `' { z } ) ) -> ( U. `' { z } e. `' ( F \ ( _V X. { .0. } ) ) /\ z = U. `' { U. `' { z } } ) )
136	135	simpld	|- ( ( Rel ( F \ ( _V X. { .0. } ) ) /\ ( z e. ( F \ ( _V X. { .0. } ) ) /\ U. `' { z } = U. `' { z } ) ) -> U. `' { z } e. `' ( F \ ( _V X. { .0. } ) ) )
137	133 97 134 136	syl12anc	|- ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) -> U. `' { z } e. `' ( F \ ( _V X. { .0. } ) ) )
138	137 126	eleqtrdi	|- ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) -> U. `' { z } e. ( `' F \ ( { .0. } X. _V ) ) )
139		eqeq2	|- ( u = U. `' { z } -> ( t = u <-> t = U. `' { z } ) )
140	139	bibi2d	|- ( u = U. `' { z } -> ( ( z = <. ( 2nd ` t ) , ( 1st ` t ) >. <-> t = u ) <-> ( z = <. ( 2nd ` t ) , ( 1st ` t ) >. <-> t = U. `' { z } ) ) )
141	140	ralbidv	|- ( u = U. `' { z } -> ( A. t e. ( `' F \ ( { .0. } X. _V ) ) ( z = <. ( 2nd ` t ) , ( 1st ` t ) >. <-> t = u ) <-> A. t e. ( `' F \ ( { .0. } X. _V ) ) ( z = <. ( 2nd ` t ) , ( 1st ` t ) >. <-> t = U. `' { z } ) ) )
142	141	adantl	|- ( ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ u = U. `' { z } ) -> ( A. t e. ( `' F \ ( { .0. } X. _V ) ) ( z = <. ( 2nd ` t ) , ( 1st ` t ) >. <-> t = u ) <-> A. t e. ( `' F \ ( { .0. } X. _V ) ) ( z = <. ( 2nd ` t ) , ( 1st ` t ) >. <-> t = U. `' { z } ) ) )
143	118 119	mp1i	|- ( ( ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ t e. ( `' F \ ( { .0. } X. _V ) ) ) /\ z = <. ( 2nd ` t ) , ( 1st ` t ) >. ) -> Rel ( `' F \ ( { .0. } X. _V ) ) )
144		simplr	|- ( ( ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ t e. ( `' F \ ( { .0. } X. _V ) ) ) /\ z = <. ( 2nd ` t ) , ( 1st ` t ) >. ) -> t e. ( `' F \ ( { .0. } X. _V ) ) )
145		simpr	|- ( ( ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ t e. ( `' F \ ( { .0. } X. _V ) ) ) /\ z = <. ( 2nd ` t ) , ( 1st ` t ) >. ) -> z = <. ( 2nd ` t ) , ( 1st ` t ) >. )
146		df-rel	|- ( Rel ( `' F \ ( { .0. } X. _V ) ) <-> ( `' F \ ( { .0. } X. _V ) ) C_ ( _V X. _V ) )
147	120 146	sylib	|- ( ph -> ( `' F \ ( { .0. } X. _V ) ) C_ ( _V X. _V ) )
148	147	ad3antrrr	|- ( ( ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ t e. ( `' F \ ( { .0. } X. _V ) ) ) /\ z = <. ( 2nd ` t ) , ( 1st ` t ) >. ) -> ( `' F \ ( { .0. } X. _V ) ) C_ ( _V X. _V ) )
149	148 144	sseldd	|- ( ( ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ t e. ( `' F \ ( { .0. } X. _V ) ) ) /\ z = <. ( 2nd ` t ) , ( 1st ` t ) >. ) -> t e. ( _V X. _V ) )
150		2nd1st	|- ( t e. ( _V X. _V ) -> U. `' { t } = <. ( 2nd ` t ) , ( 1st ` t ) >. )
151	149 150	syl	|- ( ( ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ t e. ( `' F \ ( { .0. } X. _V ) ) ) /\ z = <. ( 2nd ` t ) , ( 1st ` t ) >. ) -> U. `' { t } = <. ( 2nd ` t ) , ( 1st ` t ) >. )
152	145 151	eqtr4d	|- ( ( ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ t e. ( `' F \ ( { .0. } X. _V ) ) ) /\ z = <. ( 2nd ` t ) , ( 1st ` t ) >. ) -> z = U. `' { t } )
153		cnvf1olem	|- ( ( Rel ( `' F \ ( { .0. } X. _V ) ) /\ ( t e. ( `' F \ ( { .0. } X. _V ) ) /\ z = U. `' { t } ) ) -> ( z e. `' ( `' F \ ( { .0. } X. _V ) ) /\ t = U. `' { z } ) )
154	153	simprd	|- ( ( Rel ( `' F \ ( { .0. } X. _V ) ) /\ ( t e. ( `' F \ ( { .0. } X. _V ) ) /\ z = U. `' { t } ) ) -> t = U. `' { z } )
155	143 144 152 154	syl12anc	|- ( ( ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ t e. ( `' F \ ( { .0. } X. _V ) ) ) /\ z = <. ( 2nd ` t ) , ( 1st ` t ) >. ) -> t = U. `' { z } )
156	28	ad3antrrr	|- ( ( ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ t e. ( `' F \ ( { .0. } X. _V ) ) ) /\ t = U. `' { z } ) -> Rel ( F \ ( _V X. { .0. } ) ) )
157	97	ad2antrr	|- ( ( ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ t e. ( `' F \ ( { .0. } X. _V ) ) ) /\ t = U. `' { z } ) -> z e. ( F \ ( _V X. { .0. } ) ) )
158		simpr	|- ( ( ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ t e. ( `' F \ ( { .0. } X. _V ) ) ) /\ t = U. `' { z } ) -> t = U. `' { z } )
159		cnvf1olem	|- ( ( Rel ( F \ ( _V X. { .0. } ) ) /\ ( z e. ( F \ ( _V X. { .0. } ) ) /\ t = U. `' { z } ) ) -> ( t e. `' ( F \ ( _V X. { .0. } ) ) /\ z = U. `' { t } ) )
160	159	simprd	|- ( ( Rel ( F \ ( _V X. { .0. } ) ) /\ ( z e. ( F \ ( _V X. { .0. } ) ) /\ t = U. `' { z } ) ) -> z = U. `' { t } )
161	156 157 158 160	syl12anc	|- ( ( ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ t e. ( `' F \ ( { .0. } X. _V ) ) ) /\ t = U. `' { z } ) -> z = U. `' { t } )
162	147	ad3antrrr	|- ( ( ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ t e. ( `' F \ ( { .0. } X. _V ) ) ) /\ t = U. `' { z } ) -> ( `' F \ ( { .0. } X. _V ) ) C_ ( _V X. _V ) )
163		simplr	|- ( ( ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ t e. ( `' F \ ( { .0. } X. _V ) ) ) /\ t = U. `' { z } ) -> t e. ( `' F \ ( { .0. } X. _V ) ) )
164	162 163	sseldd	|- ( ( ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ t e. ( `' F \ ( { .0. } X. _V ) ) ) /\ t = U. `' { z } ) -> t e. ( _V X. _V ) )
165	164 150	syl	|- ( ( ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ t e. ( `' F \ ( { .0. } X. _V ) ) ) /\ t = U. `' { z } ) -> U. `' { t } = <. ( 2nd ` t ) , ( 1st ` t ) >. )
166	161 165	eqtrd	|- ( ( ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ t e. ( `' F \ ( { .0. } X. _V ) ) ) /\ t = U. `' { z } ) -> z = <. ( 2nd ` t ) , ( 1st ` t ) >. )
167	155 166	impbida	|- ( ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ t e. ( `' F \ ( { .0. } X. _V ) ) ) -> ( z = <. ( 2nd ` t ) , ( 1st ` t ) >. <-> t = U. `' { z } ) )
168	167	ralrimiva	|- ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) -> A. t e. ( `' F \ ( { .0. } X. _V ) ) ( z = <. ( 2nd ` t ) , ( 1st ` t ) >. <-> t = U. `' { z } ) )
169	138 142 168	rspcedvd	|- ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) -> E. u e. ( `' F \ ( { .0. } X. _V ) ) A. t e. ( `' F \ ( { .0. } X. _V ) ) ( z = <. ( 2nd ` t ) , ( 1st ` t ) >. <-> t = u ) )
170		reu6	|- ( E! t e. ( `' F \ ( { .0. } X. _V ) ) z = <. ( 2nd ` t ) , ( 1st ` t ) >. <-> E. u e. ( `' F \ ( { .0. } X. _V ) ) A. t e. ( `' F \ ( { .0. } X. _V ) ) ( z = <. ( 2nd ` t ) , ( 1st ` t ) >. <-> t = u ) )
171	169 170	sylibr	|- ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) -> E! t e. ( `' F \ ( { .0. } X. _V ) ) z = <. ( 2nd ` t ) , ( 1st ` t ) >. )
172	104 1 2 107 4 110 115 117 132 171	gsummptf1o	|- ( ph -> ( G gsum ( z e. ( F \ ( _V X. { .0. } ) ) |-> ( 2nd ` z ) ) ) = ( G gsum ( t e. ( `' F \ ( { .0. } X. _V ) ) |-> ( 1st ` t ) ) ) )
173		fveq2	|- ( t = z -> ( 1st ` t ) = ( 1st ` z ) )
174	173	cbvmptv	|- ( t e. ( `' F \ ( { .0. } X. _V ) ) |-> ( 1st ` t ) ) = ( z e. ( `' F \ ( { .0. } X. _V ) ) |-> ( 1st ` z ) )
175	34	cnveqd	|- ( ph -> `' ( F |` ( F supp .0. ) ) = `' ( F \ ( _V X. { .0. } ) ) )
176	175 126	eqtr2di	|- ( ph -> ( `' F \ ( { .0. } X. _V ) ) = `' ( F |` ( F supp .0. ) ) )
177	176	mpteq1d	|- ( ph -> ( z e. ( `' F \ ( { .0. } X. _V ) ) |-> ( 1st ` z ) ) = ( z e. `' ( F |` ( F supp .0. ) ) |-> ( 1st ` z ) ) )
178	174 177	syl5eq	|- ( ph -> ( t e. ( `' F \ ( { .0. } X. _V ) ) |-> ( 1st ` t ) ) = ( z e. `' ( F |` ( F supp .0. ) ) |-> ( 1st ` z ) ) )
179	178	oveq2d	|- ( ph -> ( G gsum ( t e. ( `' F \ ( { .0. } X. _V ) ) |-> ( 1st ` t ) ) ) = ( G gsum ( z e. `' ( F |` ( F supp .0. ) ) |-> ( 1st ` z ) ) ) )
180	103 172 179	3eqtrd	|- ( ph -> ( G gsum F ) = ( G gsum ( z e. `' ( F |` ( F supp .0. ) ) |-> ( 1st ` z ) ) ) )
181		nfcv	|- F/_ y ( 1st ` z )
182		nfv	|- F/ x ph
183		vex	|- y e. _V
184	75 183	op1std	|- ( z = <. x , y >. -> ( 1st ` z ) = x )
185		relcnv	|- Rel `' ( F |` ( F supp .0. ) )
186	185	a1i	|- ( ph -> Rel `' ( F |` ( F supp .0. ) ) )
187		cnvfi	|- ( ( F |` ( F supp .0. ) ) e. Fin -> `' ( F |` ( F supp .0. ) ) e. Fin )
188	109 187	syl	|- ( ph -> `' ( F |` ( F supp .0. ) ) e. Fin )
189	113	adantr	|- ( ( ph /\ z e. `' ( F |` ( F supp .0. ) ) ) -> ran F C_ B )
190	185	a1i	|- ( ( ph /\ z e. `' ( F |` ( F supp .0. ) ) ) -> Rel `' ( F |` ( F supp .0. ) ) )
191		simpr	|- ( ( ph /\ z e. `' ( F |` ( F supp .0. ) ) ) -> z e. `' ( F |` ( F supp .0. ) ) )
192		1stdm	|- ( ( Rel `' ( F |` ( F supp .0. ) ) /\ z e. `' ( F |` ( F supp .0. ) ) ) -> ( 1st ` z ) e. dom `' ( F |` ( F supp .0. ) ) )
193	190 191 192	syl2anc	|- ( ( ph /\ z e. `' ( F |` ( F supp .0. ) ) ) -> ( 1st ` z ) e. dom `' ( F |` ( F supp .0. ) ) )
194		df-rn	|- ran ( F |` ( F supp .0. ) ) = dom `' ( F |` ( F supp .0. ) )
195	193 194	eleqtrrdi	|- ( ( ph /\ z e. `' ( F |` ( F supp .0. ) ) ) -> ( 1st ` z ) e. ran ( F |` ( F supp .0. ) ) )
196	112 195	sselid	|- ( ( ph /\ z e. `' ( F |` ( F supp .0. ) ) ) -> ( 1st ` z ) e. ran F )
197	189 196	sseldd	|- ( ( ph /\ z e. `' ( F |` ( F supp .0. ) ) ) -> ( 1st ` z ) e. B )
198	181 182 1 184 186 188 4 197	gsummpt2d	|- ( ph -> ( G gsum ( z e. `' ( F |` ( F supp .0. ) ) |-> ( 1st ` z ) ) ) = ( G gsum ( x e. dom `' ( F |` ( F supp .0. ) ) |-> ( G gsum ( y e. ( `' ( F |` ( F supp .0. ) ) " { x } ) |-> x ) ) ) ) )
199		df-ima	|- ( F " ( F supp .0. ) ) = ran ( F |` ( F supp .0. ) )
200		supppreima	|- ( ( Fun F /\ F e. _V /\ .0. e. _V ) -> ( F supp .0. ) = ( `' F " ( ran F \ { .0. } ) ) )
201	25 13 32 200	syl3anc	|- ( ph -> ( F supp .0. ) = ( `' F " ( ran F \ { .0. } ) ) )
202	201	imaeq2d	|- ( ph -> ( F " ( F supp .0. ) ) = ( F " ( `' F " ( ran F \ { .0. } ) ) ) )
203	199 202	eqtr3id	|- ( ph -> ran ( F |` ( F supp .0. ) ) = ( F " ( `' F " ( ran F \ { .0. } ) ) ) )
204		funimacnv	|- ( Fun F -> ( F " ( `' F " ( ran F \ { .0. } ) ) ) = ( ( ran F \ { .0. } ) i^i ran F ) )
205	25 204	syl	|- ( ph -> ( F " ( `' F " ( ran F \ { .0. } ) ) ) = ( ( ran F \ { .0. } ) i^i ran F ) )
206		difssd	|- ( ph -> ( ran F \ { .0. } ) C_ ran F )
207		df-ss	|- ( ( ran F \ { .0. } ) C_ ran F <-> ( ( ran F \ { .0. } ) i^i ran F ) = ( ran F \ { .0. } ) )
208	206 207	sylib	|- ( ph -> ( ( ran F \ { .0. } ) i^i ran F ) = ( ran F \ { .0. } ) )
209	203 205 208	3eqtrd	|- ( ph -> ran ( F |` ( F supp .0. ) ) = ( ran F \ { .0. } ) )
210	194 209	eqtr3id	|- ( ph -> dom `' ( F |` ( F supp .0. ) ) = ( ran F \ { .0. } ) )
211	4	cmnmndd	|- ( ph -> G e. Mnd )
212	211	adantr	|- ( ( ph /\ x e. dom `' ( F |` ( F supp .0. ) ) ) -> G e. Mnd )
213	109	adantr	|- ( ( ph /\ x e. dom `' ( F |` ( F supp .0. ) ) ) -> ( F |` ( F supp .0. ) ) e. Fin )
214		imafi2	|- ( `' ( F |` ( F supp .0. ) ) e. Fin -> ( `' ( F |` ( F supp .0. ) ) " { x } ) e. Fin )
215	213 187 214	3syl	|- ( ( ph /\ x e. dom `' ( F |` ( F supp .0. ) ) ) -> ( `' ( F |` ( F supp .0. ) ) " { x } ) e. Fin )
216	194 114	eqsstrrid	|- ( ph -> dom `' ( F |` ( F supp .0. ) ) C_ B )
217	216	sselda	|- ( ( ph /\ x e. dom `' ( F |` ( F supp .0. ) ) ) -> x e. B )
218	1 3	gsumconst	|- ( ( G e. Mnd /\ ( `' ( F |` ( F supp .0. ) ) " { x } ) e. Fin /\ x e. B ) -> ( G gsum ( y e. ( `' ( F |` ( F supp .0. ) ) " { x } ) |-> x ) ) = ( ( # ` ( `' ( F |` ( F supp .0. ) ) " { x } ) ) .x. x ) )
219	212 215 217 218	syl3anc	|- ( ( ph /\ x e. dom `' ( F |` ( F supp .0. ) ) ) -> ( G gsum ( y e. ( `' ( F |` ( F supp .0. ) ) " { x } ) |-> x ) ) = ( ( # ` ( `' ( F |` ( F supp .0. ) ) " { x } ) ) .x. x ) )
220		cnvresima	|- ( `' ( F |` ( F supp .0. ) ) " { x } ) = ( ( `' F " { x } ) i^i ( F supp .0. ) )
221	210	eleq2d	|- ( ph -> ( x e. dom `' ( F |` ( F supp .0. ) ) <-> x e. ( ran F \ { .0. } ) ) )
222	221	biimpa	|- ( ( ph /\ x e. dom `' ( F |` ( F supp .0. ) ) ) -> x e. ( ran F \ { .0. } ) )
223	222	snssd	|- ( ( ph /\ x e. dom `' ( F |` ( F supp .0. ) ) ) -> { x } C_ ( ran F \ { .0. } ) )
224		sspreima	|- ( ( Fun F /\ { x } C_ ( ran F \ { .0. } ) ) -> ( `' F " { x } ) C_ ( `' F " ( ran F \ { .0. } ) ) )
225	25 223 224	syl2an2r	|- ( ( ph /\ x e. dom `' ( F |` ( F supp .0. ) ) ) -> ( `' F " { x } ) C_ ( `' F " ( ran F \ { .0. } ) ) )
226	201	adantr	|- ( ( ph /\ x e. dom `' ( F |` ( F supp .0. ) ) ) -> ( F supp .0. ) = ( `' F " ( ran F \ { .0. } ) ) )
227	225 226	sseqtrrd	|- ( ( ph /\ x e. dom `' ( F |` ( F supp .0. ) ) ) -> ( `' F " { x } ) C_ ( F supp .0. ) )
228		df-ss	|- ( ( `' F " { x } ) C_ ( F supp .0. ) <-> ( ( `' F " { x } ) i^i ( F supp .0. ) ) = ( `' F " { x } ) )
229	227 228	sylib	|- ( ( ph /\ x e. dom `' ( F |` ( F supp .0. ) ) ) -> ( ( `' F " { x } ) i^i ( F supp .0. ) ) = ( `' F " { x } ) )
230	220 229	eqtr2id	|- ( ( ph /\ x e. dom `' ( F |` ( F supp .0. ) ) ) -> ( `' F " { x } ) = ( `' ( F |` ( F supp .0. ) ) " { x } ) )
231	230	fveq2d	|- ( ( ph /\ x e. dom `' ( F |` ( F supp .0. ) ) ) -> ( # ` ( `' F " { x } ) ) = ( # ` ( `' ( F |` ( F supp .0. ) ) " { x } ) ) )
232	231	oveq1d	|- ( ( ph /\ x e. dom `' ( F |` ( F supp .0. ) ) ) -> ( ( # ` ( `' F " { x } ) ) .x. x ) = ( ( # ` ( `' ( F |` ( F supp .0. ) ) " { x } ) ) .x. x ) )
233	219 232	eqtr4d	|- ( ( ph /\ x e. dom `' ( F |` ( F supp .0. ) ) ) -> ( G gsum ( y e. ( `' ( F |` ( F supp .0. ) ) " { x } ) |-> x ) ) = ( ( # ` ( `' F " { x } ) ) .x. x ) )
234	210 233	mpteq12dva	|- ( ph -> ( x e. dom `' ( F |` ( F supp .0. ) ) |-> ( G gsum ( y e. ( `' ( F |` ( F supp .0. ) ) " { x } ) |-> x ) ) ) = ( x e. ( ran F \ { .0. } ) |-> ( ( # ` ( `' F " { x } ) ) .x. x ) ) )
235	234	oveq2d	|- ( ph -> ( G gsum ( x e. dom `' ( F |` ( F supp .0. ) ) |-> ( G gsum ( y e. ( `' ( F |` ( F supp .0. ) ) " { x } ) |-> x ) ) ) ) = ( G gsum ( x e. ( ran F \ { .0. } ) |-> ( ( # ` ( `' F " { x } ) ) .x. x ) ) ) )
236	180 198 235	3eqtrd	|- ( ph -> ( G gsum F ) = ( G gsum ( x e. ( ran F \ { .0. } ) |-> ( ( # ` ( `' F " { x } ) ) .x. x ) ) ) )