MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  gsumval3 Structured version   Unicode version

Theorem gsumval3 16374
Description: Value of the group sum operation over an arbitrary finite set. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by AV, 31-May-2019.)
Hypotheses
Ref Expression
gsumval3.b  |-  B  =  ( Base `  G
)
gsumval3.0  |-  .0.  =  ( 0g `  G )
gsumval3.p  |-  .+  =  ( +g  `  G )
gsumval3.z  |-  Z  =  (Cntz `  G )
gsumval3.g  |-  ( ph  ->  G  e.  Mnd )
gsumval3.a  |-  ( ph  ->  A  e.  V )
gsumval3.f  |-  ( ph  ->  F : A --> B )
gsumval3.c  |-  ( ph  ->  ran  F  C_  ( Z `  ran  F ) )
gsumval3.m  |-  ( ph  ->  M  e.  NN )
gsumval3.h  |-  ( ph  ->  H : ( 1 ... M ) -1-1-> A
)
gsumval3.n  |-  ( ph  ->  ( F supp  .0.  )  C_ 
ran  H )
gsumval3.w  |-  W  =  ( ( F  o.  H ) supp  .0.  )
Assertion
Ref Expression
gsumval3  |-  ( ph  ->  ( G  gsumg  F )  =  (  seq 1 (  .+  ,  ( F  o.  H ) ) `  M ) )

Proof of Theorem gsumval3
Dummy variables  f 
k  m  n  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 gsumval3.g . . . . 5  |-  ( ph  ->  G  e.  Mnd )
2 gsumval3.a . . . . 5  |-  ( ph  ->  A  e.  V )
3 gsumval3.0 . . . . . 6  |-  .0.  =  ( 0g `  G )
43gsumz 15500 . . . . 5  |-  ( ( G  e.  Mnd  /\  A  e.  V )  ->  ( G  gsumg  ( x  e.  A  |->  .0.  ) )  =  .0.  )
51, 2, 4syl2anc 661 . . . 4  |-  ( ph  ->  ( G  gsumg  ( x  e.  A  |->  .0.  ) )  =  .0.  )
65adantr 465 . . 3  |-  ( (
ph  /\  W  =  (/) )  ->  ( G  gsumg  ( x  e.  A  |->  .0.  ) )  =  .0.  )
7 gsumval3.f . . . . . . 7  |-  ( ph  ->  F : A --> B )
87feqmptd 5737 . . . . . 6  |-  ( ph  ->  F  =  ( x  e.  A  |->  ( F `
 x ) ) )
