Theorem psrmonprod

Description: Finite product of bags of variables in a power series. Here the function G maps a bag of variables to the corresponding monomial. (Contributed by Thierry Arnoux, 16-Mar-2026)

	Ref	Expression
Hypotheses	psrmonprod.s	|- S = ( I mPwSer R )
	psrmonprod.b	|- B = ( Base ` S )
	psrmonprod.r	|- ( ph -> R e. CRing )
	psrmonprod.i	|- ( ph -> I e. V )
	psrmonprod.d	|- D = { h e. ( NN0 ^m I ) | h finSupp 0 }
	psrmonprod.a	|- ( ph -> A e. Fin )
	psrmonprod.f	|- ( ph -> F : A --> D )
	psrmonprod.1	|- .1. = ( 1r ` R )
	psrmonprod.0	|- .0. = ( 0g ` R )
	psrmonprod.m	|- M = ( mulGrp ` S )
	psrmonprod.g	|- G = ( y e. D |-> ( z e. D |-> if ( z = y , .1. , .0. ) ) )
Assertion	psrmonprod	|- ( ph -> ( M gsum ( G o. F ) ) = ( G ` ( i e. I |-> ( CCfld gsum ( x e. A |-> ( ( F ` x ) ` i ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		psrmonprod.s	|- S = ( I mPwSer R )
2		psrmonprod.b	|- B = ( Base ` S )
3		psrmonprod.r	|- ( ph -> R e. CRing )
4		psrmonprod.i	|- ( ph -> I e. V )
5		psrmonprod.d	|- D = { h e. ( NN0 ^m I ) | h finSupp 0 }
6		psrmonprod.a	|- ( ph -> A e. Fin )
7		psrmonprod.f	|- ( ph -> F : A --> D )
8		psrmonprod.1	|- .1. = ( 1r ` R )
9		psrmonprod.0	|- .0. = ( 0g ` R )
10		psrmonprod.m	|- M = ( mulGrp ` S )
11		psrmonprod.g	|- G = ( y e. D |-> ( z e. D |-> if ( z = y , .1. , .0. ) ) )
12	7	ffvelcdmda	|- ( ( ph /\ k e. A ) -> ( F ` k ) e. D )
13	7	feqmptd	|- ( ph -> F = ( k e. A |-> ( F ` k ) ) )
14		fvexd	|- ( ( ph /\ y e. D ) -> ( Base ` R ) e. _V )
15		ovex	|- ( NN0 ^m I ) e. _V
16	5 15	rabex2	|- D e. _V
17	16	a1i	|- ( ( ph /\ y e. D ) -> D e. _V )
18		eqid	|- ( Base ` R ) = ( Base ` R )
19	3	crngringd	|- ( ph -> R e. Ring )
20	18 8 19	ringidcld	|- ( ph -> .1. e. ( Base ` R ) )
21	20	ad2antrr	|- ( ( ( ph /\ y e. D ) /\ z e. D ) -> .1. e. ( Base ` R ) )
22	3	crnggrpd	|- ( ph -> R e. Grp )
23	18 9	grpidcl	|- ( R e. Grp -> .0. e. ( Base ` R ) )
24	22 23	syl	|- ( ph -> .0. e. ( Base ` R ) )
25	24	ad2antrr	|- ( ( ( ph /\ y e. D ) /\ z e. D ) -> .0. e. ( Base ` R ) )
26	21 25	ifcld	|- ( ( ( ph /\ y e. D ) /\ z e. D ) -> if ( z = y , .1. , .0. ) e. ( Base ` R ) )
27	26	fmpttd	|- ( ( ph /\ y e. D ) -> ( z e. D |-> if ( z = y , .1. , .0. ) ) : D --> ( Base ` R ) )
28	14 17 27	elmapdd	|- ( ( ph /\ y e. D ) -> ( z e. D |-> if ( z = y , .1. , .0. ) ) e. ( ( Base ` R ) ^m D ) )
29	5	psrbasfsupp	|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
30	1 18 29 2 4	psrbas	|- ( ph -> B = ( ( Base ` R ) ^m D ) )
31	30	adantr	|- ( ( ph /\ y e. D ) -> B = ( ( Base ` R ) ^m D ) )
32	28 31	eleqtrrd	|- ( ( ph /\ y e. D ) -> ( z e. D |-> if ( z = y , .1. , .0. ) ) e. B )
33	32 11	fmptd	|- ( ph -> G : D --> B )
34	33	feqmptd	|- ( ph -> G = ( y e. D |-> ( G ` y ) ) )
35		fveq2	|- ( y = ( F ` k ) -> ( G ` y ) = ( G ` ( F ` k ) ) )
36	12 13 34 35	fmptco	|- ( ph -> ( G o. F ) = ( k e. A |-> ( G ` ( F ` k ) ) ) )
37	36	oveq2d	|- ( ph -> ( M gsum ( G o. F ) ) = ( M gsum ( k e. A |-> ( G ` ( F ` k ) ) ) ) )
38		mpteq1	|- ( a = (/) -> ( k e. a |-> ( G ` ( F ` k ) ) ) = ( k e. (/) |-> ( G ` ( F ` k ) ) ) )
39	38	oveq2d	|- ( a = (/) -> ( M gsum ( k e. a |-> ( G ` ( F ` k ) ) ) ) = ( M gsum ( k e. (/) |-> ( G ` ( F ` k ) ) ) ) )
40		mpteq1	|- ( a = (/) -> ( x e. a |-> ( ( F ` x ) ` i ) ) = ( x e. (/) |-> ( ( F ` x ) ` i ) ) )
41	40	oveq2d	|- ( a = (/) -> ( CCfld gsum ( x e. a |-> ( ( F ` x ) ` i ) ) ) = ( CCfld gsum ( x e. (/) |-> ( ( F ` x ) ` i ) ) ) )
42	41	mpteq2dv	|- ( a = (/) -> ( i e. I |-> ( CCfld gsum ( x e. a |-> ( ( F ` x ) ` i ) ) ) ) = ( i e. I |-> ( CCfld gsum ( x e. (/) |-> ( ( F ` x ) ` i ) ) ) ) )
43	42	fveq2d	|- ( a = (/) -> ( G ` ( i e. I |-> ( CCfld gsum ( x e. a |-> ( ( F ` x ) ` i ) ) ) ) ) = ( G ` ( i e. I |-> ( CCfld gsum ( x e. (/) |-> ( ( F ` x ) ` i ) ) ) ) ) )
44	39 43	eqeq12d	|- ( a = (/) -> ( ( M gsum ( k e. a |-> ( G ` ( F ` k ) ) ) ) = ( G ` ( i e. I |-> ( CCfld gsum ( x e. a |-> ( ( F ` x ) ` i ) ) ) ) ) <-> ( M gsum ( k e. (/) |-> ( G ` ( F ` k ) ) ) ) = ( G ` ( i e. I |-> ( CCfld gsum ( x e. (/) |-> ( ( F ` x ) ` i ) ) ) ) ) ) )
45		mpteq1	|- ( a = b -> ( k e. a |-> ( G ` ( F ` k ) ) ) = ( k e. b |-> ( G ` ( F ` k ) ) ) )
46	45	oveq2d	|- ( a = b -> ( M gsum ( k e. a |-> ( G ` ( F ` k ) ) ) ) = ( M gsum ( k e. b |-> ( G ` ( F ` k ) ) ) ) )
47		mpteq1	|- ( a = b -> ( x e. a |-> ( ( F ` x ) ` i ) ) = ( x e. b |-> ( ( F ` x ) ` i ) ) )
48	47	oveq2d	|- ( a = b -> ( CCfld gsum ( x e. a |-> ( ( F ` x ) ` i ) ) ) = ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) )
49	48	mpteq2dv	|- ( a = b -> ( i e. I |-> ( CCfld gsum ( x e. a |-> ( ( F ` x ) ` i ) ) ) ) = ( i e. I |-> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) ) )
50	49	fveq2d	|- ( a = b -> ( G ` ( i e. I |-> ( CCfld gsum ( x e. a |-> ( ( F ` x ) ` i ) ) ) ) ) = ( G ` ( i e. I |-> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) ) ) )
51	46 50	eqeq12d	|- ( a = b -> ( ( M gsum ( k e. a |-> ( G ` ( F ` k ) ) ) ) = ( G ` ( i e. I |-> ( CCfld gsum ( x e. a |-> ( ( F ` x ) ` i ) ) ) ) ) <-> ( M gsum ( k e. b |-> ( G ` ( F ` k ) ) ) ) = ( G ` ( i e. I |-> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) ) ) ) )
52		mpteq1	|- ( a = ( b u. { f } ) -> ( k e. a |-> ( G ` ( F ` k ) ) ) = ( k e. ( b u. { f } ) |-> ( G ` ( F ` k ) ) ) )
53	52	oveq2d	|- ( a = ( b u. { f } ) -> ( M gsum ( k e. a |-> ( G ` ( F ` k ) ) ) ) = ( M gsum ( k e. ( b u. { f } ) |-> ( G ` ( F ` k ) ) ) ) )
54		mpteq1	|- ( a = ( b u. { f } ) -> ( x e. a |-> ( ( F ` x ) ` i ) ) = ( x e. ( b u. { f } ) |-> ( ( F ` x ) ` i ) ) )
55	54	oveq2d	|- ( a = ( b u. { f } ) -> ( CCfld gsum ( x e. a |-> ( ( F ` x ) ` i ) ) ) = ( CCfld gsum ( x e. ( b u. { f } ) |-> ( ( F ` x ) ` i ) ) ) )
56	55	mpteq2dv	|- ( a = ( b u. { f } ) -> ( i e. I |-> ( CCfld gsum ( x e. a |-> ( ( F ` x ) ` i ) ) ) ) = ( i e. I |-> ( CCfld gsum ( x e. ( b u. { f } ) |-> ( ( F ` x ) ` i ) ) ) ) )
57	56	fveq2d	|- ( a = ( b u. { f } ) -> ( G ` ( i e. I |-> ( CCfld gsum ( x e. a |-> ( ( F ` x ) ` i ) ) ) ) ) = ( G ` ( i e. I |-> ( CCfld gsum ( x e. ( b u. { f } ) |-> ( ( F ` x ) ` i ) ) ) ) ) )
58	53 57	eqeq12d	|- ( a = ( b u. { f } ) -> ( ( M gsum ( k e. a |-> ( G ` ( F ` k ) ) ) ) = ( G ` ( i e. I |-> ( CCfld gsum ( x e. a |-> ( ( F ` x ) ` i ) ) ) ) ) <-> ( M gsum ( k e. ( b u. { f } ) |-> ( G ` ( F ` k ) ) ) ) = ( G ` ( i e. I |-> ( CCfld gsum ( x e. ( b u. { f } ) |-> ( ( F ` x ) ` i ) ) ) ) ) ) )
59		mpteq1	|- ( a = A -> ( k e. a |-> ( G ` ( F ` k ) ) ) = ( k e. A |-> ( G ` ( F ` k ) ) ) )
60	59	oveq2d	|- ( a = A -> ( M gsum ( k e. a |-> ( G ` ( F ` k ) ) ) ) = ( M gsum ( k e. A |-> ( G ` ( F ` k ) ) ) ) )
61		mpteq1	|- ( a = A -> ( x e. a |-> ( ( F ` x ) ` i ) ) = ( x e. A |-> ( ( F ` x ) ` i ) ) )
62	61	oveq2d	|- ( a = A -> ( CCfld gsum ( x e. a |-> ( ( F ` x ) ` i ) ) ) = ( CCfld gsum ( x e. A |-> ( ( F ` x ) ` i ) ) ) )
63	62	mpteq2dv	|- ( a = A -> ( i e. I |-> ( CCfld gsum ( x e. a |-> ( ( F ` x ) ` i ) ) ) ) = ( i e. I |-> ( CCfld gsum ( x e. A |-> ( ( F ` x ) ` i ) ) ) ) )
64	63	fveq2d	|- ( a = A -> ( G ` ( i e. I |-> ( CCfld gsum ( x e. a |-> ( ( F ` x ) ` i ) ) ) ) ) = ( G ` ( i e. I |-> ( CCfld gsum ( x e. A |-> ( ( F ` x ) ` i ) ) ) ) ) )
65	60 64	eqeq12d	|- ( a = A -> ( ( M gsum ( k e. a |-> ( G ` ( F ` k ) ) ) ) = ( G ` ( i e. I |-> ( CCfld gsum ( x e. a |-> ( ( F ` x ) ` i ) ) ) ) ) <-> ( M gsum ( k e. A |-> ( G ` ( F ` k ) ) ) ) = ( G ` ( i e. I |-> ( CCfld gsum ( x e. A |-> ( ( F ` x ) ` i ) ) ) ) ) ) )
66		eqid	|- ( 1r ` S ) = ( 1r ` S )
67	10 66	ringidval	|- ( 1r ` S ) = ( 0g ` M )
68	67	gsum0	|- ( M gsum (/) ) = ( 1r ` S )
69		mpt0	|- ( k e. (/) |-> ( G ` ( F ` k ) ) ) = (/)
70	69	oveq2i	|- ( M gsum ( k e. (/) |-> ( G ` ( F ` k ) ) ) ) = ( M gsum (/) )
71	70	a1i	|- ( ph -> ( M gsum ( k e. (/) |-> ( G ` ( F ` k ) ) ) ) = ( M gsum (/) ) )
72		mpt0	|- ( x e. (/) |-> ( ( F ` x ) ` i ) ) = (/)
73	72	oveq2i	|- ( CCfld gsum ( x e. (/) |-> ( ( F ` x ) ` i ) ) ) = ( CCfld gsum (/) )
74		cnfld0	|- 0 = ( 0g ` CCfld )
75	74	gsum0	|- ( CCfld gsum (/) ) = 0
76	73 75	eqtri	|- ( CCfld gsum ( x e. (/) |-> ( ( F ` x ) ` i ) ) ) = 0
77	76	mpteq2i	|- ( i e. I |-> ( CCfld gsum ( x e. (/) |-> ( ( F ` x ) ` i ) ) ) ) = ( i e. I |-> 0 )
78		fconstmpt	|- ( I X. { 0 } ) = ( i e. I |-> 0 )
79	77 78	eqtr4i	|- ( i e. I |-> ( CCfld gsum ( x e. (/) |-> ( ( F ` x ) ` i ) ) ) ) = ( I X. { 0 } )
80	79	a1i	|- ( ph -> ( i e. I |-> ( CCfld gsum ( x e. (/) |-> ( ( F ` x ) ` i ) ) ) ) = ( I X. { 0 } ) )
81	80	eqeq2d	|- ( ph -> ( y = ( i e. I |-> ( CCfld gsum ( x e. (/) |-> ( ( F ` x ) ` i ) ) ) ) <-> y = ( I X. { 0 } ) ) )
82	81	biimpa	|- ( ( ph /\ y = ( i e. I |-> ( CCfld gsum ( x e. (/) |-> ( ( F ` x ) ` i ) ) ) ) ) -> y = ( I X. { 0 } ) )
83	82	eqeq2d	|- ( ( ph /\ y = ( i e. I |-> ( CCfld gsum ( x e. (/) |-> ( ( F ` x ) ` i ) ) ) ) ) -> ( z = y <-> z = ( I X. { 0 } ) ) )
84	83	ifbid	|- ( ( ph /\ y = ( i e. I |-> ( CCfld gsum ( x e. (/) |-> ( ( F ` x ) ` i ) ) ) ) ) -> if ( z = y , .1. , .0. ) = if ( z = ( I X. { 0 } ) , .1. , .0. ) )
85	84	mpteq2dv	|- ( ( ph /\ y = ( i e. I |-> ( CCfld gsum ( x e. (/) |-> ( ( F ` x ) ` i ) ) ) ) ) -> ( z e. D |-> if ( z = y , .1. , .0. ) ) = ( z e. D |-> if ( z = ( I X. { 0 } ) , .1. , .0. ) ) )
86	1 4 19 29 9 8 66	psr1	|- ( ph -> ( 1r ` S ) = ( z e. D |-> if ( z = ( I X. { 0 } ) , .1. , .0. ) ) )
87	86	adantr	|- ( ( ph /\ y = ( i e. I |-> ( CCfld gsum ( x e. (/) |-> ( ( F ` x ) ` i ) ) ) ) ) -> ( 1r ` S ) = ( z e. D |-> if ( z = ( I X. { 0 } ) , .1. , .0. ) ) )
88	85 87	eqtr4d	|- ( ( ph /\ y = ( i e. I |-> ( CCfld gsum ( x e. (/) |-> ( ( F ` x ) ` i ) ) ) ) ) -> ( z e. D |-> if ( z = y , .1. , .0. ) ) = ( 1r ` S ) )
89		breq1	|- ( h = ( i e. I |-> ( CCfld gsum ( x e. (/) |-> ( ( F ` x ) ` i ) ) ) ) -> ( h finSupp 0 <-> ( i e. I |-> ( CCfld gsum ( x e. (/) |-> ( ( F ` x ) ` i ) ) ) ) finSupp 0 ) )
90		nn0ex	|- NN0 e. _V
91	90	a1i	|- ( ph -> NN0 e. _V )
92		0nn0	|- 0 e. NN0
93	92	fconst6	|- ( I X. { 0 } ) : I --> NN0
94	93	a1i	|- ( ph -> ( I X. { 0 } ) : I --> NN0 )
95	91 4 94	elmapdd	|- ( ph -> ( I X. { 0 } ) e. ( NN0 ^m I ) )
96	79 95	eqeltrid	|- ( ph -> ( i e. I |-> ( CCfld gsum ( x e. (/) |-> ( ( F ` x ) ` i ) ) ) ) e. ( NN0 ^m I ) )
97	92	a1i	|- ( ph -> 0 e. NN0 )
98	4 97	fczfsuppd	|- ( ph -> ( I X. { 0 } ) finSupp 0 )
99	79 98	eqbrtrid	|- ( ph -> ( i e. I |-> ( CCfld gsum ( x e. (/) |-> ( ( F ` x ) ` i ) ) ) ) finSupp 0 )
100	89 96 99	elrabd	|- ( ph -> ( i e. I |-> ( CCfld gsum ( x e. (/) |-> ( ( F ` x ) ` i ) ) ) ) e. { h e. ( NN0 ^m I ) | h finSupp 0 } )
101	100 5	eleqtrrdi	|- ( ph -> ( i e. I |-> ( CCfld gsum ( x e. (/) |-> ( ( F ` x ) ` i ) ) ) ) e. D )
102		fvexd	|- ( ph -> ( 1r ` S ) e. _V )
103	11 88 101 102	fvmptd2	|- ( ph -> ( G ` ( i e. I |-> ( CCfld gsum ( x e. (/) |-> ( ( F ` x ) ` i ) ) ) ) ) = ( 1r ` S ) )
104	68 71 103	3eqtr4a	|- ( ph -> ( M gsum ( k e. (/) |-> ( G ` ( F ` k ) ) ) ) = ( G ` ( i e. I |-> ( CCfld gsum ( x e. (/) |-> ( ( F ` x ) ` i ) ) ) ) ) )
105		2fveq3	|- ( k = l -> ( G ` ( F ` k ) ) = ( G ` ( F ` l ) ) )
106	105	cbvmptv	|- ( k e. ( b u. { f } ) |-> ( G ` ( F ` k ) ) ) = ( l e. ( b u. { f } ) |-> ( G ` ( F ` l ) ) )
107	106	oveq2i	|- ( M gsum ( k e. ( b u. { f } ) |-> ( G ` ( F ` k ) ) ) ) = ( M gsum ( l e. ( b u. { f } ) |-> ( G ` ( F ` l ) ) ) )
108	10 2	mgpbas	|- B = ( Base ` M )
109		eqid	|- ( .r ` S ) = ( .r ` S )
110	10 109	mgpplusg	|- ( .r ` S ) = ( +g ` M )
111	1 4 3	psrcrng	|- ( ph -> S e. CRing )
112	10	crngmgp	|- ( S e. CRing -> M e. CMnd )
113	111 112	syl	|- ( ph -> M e. CMnd )
114	113	ad3antrrr	|- ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ ( M gsum ( k e. b |-> ( G ` ( F ` k ) ) ) ) = ( G ` ( i e. I |-> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) ) ) ) -> M e. CMnd )
115	6	adantr	|- ( ( ph /\ b C_ A ) -> A e. Fin )
116		simpr	|- ( ( ph /\ b C_ A ) -> b C_ A )
117	115 116	ssfid	|- ( ( ph /\ b C_ A ) -> b e. Fin )
118	117	ad2antrr	|- ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ ( M gsum ( k e. b |-> ( G ` ( F ` k ) ) ) ) = ( G ` ( i e. I |-> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) ) ) ) -> b e. Fin )
119	33	ad4antr	|- ( ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ ( M gsum ( k e. b |-> ( G ` ( F ` k ) ) ) ) = ( G ` ( i e. I |-> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) ) ) ) /\ l e. b ) -> G : D --> B )
120	7	ad4antr	|- ( ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ ( M gsum ( k e. b |-> ( G ` ( F ` k ) ) ) ) = ( G ` ( i e. I |-> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) ) ) ) /\ l e. b ) -> F : A --> D )
121		simpllr	|- ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ ( M gsum ( k e. b |-> ( G ` ( F ` k ) ) ) ) = ( G ` ( i e. I |-> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) ) ) ) -> b C_ A )
122	121	sselda	|- ( ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ ( M gsum ( k e. b |-> ( G ` ( F ` k ) ) ) ) = ( G ` ( i e. I |-> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) ) ) ) /\ l e. b ) -> l e. A )
123	120 122	ffvelcdmd	|- ( ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ ( M gsum ( k e. b |-> ( G ` ( F ` k ) ) ) ) = ( G ` ( i e. I |-> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) ) ) ) /\ l e. b ) -> ( F ` l ) e. D )
124	119 123	ffvelcdmd	|- ( ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ ( M gsum ( k e. b |-> ( G ` ( F ` k ) ) ) ) = ( G ` ( i e. I |-> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) ) ) ) /\ l e. b ) -> ( G ` ( F ` l ) ) e. B )
125		simplr	|- ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ ( M gsum ( k e. b |-> ( G ` ( F ` k ) ) ) ) = ( G ` ( i e. I |-> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) ) ) ) -> f e. ( A \ b ) )
126	125	eldifbd	|- ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ ( M gsum ( k e. b |-> ( G ` ( F ` k ) ) ) ) = ( G ` ( i e. I |-> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) ) ) ) -> -. f e. b )
127	33	ad3antrrr	|- ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ ( M gsum ( k e. b |-> ( G ` ( F ` k ) ) ) ) = ( G ` ( i e. I |-> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) ) ) ) -> G : D --> B )
128	7	ad3antrrr	|- ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ ( M gsum ( k e. b |-> ( G ` ( F ` k ) ) ) ) = ( G ` ( i e. I |-> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) ) ) ) -> F : A --> D )
129	125	eldifad	|- ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ ( M gsum ( k e. b |-> ( G ` ( F ` k ) ) ) ) = ( G ` ( i e. I |-> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) ) ) ) -> f e. A )
130	128 129	ffvelcdmd	|- ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ ( M gsum ( k e. b |-> ( G ` ( F ` k ) ) ) ) = ( G ` ( i e. I |-> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) ) ) ) -> ( F ` f ) e. D )
131	127 130	ffvelcdmd	|- ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ ( M gsum ( k e. b |-> ( G ` ( F ` k ) ) ) ) = ( G ` ( i e. I |-> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) ) ) ) -> ( G ` ( F ` f ) ) e. B )
132		2fveq3	|- ( l = f -> ( G ` ( F ` l ) ) = ( G ` ( F ` f ) ) )
133	108 110 114 118 124 125 126 131 132	gsumunsn	|- ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ ( M gsum ( k e. b |-> ( G ` ( F ` k ) ) ) ) = ( G ` ( i e. I |-> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) ) ) ) -> ( M gsum ( l e. ( b u. { f } ) |-> ( G ` ( F ` l ) ) ) ) = ( ( M gsum ( l e. b |-> ( G ` ( F ` l ) ) ) ) ( .r ` S ) ( G ` ( F ` f ) ) ) )
134	105	cbvmptv	|- ( k e. b |-> ( G ` ( F ` k ) ) ) = ( l e. b |-> ( G ` ( F ` l ) ) )
135	134	oveq2i	|- ( M gsum ( k e. b |-> ( G ` ( F ` k ) ) ) ) = ( M gsum ( l e. b |-> ( G ` ( F ` l ) ) ) )
136		id	|- ( ( M gsum ( k e. b |-> ( G ` ( F ` k ) ) ) ) = ( G ` ( i e. I |-> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) ) ) -> ( M gsum ( k e. b |-> ( G ` ( F ` k ) ) ) ) = ( G ` ( i e. I |-> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) ) ) )
137	135 136	eqtr3id	|- ( ( M gsum ( k e. b |-> ( G ` ( F ` k ) ) ) ) = ( G ` ( i e. I |-> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) ) ) -> ( M gsum ( l e. b |-> ( G ` ( F ` l ) ) ) ) = ( G ` ( i e. I |-> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) ) ) )
138	137	oveq1d	|- ( ( M gsum ( k e. b |-> ( G ` ( F ` k ) ) ) ) = ( G ` ( i e. I |-> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) ) ) -> ( ( M gsum ( l e. b |-> ( G ` ( F ` l ) ) ) ) ( .r ` S ) ( G ` ( F ` f ) ) ) = ( ( G ` ( i e. I |-> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) ) ) ( .r ` S ) ( G ` ( F ` f ) ) ) )
139	138	adantl	|- ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ ( M gsum ( k e. b |-> ( G ` ( F ` k ) ) ) ) = ( G ` ( i e. I |-> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) ) ) ) -> ( ( M gsum ( l e. b |-> ( G ` ( F ` l ) ) ) ) ( .r ` S ) ( G ` ( F ` f ) ) ) = ( ( G ` ( i e. I |-> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) ) ) ( .r ` S ) ( G ` ( F ` f ) ) ) )
140	4	ad2antrr	|- ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) -> I e. V )
141	19	ad2antrr	|- ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) -> R e. Ring )
142		breq1	|- ( h = ( i e. I |-> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) ) -> ( h finSupp 0 <-> ( i e. I |-> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) ) finSupp 0 ) )
143	90	a1i	|- ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) -> NN0 e. _V )
144		cnfldfld	|- CCfld e. Field
145		id	|- ( CCfld e. Field -> CCfld e. Field )
146	145	fldcrngd	|- ( CCfld e. Field -> CCfld e. CRing )
147		crngring	|- ( CCfld e. CRing -> CCfld e. Ring )
148		ringcmn	|- ( CCfld e. Ring -> CCfld e. CMnd )
149	146 147 148	3syl	|- ( CCfld e. Field -> CCfld e. CMnd )
150	144 149	ax-mp	|- CCfld e. CMnd
151	150	a1i	|- ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ i e. I ) -> CCfld e. CMnd )
152	117	ad2antrr	|- ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ i e. I ) -> b e. Fin )
153		nn0subm	|- NN0 e. ( SubMnd ` CCfld )
154	153	a1i	|- ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ i e. I ) -> NN0 e. ( SubMnd ` CCfld ) )
155	4	ad4antr	|- ( ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ i e. I ) /\ x e. b ) -> I e. V )
156	90	a1i	|- ( ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ i e. I ) /\ x e. b ) -> NN0 e. _V )
157	5	ssrab3	|- D C_ ( NN0 ^m I )
158	7	ad2antrr	|- ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) -> F : A --> D )
159	158	ad2antrr	|- ( ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ i e. I ) /\ x e. b ) -> F : A --> D )
160		simpllr	|- ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ i e. I ) -> b C_ A )
161	160	sselda	|- ( ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ i e. I ) /\ x e. b ) -> x e. A )
162	159 161	ffvelcdmd	|- ( ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ i e. I ) /\ x e. b ) -> ( F ` x ) e. D )
163	157 162	sselid	|- ( ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ i e. I ) /\ x e. b ) -> ( F ` x ) e. ( NN0 ^m I ) )
164	155 156 163	elmaprd	|- ( ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ i e. I ) /\ x e. b ) -> ( F ` x ) : I --> NN0 )
165		simplr	|- ( ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ i e. I ) /\ x e. b ) -> i e. I )
166	164 165	ffvelcdmd	|- ( ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ i e. I ) /\ x e. b ) -> ( ( F ` x ) ` i ) e. NN0 )
167	166	fmpttd	|- ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ i e. I ) -> ( x e. b |-> ( ( F ` x ) ` i ) ) : b --> NN0 )
168	92	a1i	|- ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ i e. I ) -> 0 e. NN0 )
169	167 152 168	fdmfifsupp	|- ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ i e. I ) -> ( x e. b |-> ( ( F ` x ) ` i ) ) finSupp 0 )
170	74 151 152 154 167 169	gsumsubmcl	|- ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ i e. I ) -> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) e. NN0 )
171	170	fmpttd	|- ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) -> ( i e. I |-> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) ) : I --> NN0 )
172	143 140 171	elmapdd	|- ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) -> ( i e. I |-> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) ) e. ( NN0 ^m I ) )
173	92	a1i	|- ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) -> 0 e. NN0 )
174	171	ffund	|- ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) -> Fun ( i e. I |-> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) ) )
175	117	adantr	|- ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) -> b e. Fin )
176	140	adantr	|- ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ x e. b ) -> I e. V )
177	90	a1i	|- ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ x e. b ) -> NN0 e. _V )
178	158	adantr	|- ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ x e. b ) -> F : A --> D )
179		simplr	|- ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) -> b C_ A )
180	179	sselda	|- ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ x e. b ) -> x e. A )
181	178 180	ffvelcdmd	|- ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ x e. b ) -> ( F ` x ) e. D )
182	157 181	sselid	|- ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ x e. b ) -> ( F ` x ) e. ( NN0 ^m I ) )
183	176 177 182	elmaprd	|- ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ x e. b ) -> ( F ` x ) : I --> NN0 )
184	183	feqmptd	|- ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ x e. b ) -> ( F ` x ) = ( i e. I |-> ( ( F ` x ) ` i ) ) )
185	184	oveq1d	|- ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ x e. b ) -> ( ( F ` x ) supp 0 ) = ( ( i e. I |-> ( ( F ` x ) ` i ) ) supp 0 ) )
186		breq1	|- ( h = ( F ` x ) -> ( h finSupp 0 <-> ( F ` x ) finSupp 0 ) )
187	181 5	eleqtrdi	|- ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ x e. b ) -> ( F ` x ) e. { h e. ( NN0 ^m I ) | h finSupp 0 } )
188	186 187	elrabrd	|- ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ x e. b ) -> ( F ` x ) finSupp 0 )
189	188	fsuppimpd	|- ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ x e. b ) -> ( ( F ` x ) supp 0 ) e. Fin )
190	185 189	eqeltrrd	|- ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ x e. b ) -> ( ( i e. I |-> ( ( F ` x ) ` i ) ) supp 0 ) e. Fin )
191	190	ralrimiva	|- ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) -> A. x e. b ( ( i e. I |-> ( ( F ` x ) ` i ) ) supp 0 ) e. Fin )
192		iunfi	|- ( ( b e. Fin /\ A. x e. b ( ( i e. I |-> ( ( F ` x ) ` i ) ) supp 0 ) e. Fin ) -> U_ x e. b ( ( i e. I |-> ( ( F ` x ) ` i ) ) supp 0 ) e. Fin )
193	175 191 192	syl2anc	|- ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) -> U_ x e. b ( ( i e. I |-> ( ( F ` x ) ` i ) ) supp 0 ) e. Fin )
194		cmnmnd	|- ( CCfld e. CMnd -> CCfld e. Mnd )
195	150 194	ax-mp	|- CCfld e. Mnd
196	195	a1i	|- ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) -> CCfld e. Mnd )
197	115	adantr	|- ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) -> A e. Fin )
198	197 179	ssexd	|- ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) -> b e. _V )
199	74 196 198 140 166	suppgsumssiun	|- ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) -> ( ( i e. I |-> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) ) supp 0 ) C_ U_ x e. b ( ( i e. I |-> ( ( F ` x ) ` i ) ) supp 0 ) )
200	193 199	ssfid	|- ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) -> ( ( i e. I |-> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) ) supp 0 ) e. Fin )
201	172 173 174 200	isfsuppd	|- ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) -> ( i e. I |-> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) ) finSupp 0 )
202	142 172 201	elrabd	|- ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) -> ( i e. I |-> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) ) e. { h e. ( NN0 ^m I ) | h finSupp 0 } )
203	202 5	eleqtrrdi	|- ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) -> ( i e. I |-> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) ) e. D )
204		difssd	|- ( ( ph /\ b C_ A ) -> ( A \ b ) C_ A )
205	204	sselda	|- ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) -> f e. A )
206	158 205	ffvelcdmd	|- ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) -> ( F ` f ) e. D )
207	1 2 9 8 5 140 141 203 109 206 11	psrmonmul2	|- ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) -> ( ( G ` ( i e. I |-> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) ) ) ( .r ` S ) ( G ` ( F ` f ) ) ) = ( G ` ( ( i e. I |-> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) ) oF + ( F ` f ) ) ) )
208	171	ffnd	|- ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) -> ( i e. I |-> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) ) Fn I )
209	157 206	sselid	|- ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) -> ( F ` f ) e. ( NN0 ^m I ) )
210	140 143 209	elmaprd	|- ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) -> ( F ` f ) : I --> NN0 )
211	210	ffnd	|- ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) -> ( F ` f ) Fn I )
212		nfv	|- F/ i ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) )
213		ovexd	|- ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ i e. I ) -> ( CCfld gsum ( x e. ( b u. { f } ) |-> ( ( F ` x ) ` i ) ) ) e. _V )
214		eqid	|- ( i e. I |-> ( CCfld gsum ( x e. ( b u. { f } ) |-> ( ( F ` x ) ` i ) ) ) ) = ( i e. I |-> ( CCfld gsum ( x e. ( b u. { f } ) |-> ( ( F ` x ) ` i ) ) ) )
215	212 213 214	fnmptd	|- ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) -> ( i e. I |-> ( CCfld gsum ( x e. ( b u. { f } ) |-> ( ( F ` x ) ` i ) ) ) ) Fn I )
216		eqid	|- ( i e. I |-> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) ) = ( i e. I |-> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) )
217		fveq2	|- ( i = j -> ( ( F ` x ) ` i ) = ( ( F ` x ) ` j ) )
218	217	mpteq2dv	|- ( i = j -> ( x e. b |-> ( ( F ` x ) ` i ) ) = ( x e. b |-> ( ( F ` x ) ` j ) ) )
219	218	oveq2d	|- ( i = j -> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) = ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` j ) ) ) )
220		simpr	|- ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ j e. I ) -> j e. I )
221		ovexd	|- ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ j e. I ) -> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` j ) ) ) e. _V )
222	216 219 220 221	fvmptd3	|- ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ j e. I ) -> ( ( i e. I |-> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) ) ` j ) = ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` j ) ) ) )
223		eqidd	|- ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ j e. I ) -> ( ( F ` f ) ` j ) = ( ( F ` f ) ` j ) )
224	217	mpteq2dv	|- ( i = j -> ( x e. ( b u. { f } ) |-> ( ( F ` x ) ` i ) ) = ( x e. ( b u. { f } ) |-> ( ( F ` x ) ` j ) ) )
225	224	oveq2d	|- ( i = j -> ( CCfld gsum ( x e. ( b u. { f } ) |-> ( ( F ` x ) ` i ) ) ) = ( CCfld gsum ( x e. ( b u. { f } ) |-> ( ( F ` x ) ` j ) ) ) )
226		ovexd	|- ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ j e. I ) -> ( CCfld gsum ( x e. ( b u. { f } ) |-> ( ( F ` x ) ` j ) ) ) e. _V )
227	214 225 220 226	fvmptd3	|- ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ j e. I ) -> ( ( i e. I |-> ( CCfld gsum ( x e. ( b u. { f } ) |-> ( ( F ` x ) ` i ) ) ) ) ` j ) = ( CCfld gsum ( x e. ( b u. { f } ) |-> ( ( F ` x ) ` j ) ) ) )
228		cnfldbas	|- CC = ( Base ` CCfld )
229		cnfldadd	|- + = ( +g ` CCfld )
230	150	a1i	|- ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ j e. I ) -> CCfld e. CMnd )
231	175	adantr	|- ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ j e. I ) -> b e. Fin )
232	183	adantlr	|- ( ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ j e. I ) /\ x e. b ) -> ( F ` x ) : I --> NN0 )
233		nn0sscn	|- NN0 C_ CC
234	233	a1i	|- ( ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ j e. I ) /\ x e. b ) -> NN0 C_ CC )
235	232 234	fssd	|- ( ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ j e. I ) /\ x e. b ) -> ( F ` x ) : I --> CC )
236		simplr	|- ( ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ j e. I ) /\ x e. b ) -> j e. I )
237	235 236	ffvelcdmd	|- ( ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ j e. I ) /\ x e. b ) -> ( ( F ` x ) ` j ) e. CC )
238		simplr	|- ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ j e. I ) -> f e. ( A \ b ) )
239	238	eldifbd	|- ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ j e. I ) -> -. f e. b )
240	210	adantr	|- ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ j e. I ) -> ( F ` f ) : I --> NN0 )
241	233	a1i	|- ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ j e. I ) -> NN0 C_ CC )
242	240 241	fssd	|- ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ j e. I ) -> ( F ` f ) : I --> CC )
243	242 220	ffvelcdmd	|- ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ j e. I ) -> ( ( F ` f ) ` j ) e. CC )
244		fveq2	|- ( x = f -> ( F ` x ) = ( F ` f ) )
245	244	fveq1d	|- ( x = f -> ( ( F ` x ) ` j ) = ( ( F ` f ) ` j ) )
246	228 229 230 231 237 238 239 243 245	gsumunsn	|- ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ j e. I ) -> ( CCfld gsum ( x e. ( b u. { f } ) |-> ( ( F ` x ) ` j ) ) ) = ( ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` j ) ) ) + ( ( F ` f ) ` j ) ) )
247	227 246	eqtr2d	|- ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ j e. I ) -> ( ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` j ) ) ) + ( ( F ` f ) ` j ) ) = ( ( i e. I |-> ( CCfld gsum ( x e. ( b u. { f } ) |-> ( ( F ` x ) ` i ) ) ) ) ` j ) )
248	140 208 211 215 222 223 247	offveq	|- ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) -> ( ( i e. I |-> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) ) oF + ( F ` f ) ) = ( i e. I |-> ( CCfld gsum ( x e. ( b u. { f } ) |-> ( ( F ` x ) ` i ) ) ) ) )
249	248	fveq2d	|- ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) -> ( G ` ( ( i e. I |-> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) ) oF + ( F ` f ) ) ) = ( G ` ( i e. I |-> ( CCfld gsum ( x e. ( b u. { f } ) |-> ( ( F ` x ) ` i ) ) ) ) ) )
250	207 249	eqtrd	|- ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) -> ( ( G ` ( i e. I |-> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) ) ) ( .r ` S ) ( G ` ( F ` f ) ) ) = ( G ` ( i e. I |-> ( CCfld gsum ( x e. ( b u. { f } ) |-> ( ( F ` x ) ` i ) ) ) ) ) )
251	250	adantr	|- ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ ( M gsum ( k e. b |-> ( G ` ( F ` k ) ) ) ) = ( G ` ( i e. I |-> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) ) ) ) -> ( ( G ` ( i e. I |-> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) ) ) ( .r ` S ) ( G ` ( F ` f ) ) ) = ( G ` ( i e. I |-> ( CCfld gsum ( x e. ( b u. { f } ) |-> ( ( F ` x ) ` i ) ) ) ) ) )
252	133 139 251	3eqtrd	|- ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ ( M gsum ( k e. b |-> ( G ` ( F ` k ) ) ) ) = ( G ` ( i e. I |-> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) ) ) ) -> ( M gsum ( l e. ( b u. { f } ) |-> ( G ` ( F ` l ) ) ) ) = ( G ` ( i e. I |-> ( CCfld gsum ( x e. ( b u. { f } ) |-> ( ( F ` x ) ` i ) ) ) ) ) )
253	107 252	eqtrid	|- ( ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) /\ ( M gsum ( k e. b |-> ( G ` ( F ` k ) ) ) ) = ( G ` ( i e. I |-> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) ) ) ) -> ( M gsum ( k e. ( b u. { f } ) |-> ( G ` ( F ` k ) ) ) ) = ( G ` ( i e. I |-> ( CCfld gsum ( x e. ( b u. { f } ) |-> ( ( F ` x ) ` i ) ) ) ) ) )
254	253	ex	|- ( ( ( ph /\ b C_ A ) /\ f e. ( A \ b ) ) -> ( ( M gsum ( k e. b |-> ( G ` ( F ` k ) ) ) ) = ( G ` ( i e. I |-> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) ) ) -> ( M gsum ( k e. ( b u. { f } ) |-> ( G ` ( F ` k ) ) ) ) = ( G ` ( i e. I |-> ( CCfld gsum ( x e. ( b u. { f } ) |-> ( ( F ` x ) ` i ) ) ) ) ) ) )
255	254	anasss	|- ( ( ph /\ ( b C_ A /\ f e. ( A \ b ) ) ) -> ( ( M gsum ( k e. b |-> ( G ` ( F ` k ) ) ) ) = ( G ` ( i e. I |-> ( CCfld gsum ( x e. b |-> ( ( F ` x ) ` i ) ) ) ) ) -> ( M gsum ( k e. ( b u. { f } ) |-> ( G ` ( F ` k ) ) ) ) = ( G ` ( i e. I |-> ( CCfld gsum ( x e. ( b u. { f } ) |-> ( ( F ` x ) ` i ) ) ) ) ) ) )
256	44 51 58 65 104 255 6	findcard2d	|- ( ph -> ( M gsum ( k e. A |-> ( G ` ( F ` k ) ) ) ) = ( G ` ( i e. I |-> ( CCfld gsum ( x e. A |-> ( ( F ` x ) ` i ) ) ) ) ) )
257	37 256	eqtrd	|- ( ph -> ( M gsum ( G o. F ) ) = ( G ` ( i e. I |-> ( CCfld gsum ( x e. A |-> ( ( F ` x ) ` i ) ) ) ) ) )