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

Theorem gsumval3 16388
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 15514 . . . . 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 5747 . . . . . 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 5609 . . . . . . . . . . . . . 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 5655 . . . . . . . . . . . . . . . 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 5656 . . . . . . . . . . . . . 14  |-  ( H : ( 1 ... M ) -1-1-onto-> ran  H  ->  `' H : ran  H -1-1-onto-> ( 1 ... M ) )
18 f1of 5644 . . . . . . . . . . . . . 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 5846 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ran  H )  -> 
( `' H `  x )  e.  ( 1 ... M ) )
21 fvco3 5771 . . . . . . . . . . . 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 3477 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  W  =  (/) )  ->  ( (
1 ... M )  \  W )  =  ( ( 1 ... M
)  \  (/) ) )
25 dif0 3752 . . . . . . . . . . . . . . 15  |-  ( ( 1 ... M ) 
\  (/) )  =  ( 1 ... M )
2624, 25syl6eq 2491 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  W  =  (/) )  ->  ( (
1 ... M )  \  W )  =  ( 1 ... M ) )
2726adantr 465 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ran  H )  -> 
( ( 1 ... M )  \  W
)  =  ( 1 ... M ) )
2820, 27eleqtrrd 2520 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ran  H )  -> 
( `' H `  x )  e.  ( ( 1 ... M
)  \  W )
)
29 fco 5571 . . . . . . . . . . . . . . 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 3414 . . . . . . . . . . . . . 14  |-  ( ( F  o.  H ) supp 
.0.  )  C_  W
3433a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  W  =  (/) )  ->  ( ( F  o.  H ) supp  .0.  )  C_  W )
35 ovex 6119 . . . . . . . . . . . . . 14  |-  ( 1 ... M )  e. 
_V
3635a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  W  =  (/) )  ->  ( 1 ... M )  e. 
_V )
37 fvex 5704 . . . . . . . . . . . . . . 15  |-  ( 0g
`  G )  e. 
_V
383, 37eqeltri 2513 . . . . . . . . . . . . . 14  |-  .0.  e.  _V
3938a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  W  =  (/) )  ->  .0.  e.  _V )
4031, 34, 36, 39suppssr 6723 . . . . . . . . . . . 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 5987 . . . . . . . . . . . . 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 5698 . . . . . . . . . . 11  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ran  H )  -> 
( F `  ( H `  ( `' H `  x )
) )  =  ( F `  x ) )
4522, 41, 443eqtr3rd 2484 . . . . . . . . . 10  |-  ( ( ( ph  /\  W  =  (/) )  /\  x  e.  ran  H )  -> 
( F `  x
)  =  .0.  )
46 fvex 5704 . . . . . . . . . . 11  |-  ( F `
 x )  e. 
_V
4746elsnc 3904 . . . . . . . . . 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 3341 . . . . . . . . . . 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 6723 . . . . . . . . . . . 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 4381 . . . . 5  |-  ( (
ph  /\  W  =  (/) )  ->  ( x  e.  A  |->  ( F `
 x ) )  =  ( x  e.  A  |->  .0.  ) )