98adantr 465 . . . . 5  |-  ( (
ph  /\  W  =  (/) )  ->  F  =  ( x  e.  A  |->  ( F `  x
) ) )
10 gsumval3.h . . . . . . . . . . . . . 14  |-  ( ph  ->  H : ( 1 ... M ) -1-1-> A
)
11 f1f 5599 . . . . . . . . . . . . . 14  |-  ( H : ( 1 ... M ) -1-1-> A  ->  H : ( 1 ... M ) --> A )
1210, 11syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  H : ( 1 ... M ) --> A )
1312ad2antrr 725 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ran  H )  ->  H : ( 1 ... M ) --> A )
14 f1f1orn 5645 . . . . . . . . . . . . . . . 16  |-  ( H : ( 1 ... M ) -1-1-> A  ->  H : ( 1 ... M ) -1-1-onto-> ran  H )
1510, 14syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  H : ( 1 ... M ) -1-1-onto-> ran  H
)
1615adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  W  =  (/) )  ->  H :
( 1 ... M
)
-1-1-onto-> ran  H )
17 f1ocnv 5646 . . . . . . . . . . . . . 14  |-  ( H : ( 1 ... M ) -1-1-onto-> ran  H  ->  `' H : ran  H -1-1-onto-> ( 1 ... M ) )
18 f1of 5634 . . . . . . . . . . . . . 14  |-  ( `' H : ran  H -1-1-onto-> (
1 ... M )  ->  `' H : ran  H --> ( 1 ... M
) )
1916, 17, 183syl 20 . . . . . . . . . . . . 13  |-  ( (
ph  /\  W  =  (/) )  ->  `' H : ran  H --> ( 1 ... M ) )
2019ffvelrnda 5836 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ran  H )  -> 
( `' H `  x )  e.  ( 1 ... M ) )
21 fvco3 5761 . . . . . . . . . . . 12  |-  ( ( H : ( 1 ... M ) --> A  /\  ( `' H `  x )  e.  ( 1 ... M ) )  ->  ( ( F  o.  H ) `  ( `' H `  x ) )  =  ( F `  ( H `  ( `' H `  x )
) ) )
2213, 20, 21syl2anc 661 . . . . . . . . . . 11  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ran  H )  -> 
( ( F  o.  H ) `  ( `' H `  x ) )  =  ( F `
 ( H `  ( `' H `  x ) ) ) )
23 simpr 461 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  W  =  (/) )  ->  W  =  (/) )
2423difeq2d 3467 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  W  =  (/) )  ->  ( (
1 ... M )  \  W )  =  ( ( 1 ... M
)  \  (/) ) )
25 dif0 3742 . . . . . . . . . . . . . . 15  |-  ( ( 1 ... M ) 
\  (/) )  =  ( 1 ... M )
2624, 25syl6eq 2485 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  W  =  (/) )  ->  ( (
1 ... M )  \  W )  =  ( 1 ... M ) )
2726adantr 465 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ran  H )  -> 
( ( 1 ... M )  \  W
)  =  ( 1 ... M ) )
2820, 27eleqtrrd 2514 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ran  H )  -> 
( `' H `  x )  e.  ( ( 1 ... M
)  \  W )
)
29 fco 5561 . . . . . . . . . . . . . . 15  |-  ( ( F : A --> B  /\  H : ( 1 ... M ) --> A )  ->  ( F  o.  H ) : ( 1 ... M ) --> B )
307, 12, 29syl2anc 661 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( F  o.  H
) : ( 1 ... M ) --> B )
3130adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  W  =  (/) )  ->  ( F  o.  H ) : ( 1 ... M ) --> B )
32 gsumval3.w . . . . . . . . . . . . . . 15  |-  W  =  ( ( F  o.  H ) supp  .0.  )
3332eqimss2i 3404 . . . . . . . . . . . . . 14  |-  ( ( F  o.  H ) supp 
.0.  )  C_  W
3433a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  W  =  (/) )  ->  ( ( F  o.  H ) supp  .0.  )  C_  W )
35 ovex 6111 . . . . . . . . . . . . . 14  |-  ( 1 ... M )  e. 
_V
3635a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  W  =  (/) )  ->  ( 1 ... M )  e. 
_V )
37 fvex 5694 . . . . . . . . . . . . . . 15  |-  ( 0g
`  G )  e. 
_V
383, 37eqeltri 2507 . . . . . . . . . . . . . 14  |-  .0.  e.  _V
3938a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  W  =  (/) )  ->  .0.  e.  _V )
4031, 34, 36, 39suppssr 6715 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  W  =  (/) )  /\  ( `' H `  x )  e.  ( ( 1 ... M )  \  W ) )  -> 
( ( F  o.  H ) `  ( `' H `  x ) )  =  .0.  )
4128, 40syldan 470 . . . . . . . . . . 11  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ran  H )  -> 
( ( F  o.  H ) `  ( `' H `  x ) )  =  .0.  )
42 f1ocnvfv2 5977 . . . . . . . . . . . . 13  |-  ( ( H : ( 1 ... M ) -1-1-onto-> ran  H  /\  x  e.  ran  H )  ->  ( H `  ( `' H `  x ) )  =  x )
4316, 42sylan 471 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ran  H )  -> 
( H `  ( `' H `  x ) )  =  x )
4443fveq2d 5688 . . . . . . . . . . 11  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ran  H )  -> 
( F `  ( H `  ( `' H `  x )
) )  =  ( F `  x ) )
4522, 41, 443eqtr3rd 2478 . . . . . . . . . 10  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ran  H )  -> 
( F `  x
)  =  .0.  )
46 fvex 5694 . . . . . . . . . . 11  |-  ( F `
 x )  e. 
_V
4746elsnc 3894 . . . . . . . . . 10  |-  ( ( F `  x )  e.  {  .0.  }  <->  ( F `  x )  =  .0.  )
4845, 47sylibr 212 . . . . . . . . 9  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ran  H )  -> 
( F `  x
)  e.  {  .0.  } )
4948adantlr 714 . . . . . . . 8  |-  ( ( ( ( ph  /\  W  =  (/) )  /\  x  e.  A )  /\  x  e.  ran  H )  ->  ( F `  x )  e.  {  .0.  } )
50 eldif 3331 . . . . . . . . . . 11  |-  ( x  e.  ( A  \  ran  H )  <->  ( x  e.  A  /\  -.  x  e.  ran  H ) )
51 gsumval3.n . . . . . . . . . . . . 13  |-  ( ph  ->  ( F supp  .0.  )  C_ 
ran  H )
5238a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  .0.  e.  _V )
537, 51, 2, 52suppssr 6715 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( A  \  ran  H
) )  ->  ( F `  x )  =  .0.  )
5453, 47sylibr 212 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( A  \  ran  H
) )  ->  ( F `  x )  e.  {  .0.  } )
5550, 54sylan2br 476 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  A  /\  -.  x  e.  ran  H ) )  ->  ( F `  x )  e.  {  .0.  } )
5655adantlr 714 . . . . . . . . 9  |-  ( ( ( ph  /\  W  =  (/) )  /\  (
x  e.  A  /\  -.  x  e.  ran  H ) )  ->  ( F `  x )  e.  {  .0.  } )
5756anassrs 648 . . . . . . . 8  |-  ( ( ( ( ph  /\  W  =  (/) )  /\  x  e.  A )  /\  -.  x  e.  ran  H )  ->  ( F `  x )  e.  {  .0.  } )
5849, 57pm2.61dan 789 . . . . . . 7  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  A )  ->  ( F `  x )  e.  {  .0.  } )
5958, 47sylib 196 . . . . . 6  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  A )  ->  ( F `  x )  =  .0.  )
6059mpteq2dva 4371 . . . . 5  |-  ( (
ph  /\  W  =  (/) )  ->  ( x  e.  A  |->  ( F `
 x ) )  =  ( x  e.  A  |->  .0.  ) )
619, 60eqtrd 2469 . . . 4  |-  ( (
ph  /\  W  =  (/) )  ->  F  =  ( x  e.  A  |->  .0.  ) )
6261oveq2d 6102 . . 3  |-  ( (
ph  /\  W  =  (/) )  ->  ( G  gsumg  F )  =  ( G 
gsumg  ( x  e.  A  |->  .0.  ) ) )
63 gsumval3.b . . . . . . . 8  |-  B  =  ( Base `  G
)
6463, 3mndidcl 15431 . . . . . . 7  |-  ( G  e.  Mnd  ->  .0.  e.  B )
651, 64syl 16 . . . . . 6  |-  ( ph  ->  .0.  e.  B )
66 gsumval3.p . . . . . . 7  |-  .+  =  ( +g  `  G )
6763, 66, 3mndlid 15433 . . . . . 6  |-  ( ( G  e.  Mnd  /\  .0.  e.  B )  -> 
(  .0.  .+  .0.  )  =  .0.  )
681, 65, 67syl2anc 661 . . . . 5  |-  ( ph  ->  (  .0.  .+  .0.  )  =  .0.  )
6968adantr 465 . . . 4  |-  ( (
ph  /\  W  =  (/) )  ->  (  .0.  .+  .0.  )  =  .0.  )
70 gsumval3.m . . . . . 6  |-  ( ph  ->  M  e.  NN )
71 nnuz 10888 . . . . . 6  |-  NN  =  ( ZZ>= `  1 )
7270, 71syl6eleq 2527 . . . . 5  |-  ( ph  ->  M  e.  ( ZZ>= ` 
1 ) )
7372adantr 465 . . . 4  |-  ( (
ph  /\  W  =  (/) )  ->  M  e.  ( ZZ>= `  1 )
)
7426eleq2d 2504 . . . . . 6  |-  ( (
ph  /\  W  =  (/) )  ->  ( x  e.  ( ( 1 ... M )  \  W
)  <->  x  e.  (
1 ... M ) ) )
7574biimpar 485 . . . . 5  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ( 1 ... M
) )  ->  x  e.  ( ( 1 ... M )  \  W
) )
7631, 34, 36, 39suppssr 6715 . . . . 5  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ( ( 1 ... M )  \  W
) )  ->  (
( F  o.  H
) `  x )  =  .0.  )
7775, 76syldan 470 . . . 4  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ( 1 ... M
) )  ->  (
( F  o.  H
) `  x )  =  .0.  )
7869, 73, 77seqid3 11842 . . 3  |-  ( (
ph  /\  W  =  (/) )  ->  (  seq 1 (  .+  , 
( F  o.  H
) ) `  M
)  =  .0.  )
796, 62, 783eqtr4d 2479 . 2  |-  ( (
ph  /\  W  =  (/) )  ->  ( G  gsumg  F )  =  (  seq 1 (  .+  , 
( F  o.  H
) ) `  M
) )
80 fzf 11433 . . . . 5  |-  ... :
( ZZ  X.  ZZ )
--> ~P ZZ
81 ffn 5552 . . . . 5  |-  ( ...
: ( ZZ  X.  ZZ ) --> ~P ZZ  ->  ... 
Fn  ( ZZ  X.  ZZ ) )
82 ovelrn 6234 . . . . 5  |-  ( ... 
Fn  ( ZZ  X.  ZZ )  ->  ( A  e.  ran  ...  <->  E. m  e.  ZZ  E. n  e.  ZZ  A  =  ( m ... n ) ) )
8380, 81, 82mp2b 10 . . . 4  |-  ( A  e.  ran  ...  <->  E. m  e.  ZZ  E. n  e.  ZZ  A  =  ( m ... n ) )
841ad2antrr 725 . . . . . . . . 9  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  ->  G  e.  Mnd )
85 simpr 461 . . . . . . . . . . 11  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  ->  A  =  ( m ... n ) )
86 frel 5555 . . . . . . . . . . . . . . . . 17  |-  ( F : A --> B  ->  Rel  F )
87 reldm0 5049 . . . . . . . . . . . . . . . . 17  |-  ( Rel 
F  ->  ( F  =  (/)  <->  dom  F  =  (/) ) )
887, 86, 873syl 20 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( F  =  (/)  <->  dom  F  =  (/) ) )
89 fdm 5556 . . . . . . . . . . . . . . . . . 18  |-  ( F : A --> B  ->  dom  F  =  A )
907, 89syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  dom  F  =  A )
9190eqeq1d 2445 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( dom  F  =  (/) 
<->  A  =  (/) ) )
9288, 91bitrd 253 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( F  =  (/)  <->  A  =  (/) ) )
93 coeq1 4989 . . . . . . . . . . . . . . . . . . 19  |-  ( F  =  (/)  ->  ( F  o.  H )  =  ( (/)  o.  H
) )
94 co01 5345 . . . . . . . . . . . . . . . . . . 19  |-  ( (/)  o.  H )  =  (/)
9593, 94syl6eq 2485 . . . . . . . . . . . . . . . . . 18  |-  ( F  =  (/)  ->  ( F  o.  H )  =  (/) )
9695oveq1d 6101 . . . . . . . . . . . . . . . . 17  |-  ( F  =  (/)  ->  ( ( F  o.  H ) supp 
.0.  )  =  (
(/) supp  .0.  ) )
97 supp0 6690 . . . . . . . . . . . . . . . . . 18  |-  (  .0. 
e.  _V  ->  ( (/) supp  .0.  )  =  (/) )
9838, 97ax-mp 5 . . . . . . . . . . . . . . . . 17  |-  ( (/) supp  .0.  )  =  (/)
9996, 98syl6eq 2485 . . . . . . . . . . . . . . . 16  |-  ( F  =  (/)  ->  ( ( F  o.  H ) supp 
.0.  )  =  (/) )
10032, 99syl5eq 2481 . . . . . . . . . . . . . . 15  |-  ( F  =  (/)  ->  W  =  (/) )
10192, 100syl6bir 229 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( A  =  (/)  ->  W  =  (/) ) )
102101necon3d 2640 . . . . . . . . . . . . 13  |-  ( ph  ->  ( W  =/=  (/)  ->  A  =/=  (/) ) )
103102imp 429 . . . . . . . . . . . 12  |-  ( (
ph  /\  W  =/=  (/) )  ->  A  =/=  (/) )
104103adantr 465 . . . . . . . . . . 11  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  ->  A  =/=  (/) )
10585, 104eqnetrrd 2622 . . . . . . . . . 10  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  -> 
( m ... n
)  =/=  (/) )
106 fzn0 11456 . . . . . . . . . 10  |-  ( ( m ... n )  =/=  (/)  <->  n  e.  ( ZZ>=
`  m ) )
107105, 106sylib 196 . . . . . . . . 9  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  ->  n  e.  ( ZZ>= `  m ) )
1087ad2antrr 725 . . . . . . . . . 10  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  ->  F : A --> B )
10985feq2d 5540 . . . . . . . . . 10  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  -> 
( F : A --> B 
<->  F : ( m ... n ) --> B ) )
110108, 109mpbid 210 . . . . . . . . 9  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  ->  F : ( m ... n ) --> B )
11163, 66, 84, 107, 110gsumval2 15502 . . . . . . . 8  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  -> 
( G  gsumg  F )  =  (  seq m (  .+  ,  F ) `  n
) )
112 frn 5558 . . . . . . . . . . . . . . 15  |-  ( H : ( 1 ... M ) --> A  ->  ran  H  C_  A )
11310, 11, 1123syl 20 . . . . . . . . . . . . . 14  |-  ( ph  ->  ran  H  C_  A
)
114113ad2antrr 725 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  ->  ran  H  C_  A )
115114, 85sseqtrd 3385 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  ->  ran  H  C_  ( m ... n ) )
116 fzssuz 11491 . . . . . . . . . . . . 13  |-  ( m ... n )  C_  ( ZZ>= `  m )
117 uzssz 10872 . . . . . . . . . . . . . 14  |-  ( ZZ>= `  m )  C_  ZZ
118 zssre 10645 . . . . . . . . . . . . . 14  |-  ZZ  C_  RR
119117, 118sstri 3358 . . . . . . . . . . . . 13  |-  ( ZZ>= `  m )  C_  RR
120116, 119sstri 3358 . . . . . . . . . . . 12  |-  ( m ... n )  C_  RR
121115, 120syl6ss 3361 . . . . . . . . . . 11  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  ->  ran  H  C_  RR )
122 ltso 9447 . . . . . . . . . . 11  |-  <  Or  RR
123 soss 4651 . . . . . . . . . . 11  |-  ( ran 
H  C_  RR  ->  (  <  Or  RR  ->  < 
Or  ran  H )
)
124121, 122, 123mpisyl 18 . . . . . . . . . 10  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  ->  <  Or  ran  H )
125 fzfi 11786 . . . . . . . . . . . 12  |-  ( 1 ... M )  e. 
Fin
126125a1i 11 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 1 ... M
)  e.  Fin )
127 fex2 6527 . . . . . . . . . . . . . . 15  |-  ( ( H : ( 1 ... M ) --> A  /\  ( 1 ... M )  e.  Fin  /\  A  e.  V )  ->  H  e.  _V )
12812, 126, 2, 127syl3anc 1218 . . . . . . . . . . . . . 14  |-  ( ph  ->  H  e.  _V )
129 f1oen3g 7317 . . . . . . . . . . . . . 14  |-  ( ( H  e.  _V  /\  H : ( 1 ... M ) -1-1-onto-> ran  H )  -> 
( 1 ... M
)  ~~  ran  H )
130128, 15, 129syl2anc 661 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 1 ... M
)  ~~  ran  H )
131 enfi 7521 . . . . . . . . . . . . 13  |-  ( ( 1 ... M ) 
~~  ran  H  ->  ( ( 1 ... M
)  e.  Fin  <->  ran  H  e. 
Fin ) )
132130, 131syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( 1 ... M )  e.  Fin  <->  ran  H  e.  Fin ) )
133125, 132mpbii 211 . . . . . . . . . . 11  |-  ( ph  ->  ran  H  e.  Fin )
134133ad2antrr 725 . . . . . . . . . 10  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  ->  ran  H  e.  Fin )
135 fz1iso 12207 . . . . . . . . . 10  |-  ( (  <  Or  ran  H  /\  ran  H  e.  Fin )  ->  E. f  f  Isom  <  ,  <  ( ( 1 ... ( # `  ran  H ) ) ,  ran  H ) )
136124, 134, 135syl2anc 661 . . . . . . . . 9  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  ->  E. f  f  Isom  <  ,  <  ( ( 1 ... ( # `  ran  H ) ) ,  ran  H ) )
13770nnnn0d 10628 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  M  e.  NN0 )
138 hashfz1 12109 . . . . . . . . . . . . . . . 16  |-  ( M  e.  NN0  ->  ( # `  ( 1 ... M
) )  =  M )
139137, 138syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( # `  (
1 ... M ) )  =  M )
140 hashen 12110 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 1 ... M
)  e.  Fin  /\  ran  H  e.  Fin )  ->  ( ( # `  (
1 ... M ) )  =  ( # `  ran  H )  <->  ( 1 ... M )  ~~  ran  H ) )
141125, 133, 140sylancr 663 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( # `  (
1 ... M ) )  =  ( # `  ran  H )  <->  ( 1 ... M )  ~~  ran  H ) )
142130, 141mpbird 232 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( # `  (
1 ... M ) )  =  ( # `  ran  H ) )
143139, 142eqtr3d 2471 . . . . . . . . . . . . . 14  |-  ( ph  ->  M  =  ( # `  ran  H ) )
144143ad2antrr 725 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  M  =  ( # `  ran  H ) )
145144fveq2d 5688 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
(  seq 1 (  .+  ,  ( F  o.  f ) ) `  M )  =  (  seq 1 (  .+  ,  ( F  o.  f ) ) `  ( # `  ran  H
) ) )
1461ad2antrr 725 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  G  e.  Mnd )
14763, 66mndcl 15412 . . . . . . . . . . . . . . 15  |-  ( ( G  e.  Mnd  /\  x  e.  B  /\  y  e.  B )  ->  ( x  .+  y
)  e.  B )
1481473expb 1188 . . . . . . . . . . . . . 14  |-  ( ( G  e.  Mnd  /\  ( x  e.  B  /\  y  e.  B
) )  ->  (
x  .+  y )  e.  B )
149146, 148sylan 471 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  /\  ( x  e.  B  /\  y  e.  B
) )  ->  (
x  .+  y )  e.  B )
150 gsumval3.c . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ran  F  C_  ( Z `  ran  F ) )
151150ad2antrr 725 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  ran  F  C_  ( Z `  ran  F ) )
152151sselda 3349 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  /\  x  e.  ran  F )  ->  x  e.  ( Z `  ran  F
) )
153 gsumval3.z . . . . . . . . . . . . . . . 16  |-  Z  =  (Cntz `  G )
15466, 153cntzi 15836 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  ( Z `
 ran  F )  /\  y  e.  ran  F )  ->  ( x  .+  y )  =  ( y  .+  x ) )
155152, 154sylan 471 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  (
m ... n )  /\  f  Isom  <  ,  <  ( ( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  /\  x  e.  ran  F )  /\  y  e.  ran  F )  ->  ( x  .+  y )  =  ( y  .+  x ) )
156155anasss 647 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  /\  ( x  e.  ran  F  /\  y  e.  ran  F ) )  ->  (
x  .+  y )  =  ( y  .+  x ) )
15763, 66mndass 15413 . . . . . . . . . . . . . 14  |-  ( ( G  e.  Mnd  /\  ( x  e.  B  /\  y  e.  B  /\  z  e.  B
) )  ->  (
( x  .+  y
)  .+  z )  =  ( x  .+  ( y  .+  z
) ) )
158146, 157sylan 471 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  /\  ( x  e.  B  /\  y  e.  B  /\  z  e.  B
) )  ->  (
( x  .+  y
)  .+  z )  =  ( x  .+  ( y  .+  z
) ) )
15972ad2antrr 725 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  M  e.  ( ZZ>= ` 
1 ) )
1607ad2antrr 725 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  F : A --> B )
161 frn 5558 . . . . . . . . . . . . . 14  |-  ( F : A --> B  ->  ran  F  C_  B )
162160, 161syl 16 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  ran  F  C_  B )
163 simprr 756 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
f  Isom  <  ,  <  ( ( 1 ... ( # `
 ran  H )
) ,  ran  H
) )
164 isof1o 6009 . . . . . . . . . . . . . . . . 17  |-  ( f 
Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
)  ->  f :
( 1 ... ( # `
 ran  H )
)
-1-1-onto-> ran  H )
165163, 164syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
f : ( 1 ... ( # `  ran  H ) ) -1-1-onto-> ran  H )
166144oveq2d 6102 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
( 1 ... M
)  =  ( 1 ... ( # `  ran  H ) ) )
167 f1oeq2 5626 . . . . . . . . . . . . . . . . 17  |-  ( ( 1 ... M )  =  ( 1 ... ( # `  ran  H ) )  ->  (
f : ( 1 ... M ) -1-1-onto-> ran  H  <->  f : ( 1 ... ( # `  ran  H ) ) -1-1-onto-> ran  H ) )
168166, 167syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
( f : ( 1 ... M ) -1-1-onto-> ran 
H  <->  f : ( 1 ... ( # `  ran  H ) ) -1-1-onto-> ran 
H ) )
169165, 168mpbird 232 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
f : ( 1 ... M ) -1-1-onto-> ran  H
)
170 f1ocnv 5646 . . . . . . . . . . . . . . 15  |-  ( f : ( 1 ... M ) -1-1-onto-> ran  H  ->  `' f : ran  H -1-1-onto-> ( 1 ... M ) )
171169, 170syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  `' f : ran  H -1-1-onto-> ( 1 ... M ) )
17215ad2antrr 725 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  H : ( 1 ... M ) -1-1-onto-> ran  H )
173 f1oco 5656 . . . . . . . . . . . . . 14  |-  ( ( `' f : ran  H -1-1-onto-> ( 1 ... M )  /\  H : ( 1 ... M ) -1-1-onto-> ran 
H )  ->  ( `' f  o.  H
) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) )
174171, 172, 173syl2anc 661 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
( `' f  o.  H ) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) )
175 ffn 5552 . . . . . . . . . . . . . . . . 17  |-  ( F : A --> B  ->  F  Fn  A )
176 dffn4 5619 . . . . . . . . . . . . . . . . 17  |-  ( F  Fn  A  <->  F : A -onto-> ran  F )
177175, 176sylib 196 . . . . . . . . . . . . . . . 16  |-  ( F : A --> B  ->  F : A -onto-> ran  F
)
178 fof 5613 . . . . . . . . . . . . . . . 16  |-  ( F : A -onto-> ran  F  ->  F : A --> ran  F
)
179160, 177, 1783syl 20 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  F : A --> ran  F
)
180 f1of 5634 . . . . . . . . . . . . . . . . 17  |-  ( f : ( 1 ... M ) -1-1-onto-> ran  H  ->  f : ( 1 ... M ) --> ran  H
)
181169, 180syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
f : ( 1 ... M ) --> ran 
H )
182113ad2antrr 725 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  ran  H  C_  A )
183 fss 5560 . . . . . . . . . . . . . . . 16  |-  ( ( f : ( 1 ... M ) --> ran 
H  /\  ran  H  C_  A )  ->  f : ( 1 ... M ) --> A )
184181, 182, 183syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
f : ( 1 ... M ) --> A )
185 fco 5561 . . . . . . . . . . . . . . 15  |-  ( ( F : A --> ran  F  /\  f : ( 1 ... M ) --> A )  ->  ( F  o.  f ) : ( 1 ... M ) --> ran  F )
186179, 184, 185syl2anc 661 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
( F  o.  f
) : ( 1 ... M ) --> ran 
F )
187186ffvelrnda 5836 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  /\  x  e.  ( 1 ... M ) )  ->  ( ( F  o.  f ) `  x )  e.  ran  F )
188 f1ococnv2 5660 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( f : ( 1 ... M ) -1-1-onto-> ran  H  ->  (
f  o.  `' f )  =  (  _I  |`  ran  H ) )
189169, 188syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
( f  o.  `' f )  =  (  _I  |`  ran  H ) )
190189coeq1d 4993 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
( ( f  o.  `' f )  o.  H )  =  ( (  _I  |`  ran  H
)  o.  H ) )
191 f1of 5634 . . . . . . . . . . . . . . . . . . . . 21  |-  ( H : ( 1 ... M ) -1-1-onto-> ran  H  ->  H : ( 1 ... M ) --> ran  H
)
192 fcoi2 5579 . . . . . . . . . . . . . . . . . . . . 21  |-  ( H : ( 1 ... M ) --> ran  H  ->  ( (  _I  |`  ran  H
)  o.  H )  =  H )
193172, 191, 1923syl 20 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
( (  _I  |`  ran  H
)  o.  H )  =  H )
194190, 193eqtr2d 2470 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  H  =  ( (
f  o.  `' f )  o.  H ) )
195 coass 5349 . . . . . . . . . . . . . . . . . . 19  |-  ( ( f  o.  `' f )  o.  H )  =  ( f  o.  ( `' f  o.  H ) )
196194, 195syl6eq 2485 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  H  =  ( f  o.  ( `' f  o.  H ) ) )
197196coeq2d 4994 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
( F  o.  H
)  =  ( F  o.  ( f  o.  ( `' f  o.  H ) ) ) )
198 coass 5349 . . . . . . . . . . . . . . . . 17  |-  ( ( F  o.  f )  o.  ( `' f  o.  H ) )  =  ( F  o.  ( f  o.  ( `' f  o.  H
) ) )
199197, 198syl6eqr 2487 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
( F  o.  H
)  =  ( ( F  o.  f )  o.  ( `' f  o.  H ) ) )
200199fveq1d 5686 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
( ( F  o.  H ) `  k
)  =  ( ( ( F  o.  f
)  o.  ( `' f  o.  H ) ) `  k ) )
201200adantr 465 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  /\  k  e.  ( 1 ... M ) )  ->  ( ( F  o.  H ) `  k )  =  ( ( ( F  o.  f )  o.  ( `' f  o.  H
) ) `  k
) )
202 f1of 5634 . . . . . . . . . . . . . . . . 17  |-  ( `' f : ran  H -1-1-onto-> (
1 ... M )  ->  `' f : ran  H --> ( 1 ... M
) )
203169, 170, 2023syl 20 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  `' f : ran  H --> ( 1 ... M
) )
204172, 191syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  H : ( 1 ... M ) --> ran  H
)
205 fco 5561 . . . . . . . . . . . . . . . 16  |-  ( ( `' f : ran  H --> ( 1 ... M
)  /\  H :
( 1 ... M
) --> ran  H )  ->  ( `' f  o.  H ) : ( 1 ... M ) --> ( 1 ... M
) )
206203, 204, 205syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
( `' f  o.  H ) : ( 1 ... M ) --> ( 1 ... M
) )
207 fvco3 5761 . . . . . . . . . . . . . . 15  |-  ( ( ( `' f  o.  H ) : ( 1 ... M ) --> ( 1 ... M
)  /\  k  e.  ( 1 ... M
) )  ->  (
( ( F  o.  f )  o.  ( `' f  o.  H
) ) `  k
)  =  ( ( F  o.  f ) `
 ( ( `' f  o.  H ) `
 k ) ) )
208206, 207sylan 471 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  /\  k  e.  ( 1 ... M ) )  ->  ( ( ( F  o.  f )  o.  ( `' f  o.  H ) ) `
 k )  =  ( ( F  o.  f ) `  (
( `' f  o.  H ) `  k
) ) )
209201, 208eqtrd 2469 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  /\  k  e.  ( 1 ... M ) )  ->  ( ( F  o.  H ) `  k )  =  ( ( F  o.  f
) `  ( ( `' f  o.  H
) `  k )
) )
210149, 156, 158, 159, 162, 174, 187, 209seqf1o 11839 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
(  seq 1 (  .+  ,  ( F  o.  H ) ) `  M )  =  (  seq 1 (  .+  ,  ( F  o.  f ) ) `  M ) )
21163, 66, 3mndlid 15433 . . . . . . . . . . . . . 14  |-  ( ( G  e.  Mnd  /\  x  e.  B )  ->  (  .0.  .+  x
)  =  x )
212146, 211sylan 471 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  /\  x  e.  B )  ->  (  .0.  .+  x
)  =  x )
21363, 66, 3mndrid 15434 . . . . . . . . . . . . . 14  |-  ( ( G  e.  Mnd  /\  x  e.  B )  ->  ( x  .+  .0.  )  =  x )
214146, 213sylan 471 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  /\  x  e.  B )  ->  ( x  .+  .0.  )  =  x )
215146, 64syl 16 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  .0.  e.  B )
216 fdm 5556 . . . . . . . . . . . . . . . . 17  |-  ( H : ( 1 ... M ) --> A  ->  dom  H  =  ( 1 ... M ) )
21710, 11, 2163syl 20 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  dom  H  =  ( 1 ... M ) )
218 eluzfz1 11450 . . . . . . . . . . . . . . . . 17  |-  ( M  e.  ( ZZ>= `  1
)  ->  1  e.  ( 1 ... M
) )
219 ne0i 3636 . . . . . . . . . . . . . . . . 17  |-  ( 1  e.  ( 1 ... M )  ->  (
1 ... M )  =/=  (/) )
22072, 218, 2193syl 20 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( 1 ... M
)  =/=  (/) )
221217, 220eqnetrd 2620 . . . . . . . . . . . . . . 15  |-  ( ph  ->  dom  H  =/=  (/) )
222 dm0rn0 5048 . . . . . . . . . . . . . . . 16  |-  ( dom 
H  =  (/)  <->  ran  H  =  (/) )
223222necon3bii 2634 . . . . . . . . . . . . . . 15  |-  ( dom 
H  =/=  (/)  <->  ran  H  =/=  (/) )
224221, 223sylib 196 . . . . . . . . . . . . . 14  |-  ( ph  ->  ran  H  =/=  (/) )
225224ad2antrr 725 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  ran  H  =/=  (/) )
226115adantrr 716 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  ran  H  C_  ( m ... n ) )
227 simprl 755 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  A  =  ( m ... n ) )
228227eleq2d 2504 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
( x  e.  A  <->  x  e.  ( m ... n ) ) )
229228biimpar 485 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  /\  x  e.  ( m ... n ) )  ->  x  e.  A )
230160ffvelrnda 5836 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  /\  x  e.  A )  ->  ( F `  x
)  e.  B )
231229, 230syldan 470 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  /\  x  e.  ( m ... n ) )  -> 
( F `  x
)  e.  B )
232227difeq1d 3466 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
( A  \  ran  H )  =  ( ( m ... n ) 
\  ran  H )
)
233232eleq2d 2504 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
( x  e.  ( A  \  ran  H
)  <->  x  e.  (
( m ... n
)  \  ran  H ) ) )
234233biimpar 485 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  /\  x  e.  ( (
m ... n )  \  ran  H ) )  ->  x  e.  ( A  \  ran  H ) )
235 simpll 753 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  ph )
236235, 53sylan 471 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  /\  x  e.  ( A  \  ran  H ) )  ->  ( F `  x )  =  .0.  )
237234, 236syldan 470 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  /\  x  e.  ( (
m ... n )  \  ran  H ) )  -> 
( F `  x
)  =  .0.  )
238 f1of 5634 . . . . . . . . . . . . . . 15  |-  ( f : ( 1 ... ( # `  ran  H ) ) -1-1-onto-> ran  H  ->  f : ( 1 ... ( # `  ran  H ) ) --> ran  H
)
239163, 164, 2383syl 20 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
f : ( 1 ... ( # `  ran  H ) ) --> ran  H
)
240 fvco3 5761 . . . . . . . . . . . . . 14  |-  ( ( f : ( 1 ... ( # `  ran  H ) ) --> ran  H  /\  y  e.  (
1 ... ( # `  ran  H ) ) )  -> 
( ( F  o.  f ) `  y
)  =  ( F `
 ( f `  y ) ) )
241239, 240sylan 471 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  /\  y  e.  ( 1 ... ( # `  ran  H ) ) )  -> 
( ( F  o.  f ) `  y
)  =  ( F `
 ( f `  y ) ) )
242212, 214, 149, 215, 163, 225, 226, 231, 237, 241seqcoll2 12209 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
(  seq m (  .+  ,  F ) `  n
)  =  (  seq 1 (  .+  , 
( F  o.  f
) ) `  ( # `
 ran  H )
) )
243145, 210, 2423eqtr4d 2479 . . . . . . . . . . 11  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
(  seq 1 (  .+  ,  ( F  o.  H ) ) `  M )  =  (  seq m (  .+  ,  F ) `  n
) )
244243expr 615 . . . . . . . . . 10  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  -> 
( f  Isom  <  ,  <  ( ( 1 ... ( # `  ran  H ) ) ,  ran  H )  ->  (  seq 1 (  .+  , 
( F  o.  H
) ) `  M
)  =  (  seq m (  .+  ,  F ) `  n
) ) )
245244exlimdv 1690 . . . . . . . . 9  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  -> 
( E. f  f 
Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
)  ->  (  seq 1 (  .+  , 
( F  o.  H
) ) `  M
)  =  (  seq m (  .+  ,  F ) `  n
) ) )
246136, 245mpd 15 . . . . . . . 8  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  -> 
(  seq 1 (  .+  ,  ( F  o.  H ) ) `  M )  =  (  seq m (  .+  ,  F ) `  n
) )
247111, 246eqtr4d 2472 . . . . . . 7  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  -> 
( G  gsumg  F )  =  (  seq 1 (  .+  ,  ( F  o.  H ) ) `  M ) )
248247ex 434 . . . . . 6  |-  ( (
ph  /\  W  =/=  (/) )  ->  ( A  =  ( m ... n )  ->  ( G  gsumg  F )  =  (  seq 1 (  .+  ,  ( F  o.  H ) ) `  M ) ) )
249248rexlimdvw 2838 . . . . 5  |-  ( (
ph  /\  W  =/=  (/) )  ->  ( E. n  e.  ZZ  A  =  ( m ... n )  ->  ( G  gsumg  F )  =  (  seq 1 (  .+  ,  ( F  o.  H ) ) `  M ) ) )
250249rexlimdvw 2838 . . . 4  |-  ( (
ph  /\  W  =/=  (/) )  ->  ( E. m  e.  ZZ  E. n  e.  ZZ  A  =  ( m ... n )  ->  ( G  gsumg  F )  =  (  seq 1
(  .+  ,  ( F  o.  H )
) `  M )
) )
25183, 250syl5bi 217 . . 3  |-  ( (
ph  /\  W  =/=  (/) )  ->  ( A  e.  ran  ...  ->  ( G 
gsumg  F )  =  (  seq 1 (  .+  ,  ( F  o.  H ) ) `  M ) ) )
252 suppssdm 6698 . . . . . . . . . . 11  |-  ( ( F  o.  H ) supp 
.0.  )  C_  dom  ( F  o.  H
)
25332, 252eqsstri 3379 . . . . . . . . . 10  |-  W  C_  dom  ( F  o.  H
)
254 fdm 5556 . . . . . . . . . . 11  |-  ( ( F  o.  H ) : ( 1 ... M ) --> B  ->  dom  ( F  o.  H
)  =  ( 1 ... M ) )
25530, 254syl 16 . . . . . . . . . 10  |-  ( ph  ->  dom  ( F  o.  H )  =  ( 1 ... M ) )
256253, 255syl5sseq 3397 . . . . . . . . 9  |-  ( ph  ->  W  C_  ( 1 ... M ) )
257 fzssuz 11491 . . . . . . . . . . 11  |-  ( 1 ... M )  C_  ( ZZ>= `  1 )
258257, 71sseqtr4i 3382 . . . . . . . . . 10  |-  ( 1 ... M )  C_  NN
259 nnssre 10318 . . . . . . . . . 10  |-  NN  C_  RR
260258, 259sstri 3358 . . . . . . . . 9  |-  ( 1 ... M )  C_  RR
261256, 260syl6ss 3361 . . . . . . . 8  |-  ( ph  ->  W  C_  RR )
262 soss 4651 . . . . . . . 8  |-  ( W 
C_  RR  ->  (  < 
Or  RR  ->  <  Or  W ) )
263261, 122, 262mpisyl 18 . . . . . . 7  |-  ( ph  ->  <  Or  W )
264 ssfi 7525 . . . . . . . 8  |-  ( ( ( 1 ... M
)  e.  Fin  /\  W  C_  ( 1 ... M ) )  ->  W  e.  Fin )
265125, 256, 264sylancr 663 . . . . . . 7  |-  ( ph  ->  W  e.  Fin )
266 fz1iso 12207 . . . . . . 7  |-  ( (  <  Or  W  /\  W  e.  Fin )  ->  E. f  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) )
267263, 265, 266syl2anc 661 . . . . . 6  |-  ( ph  ->  E. f  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) )
268267ad2antrr 725 . . . . 5  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  -.  A  e.  ran  ... )  ->  E. f  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) )
26963, 3, 66, 153, 1, 2, 7, 150, 70, 10, 51, 32gsumval3lem2 16373 . . . . . . . 8  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( G  gsumg  F )  =  (  seq 1 (  .+  ,  ( F  o.  ( H  o.  f
) ) ) `  ( # `  W ) ) )
2701ad2antrr 725 . . . . . . . . . 10  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  ->  G  e.  Mnd )
271270, 211sylan 471 . . . . . . . . 9  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  /\  x  e.  B )  ->  (  .0.  .+  x
)  =  x )
272270, 213sylan 471 . . . . . . . . 9  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  /\  x  e.  B )  ->  ( x  .+  .0.  )  =  x )
273270, 148sylan 471 . . . . . . . . 9  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  /\  ( x  e.  B  /\  y  e.  B
) )  ->  (
x  .+  y )  e.  B )
274270, 64syl 16 . . . . . . . . 9  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  ->  .0.  e.  B )
275 simprr 756 . . . . . . . . 9  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
f  Isom  <  ,  <  ( ( 1 ... ( # `
 W ) ) ,  W ) )
