This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 ) ) ) ) ) )