Metamath Proof Explorer

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