276 simplr 754 . . . . . . . . 9  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  ->  W  =/=  (/) )
277256ad2antrr 725 . . . . . . . . 9  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  ->  W  C_  ( 1 ... M ) )
27830ad2antrr 725 . . . . . . . . . 10  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( F  o.  H
) : ( 1 ... M ) --> B )
279278ffvelrnda 5836 . . . . . . . . 9  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  /\  x  e.  ( 1 ... M ) )  ->  ( ( F  o.  H ) `  x )  e.  B
)
28033a1i 11 . . . . . . . . . 10  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( ( F  o.  H ) supp  .0.  )  C_  W )
28135a1i 11 . . . . . . . . . 10  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( 1 ... M
)  e.  _V )
28238a1i 11 . . . . . . . . . 10  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  ->  .0.  e.  _V )
283278, 280, 281, 282suppssr 6715 . . . . . . . . 9  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  /\  x  e.  ( (
1 ... M )  \  W ) )  -> 
( ( F  o.  H ) `  x
)  =  .0.  )
284 coass 5349 . . . . . . . . . . 11  |-  ( ( F  o.  H )  o.  f )  =  ( F  o.  ( H  o.  f )
)
285284fveq1i 5685 . . . . . . . . . 10  |-  ( ( ( F  o.  H
)  o.  f ) `
 y )  =  ( ( F  o.  ( H  o.  f
) ) `  y
)
286 isof1o 6009 . . . . . . . . . . . 12  |-  ( f 
Isom  <  ,  <  (
( 1 ... ( # `
 W ) ) ,  W )  -> 
f : ( 1 ... ( # `  W
) ) -1-1-onto-> W )
287 f1of 5634 . . . . . . . . . . . 12  |-  ( f : ( 1 ... ( # `  W
) ) -1-1-onto-> W  ->  f :
( 1 ... ( # `
 W ) ) --> W )
