gsum2dlem2

Description: Lemma for gsum2d . (Contributed by Mario Carneiro, 28-Dec-2014) (Revised by AV, 8-Jun-2019)

	Ref	Expression
Hypotheses	gsum2d.b	\|- B = ( Base ` G )
	gsum2d.z	\|- .0. = ( 0g ` G )
	gsum2d.g	\|- ( ph -> G e. CMnd )
	gsum2d.a	\|- ( ph -> A e. V )
	gsum2d.r	\|- ( ph -> Rel A )
	gsum2d.d	\|- ( ph -> D e. W )
	gsum2d.s	\|- ( ph -> dom A C_ D )
	gsum2d.f	\|- ( ph -> F : A --> B )
	gsum2d.w	\|- ( ph -> F finSupp .0. )
Assertion	gsum2dlem2	\|- ( ph -> ( G gsum ( F \|` ( A \|` dom ( F supp .0. ) ) ) ) = ( G gsum ( j e. dom ( F supp .0. ) \|-> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		gsum2d.b	\|- B = ( Base ` G )
2		gsum2d.z	\|- .0. = ( 0g ` G )
3		gsum2d.g	\|- ( ph -> G e. CMnd )
4		gsum2d.a	\|- ( ph -> A e. V )
5		gsum2d.r	\|- ( ph -> Rel A )
6		gsum2d.d	\|- ( ph -> D e. W )
7		gsum2d.s	\|- ( ph -> dom A C_ D )
8		gsum2d.f	\|- ( ph -> F : A --> B )
9		gsum2d.w	\|- ( ph -> F finSupp .0. )
10	9	fsuppimpd	\|- ( ph -> ( F supp .0. ) e. Fin )
11		dmfi	\|- ( ( F supp .0. ) e. Fin -> dom ( F supp .0. ) e. Fin )
12	10 11	syl	\|- ( ph -> dom ( F supp .0. ) e. Fin )
13		reseq2	\|- ( x = (/) -> ( A \|` x ) = ( A \|` (/) ) )
14		res0	\|- ( A \|` (/) ) = (/)
15	13 14	eqtrdi	\|- ( x = (/) -> ( A \|` x ) = (/) )
16	15	reseq2d	\|- ( x = (/) -> ( F \|` ( A \|` x ) ) = ( F \|` (/) ) )
17		res0	\|- ( F \|` (/) ) = (/)
18	16 17	eqtrdi	\|- ( x = (/) -> ( F \|` ( A \|` x ) ) = (/) )
19	18	oveq2d	\|- ( x = (/) -> ( G gsum ( F \|` ( A \|` x ) ) ) = ( G gsum (/) ) )
20		mpteq1	\|- ( x = (/) -> ( j e. x \|-> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) ) = ( j e. (/) \|-> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) ) )
21		mpt0	\|- ( j e. (/) \|-> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) ) = (/)
22	20 21	eqtrdi	\|- ( x = (/) -> ( j e. x \|-> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) ) = (/) )
23	22	oveq2d	\|- ( x = (/) -> ( G gsum ( j e. x \|-> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) ) ) = ( G gsum (/) ) )
24	19 23	eqeq12d	\|- ( x = (/) -> ( ( G gsum ( F \|` ( A \|` x ) ) ) = ( G gsum ( j e. x \|-> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) ) ) <-> ( G gsum (/) ) = ( G gsum (/) ) ) )
25	24	imbi2d	\|- ( x = (/) -> ( ( ph -> ( G gsum ( F \|` ( A \|` x ) ) ) = ( G gsum ( j e. x \|-> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) ) ) ) <-> ( ph -> ( G gsum (/) ) = ( G gsum (/) ) ) ) )
26		reseq2	\|- ( x = y -> ( A \|` x ) = ( A \|` y ) )
27	26	reseq2d	\|- ( x = y -> ( F \|` ( A \|` x ) ) = ( F \|` ( A \|` y ) ) )
28	27	oveq2d	\|- ( x = y -> ( G gsum ( F \|` ( A \|` x ) ) ) = ( G gsum ( F \|` ( A \|` y ) ) ) )
29		mpteq1	\|- ( x = y -> ( j e. x \|-> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) ) = ( j e. y \|-> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) ) )
30	29	oveq2d	\|- ( x = y -> ( G gsum ( j e. x \|-> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) ) ) = ( G gsum ( j e. y \|-> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) ) ) )
31	28 30	eqeq12d	\|- ( x = y -> ( ( G gsum ( F \|` ( A \|` x ) ) ) = ( G gsum ( j e. x \|-> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) ) ) <-> ( G gsum ( F \|` ( A \|` y ) ) ) = ( G gsum ( j e. y \|-> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) ) ) ) )
32	31	imbi2d	\|- ( x = y -> ( ( ph -> ( G gsum ( F \|` ( A \|` x ) ) ) = ( G gsum ( j e. x \|-> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) ) ) ) <-> ( ph -> ( G gsum ( F \|` ( A \|` y ) ) ) = ( G gsum ( j e. y \|-> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) ) ) ) ) )
33		reseq2	\|- ( x = ( y u. { z } ) -> ( A \|` x ) = ( A \|` ( y u. { z } ) ) )
34	33	reseq2d	\|- ( x = ( y u. { z } ) -> ( F \|` ( A \|` x ) ) = ( F \|` ( A \|` ( y u. { z } ) ) ) )
35	34	oveq2d	\|- ( x = ( y u. { z } ) -> ( G gsum ( F \|` ( A \|` x ) ) ) = ( G gsum ( F \|` ( A \|` ( y u. { z } ) ) ) ) )
36		mpteq1	\|- ( x = ( y u. { z } ) -> ( j e. x \|-> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) ) = ( j e. ( y u. { z } ) \|-> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) ) )
37	36	oveq2d	\|- ( x = ( y u. { z } ) -> ( G gsum ( j e. x \|-> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) ) ) = ( G gsum ( j e. ( y u. { z } ) \|-> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) ) ) )
38	35 37	eqeq12d	\|- ( x = ( y u. { z } ) -> ( ( G gsum ( F \|` ( A \|` x ) ) ) = ( G gsum ( j e. x \|-> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) ) ) <-> ( G gsum ( F \|` ( A \|` ( y u. { z } ) ) ) ) = ( G gsum ( j e. ( y u. { z } ) \|-> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) ) ) ) )
39	38	imbi2d	\|- ( x = ( y u. { z } ) -> ( ( ph -> ( G gsum ( F \|` ( A \|` x ) ) ) = ( G gsum ( j e. x \|-> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) ) ) ) <-> ( ph -> ( G gsum ( F \|` ( A \|` ( y u. { z } ) ) ) ) = ( G gsum ( j e. ( y u. { z } ) \|-> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) ) ) ) ) )
40		reseq2	\|- ( x = dom ( F supp .0. ) -> ( A \|` x ) = ( A \|` dom ( F supp .0. ) ) )
41	40	reseq2d	\|- ( x = dom ( F supp .0. ) -> ( F \|` ( A \|` x ) ) = ( F \|` ( A \|` dom ( F supp .0. ) ) ) )
42	41	oveq2d	\|- ( x = dom ( F supp .0. ) -> ( G gsum ( F \|` ( A \|` x ) ) ) = ( G gsum ( F \|` ( A \|` dom ( F supp .0. ) ) ) ) )
43		mpteq1	\|- ( x = dom ( F supp .0. ) -> ( j e. x \|-> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) ) = ( j e. dom ( F supp .0. ) \|-> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) ) )
44	43	oveq2d	\|- ( x = dom ( F supp .0. ) -> ( G gsum ( j e. x \|-> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) ) ) = ( G gsum ( j e. dom ( F supp .0. ) \|-> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) ) ) )
45	42 44	eqeq12d	\|- ( x = dom ( F supp .0. ) -> ( ( G gsum ( F \|` ( A \|` x ) ) ) = ( G gsum ( j e. x \|-> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) ) ) <-> ( G gsum ( F \|` ( A \|` dom ( F supp .0. ) ) ) ) = ( G gsum ( j e. dom ( F supp .0. ) \|-> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) ) ) ) )
46	45	imbi2d	\|- ( x = dom ( F supp .0. ) -> ( ( ph -> ( G gsum ( F \|` ( A \|` x ) ) ) = ( G gsum ( j e. x \|-> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) ) ) ) <-> ( ph -> ( G gsum ( F \|` ( A \|` dom ( F supp .0. ) ) ) ) = ( G gsum ( j e. dom ( F supp .0. ) \|-> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) ) ) ) ) )
47		eqidd	\|- ( ph -> ( G gsum (/) ) = ( G gsum (/) ) )
48		oveq1	\|- ( ( G gsum ( F \|` ( A \|` y ) ) ) = ( G gsum ( j e. y \|-> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) ) ) -> ( ( G gsum ( F \|` ( A \|` y ) ) ) ( +g ` G ) ( G gsum ( F \|` ( A \|` { z } ) ) ) ) = ( ( G gsum ( j e. y \|-> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) ) ) ( +g ` G ) ( G gsum ( F \|` ( A \|` { z } ) ) ) ) )
49		eqid	\|- ( +g ` G ) = ( +g ` G )
50	3	adantr	\|- ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> G e. CMnd )
51	4	resexd	\|- ( ph -> ( A \|` ( y u. { z } ) ) e. _V )
52	51	adantr	\|- ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> ( A \|` ( y u. { z } ) ) e. _V )
53		resss	\|- ( A \|` ( y u. { z } ) ) C_ A
54		fssres	\|- ( ( F : A --> B /\ ( A \|` ( y u. { z } ) ) C_ A ) -> ( F \|` ( A \|` ( y u. { z } ) ) ) : ( A \|` ( y u. { z } ) ) --> B )
55	8 53 54	sylancl	\|- ( ph -> ( F \|` ( A \|` ( y u. { z } ) ) ) : ( A \|` ( y u. { z } ) ) --> B )
56	55	adantr	\|- ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> ( F \|` ( A \|` ( y u. { z } ) ) ) : ( A \|` ( y u. { z } ) ) --> B )
57	8	ffund	\|- ( ph -> Fun F )
58	57	funresd	\|- ( ph -> Fun ( F \|` ( A \|` ( y u. { z } ) ) ) )
59	58	adantr	\|- ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> Fun ( F \|` ( A \|` ( y u. { z } ) ) ) )
60	10	adantr	\|- ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> ( F supp .0. ) e. Fin )
61	8 4	fexd	\|- ( ph -> F e. _V )
62	2	fvexi	\|- .0. e. _V
63		ressuppss	\|- ( ( F e. _V /\ .0. e. _V ) -> ( ( F \|` ( A \|` ( y u. { z } ) ) ) supp .0. ) C_ ( F supp .0. ) )
64	61 62 63	sylancl	\|- ( ph -> ( ( F \|` ( A \|` ( y u. { z } ) ) ) supp .0. ) C_ ( F supp .0. ) )
65	64	adantr	\|- ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> ( ( F \|` ( A \|` ( y u. { z } ) ) ) supp .0. ) C_ ( F supp .0. ) )
66	60 65	ssfid	\|- ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> ( ( F \|` ( A \|` ( y u. { z } ) ) ) supp .0. ) e. Fin )
67	61	resexd	\|- ( ph -> ( F \|` ( A \|` ( y u. { z } ) ) ) e. _V )
68		isfsupp	\|- ( ( ( F \|` ( A \|` ( y u. { z } ) ) ) e. _V /\ .0. e. _V ) -> ( ( F \|` ( A \|` ( y u. { z } ) ) ) finSupp .0. <-> ( Fun ( F \|` ( A \|` ( y u. { z } ) ) ) /\ ( ( F \|` ( A \|` ( y u. { z } ) ) ) supp .0. ) e. Fin ) ) )
69	67 62 68	sylancl	\|- ( ph -> ( ( F \|` ( A \|` ( y u. { z } ) ) ) finSupp .0. <-> ( Fun ( F \|` ( A \|` ( y u. { z } ) ) ) /\ ( ( F \|` ( A \|` ( y u. { z } ) ) ) supp .0. ) e. Fin ) ) )
70	69	adantr	\|- ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> ( ( F \|` ( A \|` ( y u. { z } ) ) ) finSupp .0. <-> ( Fun ( F \|` ( A \|` ( y u. { z } ) ) ) /\ ( ( F \|` ( A \|` ( y u. { z } ) ) ) supp .0. ) e. Fin ) ) )
71	59 66 70	mpbir2and	\|- ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> ( F \|` ( A \|` ( y u. { z } ) ) ) finSupp .0. )
72		simprr	\|- ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> -. z e. y )
73		disjsn	\|- ( ( y i^i { z } ) = (/) <-> -. z e. y )
74	72 73	sylibr	\|- ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> ( y i^i { z } ) = (/) )
75	74	reseq2d	\|- ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> ( A \|` ( y i^i { z } ) ) = ( A \|` (/) ) )
76		resindi	\|- ( A \|` ( y i^i { z } ) ) = ( ( A \|` y ) i^i ( A \|` { z } ) )
77	75 76 14	3eqtr3g	\|- ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> ( ( A \|` y ) i^i ( A \|` { z } ) ) = (/) )
78		resundi	\|- ( A \|` ( y u. { z } ) ) = ( ( A \|` y ) u. ( A \|` { z } ) )
79	78	a1i	\|- ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> ( A \|` ( y u. { z } ) ) = ( ( A \|` y ) u. ( A \|` { z } ) ) )
80	1 2 49 50 52 56 71 77 79	gsumsplit	\|- ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> ( G gsum ( F \|` ( A \|` ( y u. { z } ) ) ) ) = ( ( G gsum ( ( F \|` ( A \|` ( y u. { z } ) ) ) \|` ( A \|` y ) ) ) ( +g ` G ) ( G gsum ( ( F \|` ( A \|` ( y u. { z } ) ) ) \|` ( A \|` { z } ) ) ) ) )
81		ssun1	\|- y C_ ( y u. { z } )
82		ssres2	\|- ( y C_ ( y u. { z } ) -> ( A \|` y ) C_ ( A \|` ( y u. { z } ) ) )
83		resabs1	\|- ( ( A \|` y ) C_ ( A \|` ( y u. { z } ) ) -> ( ( F \|` ( A \|` ( y u. { z } ) ) ) \|` ( A \|` y ) ) = ( F \|` ( A \|` y ) ) )
84	81 82 83	mp2b	\|- ( ( F \|` ( A \|` ( y u. { z } ) ) ) \|` ( A \|` y ) ) = ( F \|` ( A \|` y ) )
85	84	oveq2i	\|- ( G gsum ( ( F \|` ( A \|` ( y u. { z } ) ) ) \|` ( A \|` y ) ) ) = ( G gsum ( F \|` ( A \|` y ) ) )
86		ssun2	\|- { z } C_ ( y u. { z } )
87		ssres2	\|- ( { z } C_ ( y u. { z } ) -> ( A \|` { z } ) C_ ( A \|` ( y u. { z } ) ) )
88		resabs1	\|- ( ( A \|` { z } ) C_ ( A \|` ( y u. { z } ) ) -> ( ( F \|` ( A \|` ( y u. { z } ) ) ) \|` ( A \|` { z } ) ) = ( F \|` ( A \|` { z } ) ) )
89	86 87 88	mp2b	\|- ( ( F \|` ( A \|` ( y u. { z } ) ) ) \|` ( A \|` { z } ) ) = ( F \|` ( A \|` { z } ) )
90	89	oveq2i	\|- ( G gsum ( ( F \|` ( A \|` ( y u. { z } ) ) ) \|` ( A \|` { z } ) ) ) = ( G gsum ( F \|` ( A \|` { z } ) ) )
91	85 90	oveq12i	\|- ( ( G gsum ( ( F \|` ( A \|` ( y u. { z } ) ) ) \|` ( A \|` y ) ) ) ( +g ` G ) ( G gsum ( ( F \|` ( A \|` ( y u. { z } ) ) ) \|` ( A \|` { z } ) ) ) ) = ( ( G gsum ( F \|` ( A \|` y ) ) ) ( +g ` G ) ( G gsum ( F \|` ( A \|` { z } ) ) ) )
92	80 91	eqtrdi	\|- ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> ( G gsum ( F \|` ( A \|` ( y u. { z } ) ) ) ) = ( ( G gsum ( F \|` ( A \|` y ) ) ) ( +g ` G ) ( G gsum ( F \|` ( A \|` { z } ) ) ) ) )
93		simprl	\|- ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> y e. Fin )
94	1 2 3 4 5 6 7 8 9	gsum2dlem1	\|- ( ph -> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) e. B )
95	94	ad2antrr	\|- ( ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) /\ j e. y ) -> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) e. B )
96		vex	\|- z e. _V
97	96	a1i	\|- ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> z e. _V )
98		sneq	\|- ( j = z -> { j } = { z } )
99	98	imaeq2d	\|- ( j = z -> ( A " { j } ) = ( A " { z } ) )
100		oveq1	\|- ( j = z -> ( j F k ) = ( z F k ) )
101	99 100	mpteq12dv	\|- ( j = z -> ( k e. ( A " { j } ) \|-> ( j F k ) ) = ( k e. ( A " { z } ) \|-> ( z F k ) ) )
102	101	oveq2d	\|- ( j = z -> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) = ( G gsum ( k e. ( A " { z } ) \|-> ( z F k ) ) ) )
103	102	eleq1d	\|- ( j = z -> ( ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) e. B <-> ( G gsum ( k e. ( A " { z } ) \|-> ( z F k ) ) ) e. B ) )
104	103	imbi2d	\|- ( j = z -> ( ( ph -> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) e. B ) <-> ( ph -> ( G gsum ( k e. ( A " { z } ) \|-> ( z F k ) ) ) e. B ) ) )
105	104 94	chvarvv	\|- ( ph -> ( G gsum ( k e. ( A " { z } ) \|-> ( z F k ) ) ) e. B )
106	105	adantr	\|- ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> ( G gsum ( k e. ( A " { z } ) \|-> ( z F k ) ) ) e. B )
107	1 49 50 93 95 97 72 106 102	gsumunsn	\|- ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> ( G gsum ( j e. ( y u. { z } ) \|-> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) ) ) = ( ( G gsum ( j e. y \|-> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) ) ) ( +g ` G ) ( G gsum ( k e. ( A " { z } ) \|-> ( z F k ) ) ) ) )
108	98	reseq2d	\|- ( j = z -> ( A \|` { j } ) = ( A \|` { z } ) )
109	108	reseq2d	\|- ( j = z -> ( F \|` ( A \|` { j } ) ) = ( F \|` ( A \|` { z } ) ) )
110	109	oveq2d	\|- ( j = z -> ( G gsum ( F \|` ( A \|` { j } ) ) ) = ( G gsum ( F \|` ( A \|` { z } ) ) ) )
111	102 110	eqeq12d	\|- ( j = z -> ( ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) = ( G gsum ( F \|` ( A \|` { j } ) ) ) <-> ( G gsum ( k e. ( A " { z } ) \|-> ( z F k ) ) ) = ( G gsum ( F \|` ( A \|` { z } ) ) ) ) )
112	111	imbi2d	\|- ( j = z -> ( ( ph -> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) = ( G gsum ( F \|` ( A \|` { j } ) ) ) ) <-> ( ph -> ( G gsum ( k e. ( A " { z } ) \|-> ( z F k ) ) ) = ( G gsum ( F \|` ( A \|` { z } ) ) ) ) ) )
113		imaexg	\|- ( A e. V -> ( A " { j } ) e. _V )
114	4 113	syl	\|- ( ph -> ( A " { j } ) e. _V )
115		vex	\|- j e. _V
116		vex	\|- k e. _V
117	115 116	elimasn	\|- ( k e. ( A " { j } ) <-> <. j , k >. e. A )
118		df-ov	\|- ( j F k ) = ( F ` <. j , k >. )
119	8	ffvelcdmda	\|- ( ( ph /\ <. j , k >. e. A ) -> ( F ` <. j , k >. ) e. B )
120	118 119	eqeltrid	\|- ( ( ph /\ <. j , k >. e. A ) -> ( j F k ) e. B )
121	117 120	sylan2b	\|- ( ( ph /\ k e. ( A " { j } ) ) -> ( j F k ) e. B )
122	121	fmpttd	\|- ( ph -> ( k e. ( A " { j } ) \|-> ( j F k ) ) : ( A " { j } ) --> B )
123		funmpt	\|- Fun ( k e. ( A " { j } ) \|-> ( j F k ) )
124	123	a1i	\|- ( ph -> Fun ( k e. ( A " { j } ) \|-> ( j F k ) ) )
125		rnfi	\|- ( ( F supp .0. ) e. Fin -> ran ( F supp .0. ) e. Fin )
126	10 125	syl	\|- ( ph -> ran ( F supp .0. ) e. Fin )
127	117	biimpi	\|- ( k e. ( A " { j } ) -> <. j , k >. e. A )
128	115 116	opelrn	\|- ( <. j , k >. e. ( F supp .0. ) -> k e. ran ( F supp .0. ) )
129	128	con3i	\|- ( -. k e. ran ( F supp .0. ) -> -. <. j , k >. e. ( F supp .0. ) )
130	127 129	anim12i	\|- ( ( k e. ( A " { j } ) /\ -. k e. ran ( F supp .0. ) ) -> ( <. j , k >. e. A /\ -. <. j , k >. e. ( F supp .0. ) ) )
131		eldif	\|- ( k e. ( ( A " { j } ) \ ran ( F supp .0. ) ) <-> ( k e. ( A " { j } ) /\ -. k e. ran ( F supp .0. ) ) )
132		eldif	\|- ( <. j , k >. e. ( A \ ( F supp .0. ) ) <-> ( <. j , k >. e. A /\ -. <. j , k >. e. ( F supp .0. ) ) )
133	130 131 132	3imtr4i	\|- ( k e. ( ( A " { j } ) \ ran ( F supp .0. ) ) -> <. j , k >. e. ( A \ ( F supp .0. ) ) )
134		ssidd	\|- ( ph -> ( F supp .0. ) C_ ( F supp .0. ) )
135	62	a1i	\|- ( ph -> .0. e. _V )
136	8 134 4 135	suppssr	\|- ( ( ph /\ <. j , k >. e. ( A \ ( F supp .0. ) ) ) -> ( F ` <. j , k >. ) = .0. )
137	118 136	eqtrid	\|- ( ( ph /\ <. j , k >. e. ( A \ ( F supp .0. ) ) ) -> ( j F k ) = .0. )
138	133 137	sylan2	\|- ( ( ph /\ k e. ( ( A " { j } ) \ ran ( F supp .0. ) ) ) -> ( j F k ) = .0. )
139	138 114	suppss2	\|- ( ph -> ( ( k e. ( A " { j } ) \|-> ( j F k ) ) supp .0. ) C_ ran ( F supp .0. ) )
140	126 139	ssfid	\|- ( ph -> ( ( k e. ( A " { j } ) \|-> ( j F k ) ) supp .0. ) e. Fin )
141	114	mptexd	\|- ( ph -> ( k e. ( A " { j } ) \|-> ( j F k ) ) e. _V )
142		isfsupp	\|- ( ( ( k e. ( A " { j } ) \|-> ( j F k ) ) e. _V /\ .0. e. _V ) -> ( ( k e. ( A " { j } ) \|-> ( j F k ) ) finSupp .0. <-> ( Fun ( k e. ( A " { j } ) \|-> ( j F k ) ) /\ ( ( k e. ( A " { j } ) \|-> ( j F k ) ) supp .0. ) e. Fin ) ) )
143	141 62 142	sylancl	\|- ( ph -> ( ( k e. ( A " { j } ) \|-> ( j F k ) ) finSupp .0. <-> ( Fun ( k e. ( A " { j } ) \|-> ( j F k ) ) /\ ( ( k e. ( A " { j } ) \|-> ( j F k ) ) supp .0. ) e. Fin ) ) )
144	124 140 143	mpbir2and	\|- ( ph -> ( k e. ( A " { j } ) \|-> ( j F k ) ) finSupp .0. )
145		2ndconst	\|- ( j e. _V -> ( 2nd \|` ( { j } X. ( A " { j } ) ) ) : ( { j } X. ( A " { j } ) ) -1-1-onto-> ( A " { j } ) )
146	115 145	mp1i	\|- ( ph -> ( 2nd \|` ( { j } X. ( A " { j } ) ) ) : ( { j } X. ( A " { j } ) ) -1-1-onto-> ( A " { j } ) )
147	1 2 3 114 122 144 146	gsumf1o	\|- ( ph -> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) = ( G gsum ( ( k e. ( A " { j } ) \|-> ( j F k ) ) o. ( 2nd \|` ( { j } X. ( A " { j } ) ) ) ) ) )
148		1st2nd2	\|- ( x e. ( { j } X. ( A " { j } ) ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
149		xp1st	\|- ( x e. ( { j } X. ( A " { j } ) ) -> ( 1st ` x ) e. { j } )
150		elsni	\|- ( ( 1st ` x ) e. { j } -> ( 1st ` x ) = j )
151	149 150	syl	\|- ( x e. ( { j } X. ( A " { j } ) ) -> ( 1st ` x ) = j )
152	151	opeq1d	\|- ( x e. ( { j } X. ( A " { j } ) ) -> <. ( 1st ` x ) , ( 2nd ` x ) >. = <. j , ( 2nd ` x ) >. )
153	148 152	eqtrd	\|- ( x e. ( { j } X. ( A " { j } ) ) -> x = <. j , ( 2nd ` x ) >. )
154	153	fveq2d	\|- ( x e. ( { j } X. ( A " { j } ) ) -> ( F ` x ) = ( F ` <. j , ( 2nd ` x ) >. ) )
155		df-ov	\|- ( j F ( 2nd ` x ) ) = ( F ` <. j , ( 2nd ` x ) >. )
156	154 155	eqtr4di	\|- ( x e. ( { j } X. ( A " { j } ) ) -> ( F ` x ) = ( j F ( 2nd ` x ) ) )
157	156	mpteq2ia	\|- ( x e. ( { j } X. ( A " { j } ) ) \|-> ( F ` x ) ) = ( x e. ( { j } X. ( A " { j } ) ) \|-> ( j F ( 2nd ` x ) ) )
158	8	feqmptd	\|- ( ph -> F = ( x e. A \|-> ( F ` x ) ) )
159	158	reseq1d	\|- ( ph -> ( F \|` ( A \|` { j } ) ) = ( ( x e. A \|-> ( F ` x ) ) \|` ( A \|` { j } ) ) )
160		resss	\|- ( A \|` { j } ) C_ A
161		resmpt	\|- ( ( A \|` { j } ) C_ A -> ( ( x e. A \|-> ( F ` x ) ) \|` ( A \|` { j } ) ) = ( x e. ( A \|` { j } ) \|-> ( F ` x ) ) )
162	160 161	ax-mp	\|- ( ( x e. A \|-> ( F ` x ) ) \|` ( A \|` { j } ) ) = ( x e. ( A \|` { j } ) \|-> ( F ` x ) )
163		ressn	\|- ( A \|` { j } ) = ( { j } X. ( A " { j } ) )
164	163	mpteq1i	\|- ( x e. ( A \|` { j } ) \|-> ( F ` x ) ) = ( x e. ( { j } X. ( A " { j } ) ) \|-> ( F ` x ) )
165	162 164	eqtri	\|- ( ( x e. A \|-> ( F ` x ) ) \|` ( A \|` { j } ) ) = ( x e. ( { j } X. ( A " { j } ) ) \|-> ( F ` x ) )
166	159 165	eqtrdi	\|- ( ph -> ( F \|` ( A \|` { j } ) ) = ( x e. ( { j } X. ( A " { j } ) ) \|-> ( F ` x ) ) )
167		xp2nd	\|- ( x e. ( { j } X. ( A " { j } ) ) -> ( 2nd ` x ) e. ( A " { j } ) )
168	167	adantl	\|- ( ( ph /\ x e. ( { j } X. ( A " { j } ) ) ) -> ( 2nd ` x ) e. ( A " { j } ) )
169		fo2nd	\|- 2nd : _V -onto-> _V
170		fof	\|- ( 2nd : _V -onto-> _V -> 2nd : _V --> _V )
171	169 170	mp1i	\|- ( ph -> 2nd : _V --> _V )
172	171	feqmptd	\|- ( ph -> 2nd = ( x e. _V \|-> ( 2nd ` x ) ) )
173	172	reseq1d	\|- ( ph -> ( 2nd \|` ( { j } X. ( A " { j } ) ) ) = ( ( x e. _V \|-> ( 2nd ` x ) ) \|` ( { j } X. ( A " { j } ) ) ) )
174		ssv	\|- ( { j } X. ( A " { j } ) ) C_ _V
175		resmpt	\|- ( ( { j } X. ( A " { j } ) ) C_ _V -> ( ( x e. _V \|-> ( 2nd ` x ) ) \|` ( { j } X. ( A " { j } ) ) ) = ( x e. ( { j } X. ( A " { j } ) ) \|-> ( 2nd ` x ) ) )
176	174 175	ax-mp	\|- ( ( x e. _V \|-> ( 2nd ` x ) ) \|` ( { j } X. ( A " { j } ) ) ) = ( x e. ( { j } X. ( A " { j } ) ) \|-> ( 2nd ` x ) )
177	173 176	eqtrdi	\|- ( ph -> ( 2nd \|` ( { j } X. ( A " { j } ) ) ) = ( x e. ( { j } X. ( A " { j } ) ) \|-> ( 2nd ` x ) ) )
178		eqidd	\|- ( ph -> ( k e. ( A " { j } ) \|-> ( j F k ) ) = ( k e. ( A " { j } ) \|-> ( j F k ) ) )
179		oveq2	\|- ( k = ( 2nd ` x ) -> ( j F k ) = ( j F ( 2nd ` x ) ) )
180	168 177 178 179	fmptco	\|- ( ph -> ( ( k e. ( A " { j } ) \|-> ( j F k ) ) o. ( 2nd \|` ( { j } X. ( A " { j } ) ) ) ) = ( x e. ( { j } X. ( A " { j } ) ) \|-> ( j F ( 2nd ` x ) ) ) )
181	157 166 180	3eqtr4a	\|- ( ph -> ( F \|` ( A \|` { j } ) ) = ( ( k e. ( A " { j } ) \|-> ( j F k ) ) o. ( 2nd \|` ( { j } X. ( A " { j } ) ) ) ) )
182	181	oveq2d	\|- ( ph -> ( G gsum ( F \|` ( A \|` { j } ) ) ) = ( G gsum ( ( k e. ( A " { j } ) \|-> ( j F k ) ) o. ( 2nd \|` ( { j } X. ( A " { j } ) ) ) ) ) )
183	147 182	eqtr4d	\|- ( ph -> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) = ( G gsum ( F \|` ( A \|` { j } ) ) ) )
184	112 183	chvarvv	\|- ( ph -> ( G gsum ( k e. ( A " { z } ) \|-> ( z F k ) ) ) = ( G gsum ( F \|` ( A \|` { z } ) ) ) )
185	184	adantr	\|- ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> ( G gsum ( k e. ( A " { z } ) \|-> ( z F k ) ) ) = ( G gsum ( F \|` ( A \|` { z } ) ) ) )
186	185	oveq2d	\|- ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> ( ( G gsum ( j e. y \|-> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) ) ) ( +g ` G ) ( G gsum ( k e. ( A " { z } ) \|-> ( z F k ) ) ) ) = ( ( G gsum ( j e. y \|-> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) ) ) ( +g ` G ) ( G gsum ( F \|` ( A \|` { z } ) ) ) ) )
187	107 186	eqtrd	\|- ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> ( G gsum ( j e. ( y u. { z } ) \|-> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) ) ) = ( ( G gsum ( j e. y \|-> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) ) ) ( +g ` G ) ( G gsum ( F \|` ( A \|` { z } ) ) ) ) )
188	92 187	eqeq12d	\|- ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> ( ( G gsum ( F \|` ( A \|` ( y u. { z } ) ) ) ) = ( G gsum ( j e. ( y u. { z } ) \|-> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) ) ) <-> ( ( G gsum ( F \|` ( A \|` y ) ) ) ( +g ` G ) ( G gsum ( F \|` ( A \|` { z } ) ) ) ) = ( ( G gsum ( j e. y \|-> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) ) ) ( +g ` G ) ( G gsum ( F \|` ( A \|` { z } ) ) ) ) ) )
189	48 188	imbitrrid	\|- ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> ( ( G gsum ( F \|` ( A \|` y ) ) ) = ( G gsum ( j e. y \|-> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) ) ) -> ( G gsum ( F \|` ( A \|` ( y u. { z } ) ) ) ) = ( G gsum ( j e. ( y u. { z } ) \|-> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) ) ) ) )
190	189	expcom	\|- ( ( y e. Fin /\ -. z e. y ) -> ( ph -> ( ( G gsum ( F \|` ( A \|` y ) ) ) = ( G gsum ( j e. y \|-> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) ) ) -> ( G gsum ( F \|` ( A \|` ( y u. { z } ) ) ) ) = ( G gsum ( j e. ( y u. { z } ) \|-> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) ) ) ) ) )
191	190	a2d	\|- ( ( y e. Fin /\ -. z e. y ) -> ( ( ph -> ( G gsum ( F \|` ( A \|` y ) ) ) = ( G gsum ( j e. y \|-> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) ) ) ) -> ( ph -> ( G gsum ( F \|` ( A \|` ( y u. { z } ) ) ) ) = ( G gsum ( j e. ( y u. { z } ) \|-> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) ) ) ) ) )
192	25 32 39 46 47 191	findcard2s	\|- ( dom ( F supp .0. ) e. Fin -> ( ph -> ( G gsum ( F \|` ( A \|` dom ( F supp .0. ) ) ) ) = ( G gsum ( j e. dom ( F supp .0. ) \|-> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) ) ) ) )
193	12 192	mpcom	\|- ( ph -> ( G gsum ( F \|` ( A \|` dom ( F supp .0. ) ) ) ) = ( G gsum ( j e. dom ( F supp .0. ) \|-> ( G gsum ( k e. ( A " { j } ) \|-> ( j F k ) ) ) ) ) )

Metamath Proof Explorer

Theorem gsum2dlem2

Proof