619, 60eqtrd 2475 . . . 4  |-  ( (
ph  /\  W  =  (/) )  ->  F  =  ( x  e.  A  |->  .0.  ) )
6261oveq2d 6110 . . 3  |-  ( (
ph  /\  W  =  (/) )  ->  ( G  gsumg  F )  =  ( G 
gsumg  ( x  e.  A  |->  .0.  ) ) )
63 gsumval3.b . . . . . . . 8  |-  B  =  ( Base `  G
)
6463, 3mndidcl 15442 . . . . . . 7  |-  ( G  e.  Mnd  ->  .0.  e.  B )
651, 64syl 16 . . . . . 6  |-  ( ph  ->  .0.  e.  B )
66 gsumval3.p . . . . . . 7  |-  .+  =  ( +g  `  G )
6763, 66, 3mndlid 15444 . . . . . 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 10899 . . . . . 6  |-  NN  =  ( ZZ>= `  1 )
7270, 71syl6eleq 2533 . . . . 5  |-  ( ph  ->  M  e.  ( ZZ>= ` 
1 ) )
7372adantr 465 . . . 4  |-  ( (
ph  /\  W  =  (/) )  ->  M  e.  ( ZZ>= `  1 )
)
7426eleq2d 2510 . . . . . 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 6723 . . . . 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 11853 . . 3  |-  ( (
ph  /\  W  =  (/) )  ->  (  seq 1 (  .+  , 
( F  o.  H
) ) `  M
)  =  .0.  )
796, 62, 783eqtr4d 2485 . 2  |-  ( (
ph  /\  W  =  (/) )  ->  ( G  gsumg  F )  =  (  seq 1 (  .+  , 
( F  o.  H
) ) `  M
) )
80 fzf 11444 . . . . 5  |-  ... :
( ZZ  X.  ZZ )
--> ~P ZZ
81 ffn 5562 . . . . 5  |-  ( ...
: ( ZZ  X.  ZZ ) --> ~P ZZ  ->  ... 
Fn  ( ZZ  X.  ZZ ) )
82 ovelrn 6242 . . . . 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 5565 . . . . . . . . . . . . . . . . 17  |-  ( F : A --> B  ->  Rel  F )
87 reldm0 5060 . . . . . . . . . . . . . . . . 17  |-  ( Rel 
F  ->  ( F  =  (/)  <->  dom  F  =  (/) ) )
887, 86, 873syl 20 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( F  =  (/)  <->  dom  F  =  (/) ) )
89 fdm 5566 . . . . . . . . . . . . . . . . . 18  |-  ( F : A --> B  ->  dom  F  =  A )
907, 89syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  dom  F  =  A )
9190eqeq1d 2451 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( dom  F  =  (/) 
<->  A  =  (/) ) )
9288, 91bitrd 253 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( F  =  (/)  <->  A  =  (/) ) )
93 coeq1 5000 . . . . . . . . . . . . . . . . . . 19  |-  ( F  =  (/)  ->  ( F  o.  H )  =  ( (/)  o.  H
) )
94 co01 5355 . . . . . . . . . . . . . . . . . . 19  |-  ( (/)  o.  H )  =  (/)
9593, 94syl6eq 2491 . . . . . . . . . . . . . . . . . 18  |-  ( F  =  (/)  ->  ( F  o.  H )  =  (/) )
9695oveq1d 6109 . . . . . . . . . . . . . . . . 17  |-  ( F  =  (/)  ->  ( ( F  o.  H ) supp 
.0.  )  =  (
(/) supp  .0.  ) )
97 supp0 6698 . . . . . . . . . . . . . . . . . 18  |-  (  .0. 
e.  _V  ->  ( (/) supp  .0.  )  =  (/) )
9838, 97ax-mp 5 . . . . . . . . . . . . . . . . 17  |-  ( (/) supp  .0.  )  =  (/)
9996, 98syl6eq 2491 . . . . . . . . . . . . . . . 16  |-  ( F  =  (/)  ->  ( ( F  o.  H ) supp 
.0.  )  =  (/) )
10032, 99syl5eq 2487 . . . . . . . . . . . . . . 15  |-  ( F  =  (/)  ->  W  =  (/) )
10192, 100syl6bir 229 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( A  =  (/)  ->  W  =  (/) ) )
102101necon3d 2649 . . . . . . . . . . . . 13  |-  ( ph  ->  ( W  =/=  (/)  ->  A  =/=  (/) ) )
103102imp 429 . . . . . . . . . . . 12  |-  ( (
ph  /\  W  =/=  (/) )  ->  A  =/=  (/) )
104103adantr 465 . . . . . . . . . . 11  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  ->  A  =/=  (/) )
10585, 104eqnetrrd 2631 . . . . . . . . . 10  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  -> 
( m ... n
)  =/=  (/) )
106 fzn0 11467 . . . . . . . . . 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 5550 . . . . . . . . . 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 15516 . . . . . . . 8  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  -> 
( G  gsumg  F )  =  (  seq m (  .+  ,  F ) `  n
) )
112 frn 5568 . . . . . . . . . . . . . . 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 3395 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  ->  ran  H  C_  ( m ... n ) )
116 fzssuz 11502 . . . . . . . . . . . . 13  |-  ( m ... n )  C_  ( ZZ>= `  m )
117 uzssz 10883 . . . . . . . . . . . . . 14  |-  ( ZZ>= `  m )  C_  ZZ
118 zssre 10656 . . . . . . . . . . . . . 14  |-  ZZ  C_  RR
119117, 118sstri 3368 . . . . . . . . . . . . 13  |-  ( ZZ>= `  m )  C_  RR
120116, 119sstri 3368 . . . . . . . . . . . 12  |-  ( m ... n )  C_  RR
121115, 120syl6ss 3371 . . . . . . . . . . 11  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  A  =  ( m ... n ) )  ->  ran  H  C_  RR )
122 ltso 9458 . . . . . . . . . . 11  |-  <  Or  RR
123 soss 4662 . . . . . . . . . . 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 11797 . . . . . . . . . . . 12  |-  ( 1 ... M )  e. 
Fin
126125a1i 11 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 1 ... M
)  e.  Fin )
127 fex2 6535 . . . . . . . . . . . . . . 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 7328 . . . . . . . . . . . . . 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 7532 . . . . . . . . . . . . 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 12218 . . . . . . . . . 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 10639 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  M  e.  NN0 )
138 hashfz1 12120 . . . . . . . . . . . . . . . 16  |-  ( M  e.  NN0  ->  ( # `  ( 1 ... M
) )  =  M )
139137, 138syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( # `  (
1 ... M ) )  =  M )
140 hashen 12121 . . . . . . . . . . . . . . . . 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 2477 . . . . . . . . . . . . . 14  |-  ( ph  ->  M  =  ( # `  ran  H ) )
144143ad2antrr 725 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  M  =  ( # `  ran  H ) )
145144fveq2d 5698 . . . . . . . . . . . 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 15423 . . . . . . . . . . . . . . 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 3359 . . . . . . . . . . . . . . 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 15850 . . . . . . . . . . . . . . 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 15424 . . . . . . . . . . . . . 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 5568 . . . . . . . . . . . . . 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 6019 . . . . . . . . . . . . . . . . 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 6110 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
( 1 ... M
)  =  ( 1 ... ( # `  ran  H ) ) )
167 f1oeq2 5636 . . . . . . . . . . . . . . . . 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 5656 . . . . . . . . . . . . . . 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 5666 . . . . . . . . . . . . . 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 5562 . . . . . . . . . . . . . . . . 17  |-  ( F : A --> B  ->  F  Fn  A )
176 dffn4 5629 . . . . . . . . . . . . . . . . 17  |-  ( F  Fn  A  <->  F : A -onto-> ran  F )
177175, 176sylib 196 . . . . . . . . . . . . . . . 16  |-  ( F : A --> B  ->  F : A -onto-> ran  F
)
178 fof 5623 . . . . . . . . . . . . . . . 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 5644 . . . . . . . . . . . . . . . . 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 5570 . . . . . . . . . . . . . . . 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 5571 . . . . . . . . . . . . . . 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 5846 . . . . . . . . . . . . 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 5670 . . . . . . . . . . . . . . . . . . . . . 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 5004 . . . . . . . . . . . . . . . . . . . 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 5644 . . . . . . . . . . . . . . . . . . . . 21  |-  ( H : ( 1 ... M ) -1-1-onto-> ran  H  ->  H : ( 1 ... M ) --> ran  H
)
192 fcoi2 5589 . . . . . . . . . . . . . . . . . . . . 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 2476 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  H  =  ( (
f  o.  `' f )  o.  H ) )
195 coass 5359 . . . . . . . . . . . . . . . . . . 19  |-  ( ( f  o.  `' f )  o.  H )  =  ( f  o.  ( `' f  o.  H ) )
196194, 195syl6eq 2491 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  ->  H  =  ( f  o.  ( `' f  o.  H ) ) )
197196coeq2d 5005 . . . . . . . . . . . . . . . . 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 5359 . . . . . . . . . . . . . . . . 17  |-  ( ( F  o.  f )  o.  ( `' f  o.  H ) )  =  ( F  o.  ( f  o.  ( `' f  o.  H
) ) )
199197, 198syl6eqr 2493 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
( F  o.  H
)  =  ( ( F  o.  f )  o.  ( `' f  o.  H ) ) )
200199fveq1d 5696 . . . . . . . . . . . . . . 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 5644 . . . . . . . . . . . . . . . . 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 5571 . . . . . . . . . . . . . . . 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 5771 . . . . . . . . . . . . . . 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 2475 . . . . . . . . . . . . 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 11850 . . . . . . . . . . . 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 15444 . . . . . . . . . . . . . 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 15445 . . . . . . . . . . . . . 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 5566 . . . . . . . . . . . . . . . . 17  |-  ( H : ( 1 ... M ) --> A  ->  dom  H  =  ( 1 ... M ) )
21710, 11, 2163syl 20 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  dom  H  =  ( 1 ... M ) )
218 eluzfz1 11461 . . . . . . . . . . . . . . . . 17  |-  ( M  e.  ( ZZ>= `  1
)  ->  1  e.  ( 1 ... M
) )
219 ne0i 3646 . . . . . . . . . . . . . . . . 17  |-  ( 1  e.  ( 1 ... M )  ->  (
1 ... M )  =/=  (/) )
22072, 218, 2193syl 20 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( 1 ... M
)  =/=  (/) )
221217, 220eqnetrd 2629 . . . . . . . . . . . . . . 15  |-  ( ph  ->  dom  H  =/=  (/) )
222 dm0rn0 5059 . . . . . . . . . . . . . . . 16  |-  ( dom 
H  =  (/)  <->  ran  H  =  (/) )
223222necon3bii 2643 . . . . . . . . . . . . . . 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 2510 . . . . . . . . . . . . . . 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 5846 . . . . . . . . . . . . . 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 3476 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  W  =/=  (/) )  /\  ( A  =  ( m ... n )  /\  f  Isom  <  ,  <  (
( 1 ... ( # `
 ran  H )
) ,  ran  H
) ) )  -> 
( A  \  ran  H )  =  ( ( m ... n ) 
\  ran  H )
)
233232eleq2d 2510 . . . . . . . . . . . . . . 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 5644 . . . . . . . . . . . . . . 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 5771 . . . . . . . . . . . . . 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 12220 . . . . . . . . . . . 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 2485 . . . . . . . . . . 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 2478 . . . . . . 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 2847 . . . . 5  |-  ( (
ph  /\  W  =/=  (/) )  ->  ( E. n  e.  ZZ  A  =  ( m ... n )  ->  ( G  gsumg  F )  =  (  seq 1 (  .+  ,  ( F  o.  H ) ) `  M ) ) )
250249rexlimdvw 2847 . . . 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 6706 . . . . . . . . . . 11  |-  ( ( F  o.  H ) supp 
.0.  )  C_  dom  ( F  o.  H
)
25332, 252eqsstri 3389 . . . . . . . . . 10  |-  W  C_  dom  ( F  o.  H
)
254 fdm 5566 . . . . . . . . . . 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 3407 . . . . . . . . 9  |-  ( ph  ->  W  C_  ( 1 ... M ) )
257 fzssuz 11502 . . . . . . . . . . 11  |-  ( 1 ... M )  C_  ( ZZ>= `  1 )
258257, 71sseqtr4i 3392 . . . . . . . . . 10  |-  ( 1 ... M )  C_  NN
259 nnssre 10329 . . . . . . . . . 10  |-  NN  C_  RR
260258, 259sstri 3368 . . . . . . . . 9  |-  ( 1 ... M )  C_  RR
261256, 260syl6ss 3371 . . . . . . . 8  |-  ( ph  ->  W  C_  RR )
262 soss 4662 . . . . . . . 8  |-  ( W 
C_  RR  ->  (  < 
Or  RR  ->  <  Or  W ) )
263261, 122, 262mpisyl 18 . . . . . . 7  |-  ( ph  ->  <  Or  W )
264 ssfi 7536 . . . . . . . 8  |-  ( ( ( 1 ... M
)  e.  Fin  /\  W  C_  ( 1 ... M ) )  ->  W  e.  Fin )
265125, 256, 264sylancr 663 . . . . . . 7  |-  ( ph  ->  W  e.  Fin )
266 fz1iso 12218 . . . . . . 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 16387 . . . . . . . 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 5846 . . . . . . . . 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 6723 . . . . . . . . 9  |-  ( ( ( ( ph  /\  W  =/=  (/) )  /\  ( -.  A  e.  ran  ... 
/\  f  Isom  <  ,  <  ( ( 1 ... ( # `  W
) ) ,  W
) ) )  /\  x  e.  ( (
1 ... M )  \  W ) )  -> 
( ( F  o.  H ) `  x
)  =  .0.  )
284 coass 5359 . . . . . . . . . . 11  |-  ( ( F  o.  H )  o.  f )  =  ( F  o.  ( H  o.  f )
)
285284fveq1i 5695 . . . . . . . . . 10  |-  ( ( ( F  o.  H
)  o.  f ) `
 y )  =  ( ( F  o.  ( H  o.  f
) ) `  y
)
286 isof1o 6019 . . . . . . . . . . . 12  |-  ( f 
Isom  <  ,  <  (
( 1 ... ( # `
 W ) ) ,  W )  -> 
f : ( 1 ... ( # `  W
) ) -1-1-onto-> W )
287 f1of 5644 . . . . . . . . . . . 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 5771 . . . . . . . . . . 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 2489 . . . . . . . . 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 12220 . . . . . . . 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 2478 . . . . . . 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 2692 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 2609   E.wrex 2719   _Vcvv 2975    \ cdif 3328    C_ wss 3331   (/)c0 3640   ~Pcpw 3863   {csn 3880   class class class wbr 4295    e. cmpt 4353    _I cid 4634    Or wor 4643    X. cxp 4841   `'ccnv 4842   dom cdm 4843   ran crn 4844    |` cres 4845    o. ccom 4847   Rel wrel 4848    Fn wfn 5416   -->wf 5417   -1-1->wf1 5418   -onto->wfo 5419   -1-1-onto->wf1o 5420   ` cfv 5421    Isom wiso 5422  (class class class)co 6094   supp csupp 6693    ~~ cen 7310   Fincfn 7313   RRcr 9284   1c1 9286    < clt 9421   NNcn 10325   NN0cn0 10582   ZZcz 10649   ZZ>=cuz 10864   ...cfz 11440    seqcseq 11809   #chash 12106   Basecbs 14177   +g cplusg 14241   0gc0g 14381    gsumg cgsu 14382   Mndcmnd 15412  Cntzccntz 15836
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 2423  ax-rep 4406  ax-sep 4416  ax-nul 4424  ax-pow 4473  ax-pr 4534  ax-un 6375  ax-cnex 9341  ax-resscn 9342  ax-1cn 9343  ax-icn 9344  ax-addcl 9345  ax-addrcl 9346  ax-mulcl 9347  ax-mulrcl 9348  ax-mulcom 9349  ax-addass 9350  ax-mulass 9351  ax-distr 9352  ax-i2m1 9353  ax-1ne0 9354  ax-1rid 9355  ax-rnegex 9356  ax-rrecex 9357  ax-cnre 9358  ax-pre-lttri 9359  ax-pre-lttrn 9360  ax-pre-ltadd 9361  ax-pre-mulgt0 9362
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 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-ne 2611  df-nel 2612  df-ral 2723  df-rex 2724  df-reu 2725  df-rmo 2726  df-rab 2727  df-v 2977  df-sbc 3190  df-csb 3292  df-dif 3334  df-un 3336  df-in 3338  df-ss 3345  df-pss 3347  df-nul 3641  df-if 3795  df-pw 3865  df-sn 3881  df-pr 3883  df-tp 3885  df-op 3887  df-uni 4095  df-int 4132  df-iun 4176  df-br 4296  df-opab 4354  df-mpt 4355  df-tr 4389  df-eprel 4635  df-id 4639  df-po 4644  df-so 4645  df-fr 4682  df-se 4683  df-we 4684  df-ord 4725  df-on 4726  df-lim 4727  df-suc 4728  df-xp 4849  df-rel 4850  df-cnv 4851  df-co 4852  df-dm 4853  df-rn 4854  df-res 4855  df-ima 4856  df-iota 5384  df-fun 5423  df-fn 5424  df-f 5425  df-f1 5426  df-fo 5427  df-f1o 5428  df-fv 5429  df-isom 5430  df-riota 6055  df-ov 6097  df-oprab 6098  df-mpt2 6099  df-om 6480  df-1st 6580  df-2nd 6581  df-supp 6694  df-recs 6835  df-rdg 6869  df-1o 6923  df-oadd 6927  df-er 7104  df-en 7314  df-dom 7315  df-sdom 7316  df-fin 7317  df-oi 7727  df-card 8112  df-pnf 9423  df-mnf 9424  df-xr 9425  df-ltxr 9426  df-le 9427  df-sub 9600  df-neg 9601  df-nn 10326  df-n0 10583  df-z 10650  df-uz 10865  df-fz 11441  df-fzo 11552  df-seq 11810  df-hash 12107  df-0g 14383  df-gsum 14384  df-mnd 15418  df-cntz 15838
This theorem is referenced by:  gsumzres  16391  gsumzcl2  16392  gsumzf1o  16394  gsumzaddlem  16411  gsumconst  16430  gsumzmhm  16433  gsumzoppg  16443  gsumfsum  17882  wilthlem3  22411
  Copyright terms: Public domain W3C validator