288275, 286, 2873syl 20 . . . . . . . . . . 11  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
f : ( 1 ... ( # `  W
) ) --> W )
289 fvco3 5761 . . . . . . . . . . 11  |-  ( ( f : ( 1 ... ( # `  W
) ) --> W  /\  y  e.  ( 1 ... ( # `  W
) ) )  -> 
( ( ( F  o.  H )  o.  f ) `  y
)  =  ( ( F  o.  H ) `
 ( f `  y ) ) )
290288, 289sylan 471 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  /\  y  e.  ( 1 ... ( # `  W
) ) )  -> 
( ( ( F  o.  H )  o.  f ) `  y
)  =  ( ( F  o.  H ) `
 ( f `  y ) ) )
291285, 290syl5eqr 2483 . . . . . . . . 9  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  /\  y  e.  ( 1 ... ( # `  W
) ) )  -> 
( ( F  o.  ( H  o.  f
) ) `  y
)  =  ( ( F  o.  H ) `
 ( f `  y ) ) )
292271, 272, 273, 274, 275, 276, 277, 279, 283, 291seqcoll2 12209 . . . . . . . 8  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
(  seq 1 (  .+  ,  ( F  o.  H ) ) `  M )  =  (  seq 1 (  .+  ,  ( F  o.  ( H  o.  f
) ) ) `  ( # `  W ) ) )
293269, 292eqtr4d 2472 . . . . . . 7  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  -> 
( G  gsumg  F )  =  (  seq 1 (  .+  ,  ( F  o.  H ) ) `  M ) )
294293expr 615 . . . . . 6  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  -.  A  e.  ran  ... )  ->  ( f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
)  ->  ( G  gsumg  F )  =  (  seq 1 (  .+  , 
( F  o.  H
) ) `  M
) ) )
295294exlimdv 1690 . . . . 5  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  -.  A  e.  ran  ... )  ->  ( E. f  f 
Isom  <  ,  <  (
( 1 ... ( # `
 W ) ) ,  W )  -> 
( G  gsumg  F )  =  (  seq 1 (  .+  ,  ( F  o.  H ) ) `  M ) ) )
296268, 295mpd 15 . . . 4  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  -.  A  e.  ran  ... )  ->  ( G  gsumg  F )  =  (  seq 1 (  .+  ,  ( F  o.  H ) ) `  M ) )
297296ex 434 . . 3  |-  ( (
ph  /\  W  =/=  (/) )  ->  ( -.  A  e.  ran  ...  ->  ( G  gsumg  F )  =  (  seq 1 (  .+  ,  ( F  o.  H ) ) `  M ) ) )
298251, 297pm2.61d 158 . 2  |-  ( (
ph  /\  W  =/=  (/) )  ->  ( G  gsumg  F )  =  (  seq 1 (  .+  , 
( F  o.  H
) ) `  M
) )
29979, 298pm2.61dane 2683 1  |-  ( ph  ->  ( G  gsumg  F )  =  (  seq 1 (  .+  ,  ( F  o.  H ) ) `  M ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 965    = wceq 1369   E.wex 1586    e. wcel 1756    =/= wne 2600   E.wrex 2710   _Vcvv 2966    \ cdif 3318    C_ wss 3321   (/)c0 3630   ~Pcpw 3853   {csn 3870   class class class wbr 4285    e. cmpt 4343    _I cid 4623    Or wor 4632    X. cxp 4830   `'ccnv 4831   dom cdm 4832   ran crn 4833    |` cres 4834    o. ccom 4836   Rel wrel 4837    Fn wfn 5406   -->wf 5407   -1-1->wf1 5408   -onto->wfo 5409   -1-1-onto->wf1o 5410   ` cfv 5411    Isom wiso 5412  (class class class)co 6086   supp csupp 6685    ~~ cen 7299   Fincfn 7302   RRcr 9273   1c1 9275    < clt 9410   NNcn 10314   NN0cn0 10571   ZZcz 10638   ZZ>=cuz 10853   ...cfz 11429    seqcseq 11798   #chash 12095   Basecbs 14166   +g cplusg 14230   0gc0g 14370    gsumg cgsu 14371   Mndcmnd 15401  Cntzccntz 15822
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2418  ax-rep 4396  ax-sep 4406  ax-nul 4414  ax-pow 4463  ax-pr 4524  ax-un 6367  ax-cnex 9330  ax-resscn 9331  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-mulcom 9338  ax-addass 9339  ax-mulass 9340  ax-distr 9341  ax-i2m1 9342  ax-1ne0 9343  ax-1rid 9344  ax-rnegex 9345  ax-rrecex 9346  ax-cnre 9347  ax-pre-lttri 9348  ax-pre-lttrn 9349  ax-pre-ltadd 9350  ax-pre-mulgt0 9351
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-nel 2603  df-ral 2714  df-rex 2715  df-reu 2716  df-rmo 2717  df-rab 2718  df-v 2968  df-sbc 3180  df-csb 3282  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-pss 3337  df-nul 3631  df-if 3785  df-pw 3855  df-sn 3871  df-pr 3873  df-tp 3875  df-op 3877  df-uni 4085  df-int 4122  df-iun 4166  df-br 4286  df-opab 4344  df-mpt 4345  df-tr 4379  df-eprel 4624  df-id 4628  df-po 4633  df-so 4634  df-fr 4671  df-se 4672  df-we 4673  df-ord 4714  df-on 4715  df-lim 4716  df-suc 4717  df-xp 4838  df-rel 4839  df-cnv 4840  df-co 4841  df-dm 4842  df-rn 4843  df-res 4844  df-ima 4845  df-iota 5374  df-fun 5413  df-fn 5414  df-f 5415  df-f1 5416  df-fo 5417  df-f1o 5418  df-fv 5419  df-isom 5420  df-riota 6045  df-ov 6089  df-oprab 6090  df-mpt2 6091  df-om 6472  df-1st 6572  df-2nd 6573  df-supp 6686  df-recs 6824  df-rdg 6858  df-1o 6912  df-oadd 6916  df-er 7093  df-en 7303  df-dom 7304  df-sdom 7305  df-fin 7306  df-oi 7716  df-card 8101  df-pnf 9412  df-mnf 9413  df-xr 9414  df-ltxr 9415  df-le 9416  df-sub 9589  df-neg 9590  df-nn 10315  df-n0 10572  df-z 10639  df-uz 10854  df-fz 11430  df-fzo 11541  df-seq 11799  df-hash 12096  df-0g 14372  df-gsum 14373  df-mnd 15407  df-cntz 15824
This theorem is referenced by:  gsumzres  16377  gsumzcl2  16378  gsumzf1o  16380  gsumzaddlem  16397  gsumconst  16415  gsumzmhm  16418  gsumzoppg  16428  gsumfsum  17848  wilthlem3  22377
  Copyright terms: Public domain W3C validator