Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  gsumle Structured version   Unicode version

Theorem gsumle 27595
Description: A finite sum in an ordered monoid is monotonic. This proof would be much easier in an ordered group, where an inverse element would be available. (Contributed by Thierry Arnoux, 13-Mar-2018.)
Hypotheses
Ref Expression
gsumle.b  |-  B  =  ( Base `  M
)
gsumle.l  |-  .<_  =  ( le `  M )
gsumle.m  |-  ( ph  ->  M  e. oMnd )
gsumle.n  |-  ( ph  ->  M  e. CMnd )
gsumle.a  |-  ( ph  ->  A  e.  Fin )
gsumle.f  |-  ( ph  ->  F : A --> B )
gsumle.g  |-  ( ph  ->  G : A --> B )
gsumle.c  |-  ( ph  ->  F  oR  .<_  G )
Assertion
Ref Expression
gsumle  |-  ( ph  ->  ( M  gsumg  F )  .<_  ( M 
gsumg  G ) )

Proof of Theorem gsumle
Dummy variables  e 
a  y  z  x are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 gsumle.a . . 3  |-  ( ph  ->  A  e.  Fin )
2 ssid 3528 . . . 4  |-  A  C_  A
3 sseq1 3530 . . . . . . . 8  |-  ( a  =  (/)  ->  ( a 
C_  A  <->  (/)  C_  A
) )
43anbi2d 703 . . . . . . 7  |-  ( a  =  (/)  ->  ( (
ph  /\  a  C_  A )  <->  ( ph  /\  (/)  C_  A ) ) )
5 reseq2 5274 . . . . . . . . 9  |-  ( a  =  (/)  ->  ( F  |`  a )  =  ( F  |`  (/) ) )
65oveq2d 6311 . . . . . . . 8  |-  ( a  =  (/)  ->  ( M 
gsumg  ( F  |`  a ) )  =  ( M 
gsumg  ( F  |`  (/) ) ) )
7 reseq2 5274 . . . . . . . . 9  |-  ( a  =  (/)  ->  ( G  |`  a )  =  ( G  |`  (/) ) )
87oveq2d 6311 . . . . . . . 8  |-  ( a  =  (/)  ->  ( M 
gsumg  ( G  |`  a ) )  =  ( M 
gsumg  ( G  |`  (/) ) ) )
96, 8breq12d 4466 . . . . . . 7  |-  ( a  =  (/)  ->  ( ( M  gsumg  ( F  |`  a
) )  .<_  ( M 
gsumg  ( G  |`  a ) )  <->  ( M  gsumg  ( F  |`  (/) ) )  .<_  ( M  gsumg  ( G  |`  (/) ) ) ) )
104, 9imbi12d 320 . . . . . 6  |-  ( a  =  (/)  ->  ( ( ( ph  /\  a  C_  A )  ->  ( M  gsumg  ( F  |`  a
) )  .<_  ( M 
gsumg  ( G  |`  a ) ) )  <->  ( ( ph  /\  (/)  C_  A )  ->  ( M  gsumg  ( F  |`  (/) ) ) 
.<_  ( M  gsumg  ( G  |`  (/) ) ) ) ) )
11 sseq1 3530 . . . . . . . 8  |-  ( a  =  e  ->  (
a  C_  A  <->  e  C_  A ) )
1211anbi2d 703 . . . . . . 7  |-  ( a  =  e  ->  (
( ph  /\  a  C_  A )  <->  ( ph  /\  e  C_  A )
) )
13 reseq2 5274 . . . . . . . . 9  |-  ( a  =  e  ->  ( F  |`  a )  =  ( F  |`  e
) )
1413oveq2d 6311 . . . . . . . 8  |-  ( a  =  e  ->  ( M  gsumg  ( F  |`  a
) )  =  ( M  gsumg  ( F  |`  e
) ) )
15 reseq2 5274 . . . . . . . . 9  |-  ( a  =  e  ->  ( G  |`  a )  =  ( G  |`  e
) )
1615oveq2d 6311 . . . . . . . 8  |-  ( a  =  e  ->  ( M  gsumg  ( G  |`  a
) )  =  ( M  gsumg  ( G  |`  e
) ) )
1714, 16breq12d 4466 . . . . . . 7  |-  ( a  =  e  ->  (
( M  gsumg  ( F  |`  a
) )  .<_  ( M 
gsumg  ( G  |`  a ) )  <->  ( M  gsumg  ( F  |`  e ) )  .<_  ( M  gsumg  ( G  |`  e
) ) ) )
1812, 17imbi12d 320 . . . . . 6  |-  ( a  =  e  ->  (
( ( ph  /\  a  C_  A )  -> 
( M  gsumg  ( F  |`  a
) )  .<_  ( M 
gsumg  ( G  |`  a ) ) )  <->  ( ( ph  /\  e  C_  A
)  ->  ( M  gsumg  ( F  |`  e )
)  .<_  ( M  gsumg  ( G  |`  e ) ) ) ) )
19 sseq1 3530 . . . . . . . 8  |-  ( a  =  ( e  u. 
{ y } )  ->  ( a  C_  A 
<->  ( e  u.  {
y } )  C_  A ) )
2019anbi2d 703 . . . . . . 7  |-  ( a  =  ( e  u. 
{ y } )  ->  ( ( ph  /\  a  C_  A )  <->  (
ph  /\  ( e  u.  { y } ) 
C_  A ) ) )
21 reseq2 5274 . . . . . . . . 9  |-  ( a  =  ( e  u. 
{ y } )  ->  ( F  |`  a )  =  ( F  |`  ( e  u.  { y } ) ) )
2221oveq2d 6311 . . . . . . . 8  |-  ( a  =  ( e  u. 
{ y } )  ->  ( M  gsumg  ( F  |`  a ) )  =  ( M  gsumg  ( F  |`  (
e  u.  { y } ) ) ) )
23 reseq2 5274 . . . . . . . . 9  |-  ( a  =  ( e  u. 
{ y } )  ->  ( G  |`  a )  =  ( G  |`  ( e  u.  { y } ) ) )
2423oveq2d 6311 . . . . . . . 8  |-  ( a  =  ( e  u. 
{ y } )  ->  ( M  gsumg  ( G  |`  a ) )  =  ( M  gsumg  ( G  |`  (
e  u.  { y } ) ) ) )
2522, 24breq12d 4466 . . . . . . 7  |-  ( a  =  ( e  u. 
{ y } )  ->  ( ( M 
gsumg  ( F  |`  a ) )  .<_  ( M  gsumg  ( G  |`  a )
)  <->  ( M  gsumg  ( F  |`  ( e  u.  {
y } ) ) )  .<_  ( M  gsumg  ( G  |`  ( e  u.  { y } ) ) ) ) )
2620, 25imbi12d 320 . . . . . 6  |-  ( a  =  ( e  u. 
{ y } )  ->  ( ( (
ph  /\  a  C_  A )  ->  ( M  gsumg  ( F  |`  a
) )  .<_  ( M 
gsumg  ( G  |`  a ) ) )  <->  ( ( ph  /\  ( e  u. 
{ y } ) 
C_  A )  -> 
( M  gsumg  ( F  |`  (
e  u.  { y } ) ) ) 
.<_  ( M  gsumg  ( G  |`  (
e  u.  { y } ) ) ) ) ) )
27 sseq1 3530 . . . . . . . 8  |-  ( a  =  A  ->  (
a  C_  A  <->  A  C_  A
) )
2827anbi2d 703 . . . . . . 7  |-  ( a  =  A  ->  (
( ph  /\  a  C_  A )  <->  ( ph  /\  A  C_  A )
) )
29 reseq2 5274 . . . . . . . . 9  |-  ( a  =  A  ->  ( F  |`  a )  =  ( F  |`  A ) )
3029oveq2d 6311 . . . . . . . 8  |-  ( a  =  A  ->  ( M  gsumg  ( F  |`  a
) )  =  ( M  gsumg  ( F  |`  A ) ) )
31 reseq2 5274 . . . . . . . . 9  |-  ( a  =  A  ->  ( G  |`  a )  =  ( G  |`  A ) )
3231oveq2d 6311 . . . . . . . 8  |-  ( a  =  A  ->  ( M  gsumg  ( G  |`  a
) )  =  ( M  gsumg  ( G  |`  A ) ) )
3330, 32breq12d 4466 . . . . . . 7  |-  ( a  =  A  ->  (
( M  gsumg  ( F  |`  a
) )  .<_  ( M 
gsumg  ( G  |`  a ) )  <->  ( M  gsumg  ( F  |`  A ) )  .<_  ( M  gsumg  ( G  |`  A ) ) ) )
3428, 33imbi12d 320 . . . . . 6  |-  ( a  =  A  ->  (
( ( ph  /\  a  C_  A )  -> 
( M  gsumg  ( F  |`  a
) )  .<_  ( M 
gsumg  ( G  |`  a ) ) )  <->  ( ( ph  /\  A  C_  A
)  ->  ( M  gsumg  ( F  |`  A )
)  .<_  ( M  gsumg  ( G  |`  A ) ) ) ) )
35 gsumle.m . . . . . . . . . 10  |-  ( ph  ->  M  e. oMnd )
36 omndtos 27519 . . . . . . . . . 10  |-  ( M  e. oMnd  ->  M  e. Toset )
37 tospos 27470 . . . . . . . . . 10  |-  ( M  e. Toset  ->  M  e.  Poset )
3835, 36, 373syl 20 . . . . . . . . 9  |-  ( ph  ->  M  e.  Poset )
39 res0 5284 . . . . . . . . . . . 12  |-  ( F  |`  (/) )  =  (/)
4039oveq2i 6306 . . . . . . . . . . 11  |-  ( M 
gsumg  ( F  |`  (/) ) )  =  ( M  gsumg  (/) )
41 eqid 2467 . . . . . . . . . . . 12  |-  ( 0g
`  M )  =  ( 0g `  M
)
4241gsum0 15779 . . . . . . . . . . 11  |-  ( M 
gsumg  (/) )  =  ( 0g
`  M )
4340, 42eqtri 2496 . . . . . . . . . 10  |-  ( M 
gsumg  ( F  |`  (/) ) )  =  ( 0g `  M )
44 omndmnd 27518 . . . . . . . . . . 11  |-  ( M  e. oMnd  ->  M  e.  Mnd )
45 gsumle.b . . . . . . . . . . . 12  |-  B  =  ( Base `  M
)
4645, 41mndidcl 15811 . . . . . . . . . . 11  |-  ( M  e.  Mnd  ->  ( 0g `  M )  e.  B )
4735, 44, 463syl 20 . . . . . . . . . 10  |-  ( ph  ->  ( 0g `  M
)  e.  B )
4843, 47syl5eqel 2559 . . . . . . . . 9  |-  ( ph  ->  ( M  gsumg  ( F  |`  (/) ) )  e.  B )
49 gsumle.l . . . . . . . . . 10  |-  .<_  =  ( le `  M )
5045, 49posref 15455 . . . . . . . . 9  |-  ( ( M  e.  Poset  /\  ( M  gsumg  ( F  |`  (/) ) )  e.  B )  -> 
( M  gsumg  ( F  |`  (/) ) ) 
.<_  ( M  gsumg  ( F  |`  (/) ) ) )
5138, 48, 50syl2anc 661 . . . . . . . 8  |-  ( ph  ->  ( M  gsumg  ( F  |`  (/) ) ) 
.<_  ( M  gsumg  ( F  |`  (/) ) ) )
52 res0 5284 . . . . . . . . . 10  |-  ( G  |`  (/) )  =  (/)
5339, 52eqtr4i 2499 . . . . . . . . 9  |-  ( F  |`  (/) )  =  ( G  |`  (/) )
5453oveq2i 6306 . . . . . . . 8  |-  ( M 
gsumg  ( F  |`  (/) ) )  =  ( M  gsumg  ( G  |`  (/) ) )
5551, 54syl6breq 4492 . . . . . . 7  |-  ( ph  ->  ( M  gsumg  ( F  |`  (/) ) ) 
.<_  ( M  gsumg  ( G  |`  (/) ) ) )
5655adantr 465 . . . . . 6  |-  ( (
ph  /\  (/)  C_  A
)  ->  ( M  gsumg  ( F  |`  (/) ) ) 
.<_  ( M  gsumg  ( G  |`  (/) ) ) )
57 ssun1 3672 . . . . . . . . . 10  |-  e  C_  ( e  u.  {
y } )
58 sstr2 3516 . . . . . . . . . 10  |-  ( e 
C_  ( e  u. 
{ y } )  ->  ( ( e  u.  { y } )  C_  A  ->  e 
C_  A ) )
5957, 58ax-mp 5 . . . . . . . . 9  |-  ( ( e  u.  { y } )  C_  A  ->  e  C_  A )
6059anim2i 569 . . . . . . . 8  |-  ( (
ph  /\  ( e  u.  { y } ) 
C_  A )  -> 
( ph  /\  e  C_  A ) )
6160imim1i 58 . . . . . . 7  |-  ( ( ( ph  /\  e  C_  A )  ->  ( M  gsumg  ( F  |`  e
) )  .<_  ( M 
gsumg  ( G  |`  e ) ) )  ->  (
( ph  /\  (
e  u.  { y } )  C_  A
)  ->  ( M  gsumg  ( F  |`  e )
)  .<_  ( M  gsumg  ( G  |`  e ) ) ) )
62 simplr 754 . . . . . . . . . 10  |-  ( ( ( ( e  e. 
Fin  /\  -.  y  e.  e )  /\  ( ph  /\  ( e  u. 
{ y } ) 
C_  A ) )  /\  ( M  gsumg  ( F  |`  e ) )  .<_  ( M  gsumg  ( G  |`  e
) ) )  -> 
( ph  /\  (
e  u.  { y } )  C_  A
) )
63 simpllr 758 . . . . . . . . . 10  |-  ( ( ( ( e  e. 
Fin  /\  -.  y  e.  e )  /\  ( ph  /\  ( e  u. 
{ y } ) 
C_  A ) )  /\  ( M  gsumg  ( F  |`  e ) )  .<_  ( M  gsumg  ( G  |`  e
) ) )  ->  -.  y  e.  e
)
64 simpr 461 . . . . . . . . . 10  |-  ( ( ( ( e  e. 
Fin  /\  -.  y  e.  e )  /\  ( ph  /\  ( e  u. 
{ y } ) 
C_  A ) )  /\  ( M  gsumg  ( F  |`  e ) )  .<_  ( M  gsumg  ( G  |`  e
) ) )  -> 
( M  gsumg  ( F  |`  e
) )  .<_  ( M 
gsumg  ( G  |`  e ) ) )
65 eqid 2467 . . . . . . . . . . . 12  |-  ( +g  `  M )  =  ( +g  `  M )
6635ad3antrrr 729 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( e  u.  {
y } )  C_  A )  /\  -.  y  e.  e )  /\  ( M  gsumg  ( F  |`  e
) )  .<_  ( M 
gsumg  ( G  |`  e ) ) )  ->  M  e. oMnd )
67 gsumle.g . . . . . . . . . . . . . . 15  |-  ( ph  ->  G : A --> B )
6867ad2antrr 725 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
e  u.  { y } )  C_  A
)  /\  -.  y  e.  e )  ->  G : A --> B )
69 simplr 754 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
e  u.  { y } )  C_  A
)  /\  -.  y  e.  e )  ->  (
e  u.  { y } )  C_  A
)
70 ssun2 3673 . . . . . . . . . . . . . . . . 17  |-  { y }  C_  ( e  u.  { y } )
71 vex 3121 . . . . . . . . . . . . . . . . . 18  |-  y  e. 
_V
7271snss 4157 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  ( e  u. 
{ y } )  <->  { y }  C_  ( e  u.  {
y } ) )
7370, 72mpbir 209 . . . . . . . . . . . . . . . 16  |-  y  e.  ( e  u.  {
y } )
7473a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
e  u.  { y } )  C_  A
)  /\  -.  y  e.  e )  ->  y  e.  ( e  u.  {
y } ) )
7569, 74sseldd 3510 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
e  u.  { y } )  C_  A
)  /\  -.  y  e.  e )  ->  y  e.  A )
7668, 75ffvelrnd 6033 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
e  u.  { y } )  C_  A
)  /\  -.  y  e.  e )  ->  ( G `  y )  e.  B )
7776adantr 465 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( e  u.  {
y } )  C_  A )  /\  -.  y  e.  e )  /\  ( M  gsumg  ( F  |`  e
) )  .<_  ( M 
gsumg  ( G  |`  e ) ) )  ->  ( G `  y )  e.  B )
78 gsumle.n . . . . . . . . . . . . . . 15  |-  ( ph  ->  M  e. CMnd )
7978ad2antrr 725 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
e  u.  { y } )  C_  A
)  /\  -.  y  e.  e )  ->  M  e. CMnd )
80 vex 3121 . . . . . . . . . . . . . . 15  |-  e  e. 
_V
8180a1i 11 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
e  u.  { y } )  C_  A
)  /\  -.  y  e.  e )  ->  e  e.  _V )
82 gsumle.f . . . . . . . . . . . . . . . 16  |-  ( ph  ->  F : A --> B )
8382ad2antrr 725 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
e  u.  { y } )  C_  A
)  /\  -.  y  e.  e )  ->  F : A --> B )
8457, 69syl5ss 3520 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
e  u.  { y } )  C_  A
)  /\  -.  y  e.  e )  ->  e  C_  A )
85 fssres 5757 . . . . . . . . . . . . . . 15  |-  ( ( F : A --> B  /\  e  C_  A )  -> 
( F  |`  e
) : e --> B )
8683, 84, 85syl2anc 661 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
e  u.  { y } )  C_  A
)  /\  -.  y  e.  e )  ->  ( F  |`  e ) : e --> B )
871ad2antrr 725 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
e  u.  { y } )  C_  A
)  /\  -.  y  e.  e )  ->  A  e.  Fin )
88 fvex 5882 . . . . . . . . . . . . . . . . 17  |-  ( 0g
`  M )  e. 
_V
8988a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
e  u.  { y } )  C_  A
)  /\  -.  y  e.  e )  ->  ( 0g `  M )  e. 
_V )
9083, 87, 89fdmfifsupp 7851 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
e  u.  { y } )  C_  A
)  /\  -.  y  e.  e )  ->  F finSupp  ( 0g `  M ) )
9190, 89fsuppres 7866 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
e  u.  { y } )  C_  A
)  /\  -.  y  e.  e )  ->  ( F  |`  e ) finSupp  ( 0g `  M ) )
9245, 41, 79, 81, 86, 91gsumcl 16796 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
e  u.  { y } )  C_  A
)  /\  -.  y  e.  e )  ->  ( M  gsumg  ( F  |`  e
) )  e.  B
)
9392adantr 465 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( e  u.  {
y } )  C_  A )  /\  -.  y  e.  e )  /\  ( M  gsumg  ( F  |`  e
) )  .<_  ( M 
gsumg  ( G  |`  e ) ) )  ->  ( M  gsumg  ( F  |`  e
) )  e.  B
)
9483, 75ffvelrnd 6033 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
e  u.  { y } )  C_  A
)  /\  -.  y  e.  e )  ->  ( F `  y )  e.  B )
9594adantr 465 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( e  u.  {
y } )  C_  A )  /\  -.  y  e.  e )  /\  ( M  gsumg  ( F  |`  e
) )  .<_  ( M 
gsumg  ( G  |`  e ) ) )  ->  ( F `  y )  e.  B )
96 fssres 5757 . . . . . . . . . . . . . . 15  |-  ( ( G : A --> B  /\  e  C_  A )  -> 
( G  |`  e
) : e --> B )
9768, 84, 96syl2anc 661 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
e  u.  { y } )  C_  A
)  /\  -.  y  e.  e )  ->  ( G  |`  e ) : e --> B )
98 ssfi 7752 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  Fin  /\  e  C_  A )  -> 
e  e.  Fin )
9987, 84, 98syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
e  u.  { y } )  C_  A
)  /\  -.  y  e.  e )  ->  e  e.  Fin )
10097, 99, 89fdmfifsupp 7851 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
e  u.  { y } )  C_  A
)  /\  -.  y  e.  e )  ->  ( G  |`  e ) finSupp  ( 0g `  M ) )
10145, 41, 79, 81, 97, 100gsumcl 16796 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
e  u.  { y } )  C_  A
)  /\  -.  y  e.  e )  ->  ( M  gsumg  ( G  |`  e
) )  e.  B
)
102101adantr 465 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( e  u.  {
y } )  C_  A )  /\  -.  y  e.  e )  /\  ( M  gsumg  ( F  |`  e
) )  .<_  ( M 
gsumg  ( G  |`  e ) ) )  ->  ( M  gsumg  ( G  |`  e
) )  e.  B
)
103 simpr 461 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( e  u.  {
y } )  C_  A )  /\  -.  y  e.  e )  /\  ( M  gsumg  ( F  |`  e
) )  .<_  ( M 
gsumg  ( G  |`  e ) ) )  ->  ( M  gsumg  ( F  |`  e
) )  .<_  ( M 
gsumg  ( G  |`  e ) ) )
104 simpll 753 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
e  u.  { y } )  C_  A
)  /\  -.  y  e.  e )  ->  ph )
105 gsumle.c . . . . . . . . . . . . . . 15  |-  ( ph  ->  F  oR  .<_  G )
106105ad2antrr 725 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
e  u.  { y } )  C_  A
)  /\  -.  y  e.  e )  ->  F  oR  .<_  G )
107 ffn 5737 . . . . . . . . . . . . . . . 16  |-  ( F : A --> B  ->  F  Fn  A )
10882, 107syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  F  Fn  A )
109 ffn 5737 . . . . . . . . . . . . . . . 16  |-  ( G : A --> B  ->  G  Fn  A )
11067, 109syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  G  Fn  A )
111 inidm 3712 . . . . . . . . . . . . . . 15  |-  ( A  i^i  A )  =  A
112 eqidd 2468 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  A )  ->  ( F `  y )  =  ( F `  y ) )
113 eqidd 2468 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  A )  ->  ( G `  y )  =  ( G `  y ) )
114108, 110, 1, 1, 111, 112, 113ofrval 6545 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  F  oR  .<_  G  /\  y  e.  A )  ->  ( F `  y )  .<_  ( G `  y
) )
115104, 106, 75, 114syl3anc 1228 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
e  u.  { y } )  C_  A
)  /\  -.  y  e.  e )  ->  ( F `  y )  .<_  ( G `  y
) )
116115adantr 465 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( e  u.  {
y } )  C_  A )  /\  -.  y  e.  e )  /\  ( M  gsumg  ( F  |`  e
) )  .<_  ( M 
gsumg  ( G  |`  e ) ) )  ->  ( F `  y )  .<_  ( G `  y
) )
11779adantr 465 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( e  u.  {
y } )  C_  A )  /\  -.  y  e.  e )  /\  ( M  gsumg  ( F  |`  e
) )  .<_  ( M 
gsumg  ( G  |`  e ) ) )  ->  M  e. CMnd )
11845, 49, 65, 66, 77, 93, 95, 102, 103, 116, 117omndadd2d 27522 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( e  u.  {
y } )  C_  A )  /\  -.  y  e.  e )  /\  ( M  gsumg  ( F  |`  e
) )  .<_  ( M 
gsumg  ( G  |`  e ) ) )  ->  (
( M  gsumg  ( F  |`  e
) ) ( +g  `  M ) ( F `
 y ) ) 
.<_  ( ( M  gsumg  ( G  |`  e ) ) ( +g  `  M ) ( G `  y
) ) )
11999adantr 465 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( e  u.  {
y } )  C_  A )  /\  -.  y  e.  e )  /\  ( M  gsumg  ( F  |`  e
) )  .<_  ( M 
gsumg  ( G  |`  e ) ) )  ->  e  e.  Fin )
12082ad2antrr 725 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
e  u.  { y } )  C_  A
)  /\  z  e.  e )  ->  F : A --> B )
121 simplr 754 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
e  u.  { y } )  C_  A
)  /\  z  e.  e )  ->  (
e  u.  { y } )  C_  A
)
122 elun1 3676 . . . . . . . . . . . . . . . . . . 19  |-  ( z  e.  e  ->  z  e.  ( e  u.  {
y } ) )
123122adantl 466 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
e  u.  { y } )  C_  A
)  /\  z  e.  e )  ->  z  e.  ( e  u.  {
y } ) )
124121, 123sseldd 3510 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
e  u.  { y } )  C_  A
)  /\  z  e.  e )  ->  z  e.  A )
125120, 124ffvelrnd 6033 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
e  u.  { y } )  C_  A
)  /\  z  e.  e )  ->  ( F `  z )  e.  B )
126125ex 434 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( e  u.  { y } ) 
C_  A )  -> 
( z  e.  e  ->  ( F `  z )  e.  B
) )
127126ad2antrr 725 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( e  u.  {
y } )  C_  A )  /\  -.  y  e.  e )  /\  ( M  gsumg  ( F  |`  e
) )  .<_  ( M 
gsumg  ( G  |`  e ) ) )  ->  (
z  e.  e  -> 
( F `  z
)  e.  B ) )
128127imp 429 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  ( e  u.  {
y } )  C_  A )  /\  -.  y  e.  e )  /\  ( M  gsumg  ( F  |`  e
) )  .<_  ( M 
gsumg  ( G  |`  e ) ) )  /\  z  e.  e )  ->  ( F `  z )  e.  B )
12971a1i 11 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( e  u.  {
y } )  C_  A )  /\  -.  y  e.  e )  /\  ( M  gsumg  ( F  |`  e
) )  .<_  ( M 
gsumg  ( G  |`  e ) ) )  ->  y  e.  _V )
130 simplr 754 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( e  u.  {
y } )  C_  A )  /\  -.  y  e.  e )  /\  ( M  gsumg  ( F  |`  e
) )  .<_  ( M 
gsumg  ( G  |`  e ) ) )  ->  -.  y  e.  e )
131 fveq2 5872 . . . . . . . . . . . . 13  |-  ( z  =  y  ->  ( F `  z )  =  ( F `  y ) )
13245, 65, 117, 119, 128, 129, 130, 95, 131gsumunsn 16859 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( e  u.  {
y } )  C_  A )  /\  -.  y  e.  e )  /\  ( M  gsumg  ( F  |`  e
) )  .<_  ( M 
gsumg  ( G  |`  e ) ) )  ->  ( M  gsumg  ( z  e.  ( e  u.  { y } )  |->  ( F `
 z ) ) )  =  ( ( M  gsumg  ( z  e.  e 
|->  ( F `  z
) ) ) ( +g  `  M ) ( F `  y
) ) )
13383, 69feqresmpt 5928 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
e  u.  { y } )  C_  A
)  /\  -.  y  e.  e )  ->  ( F  |`  ( e  u. 
{ y } ) )  =  ( z  e.  ( e  u. 
{ y } ) 
|->  ( F `  z
) ) )
134133oveq2d 6311 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
e  u.  { y } )  C_  A
)  /\  -.  y  e.  e )  ->  ( M  gsumg  ( F  |`  (
e  u.  { y } ) ) )  =  ( M  gsumg  ( z  e.  ( e  u. 
{ y } ) 
|->  ( F `  z
) ) ) )
13583, 84feqresmpt 5928 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
e  u.  { y } )  C_  A
)  /\  -.  y  e.  e )  ->  ( F  |`  e )  =  ( z  e.  e 
|->  ( F `  z
) ) )
136135oveq2d 6311 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
e  u.  { y } )  C_  A
)  /\  -.  y  e.  e )  ->  ( M  gsumg  ( F  |`  e
) )  =  ( M  gsumg  ( z  e.  e 
|->  ( F `  z
) ) ) )
137136oveq1d 6310 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
e  u.  { y } )  C_  A
)  /\  -.  y  e.  e )  ->  (
( M  gsumg  ( F  |`  e
) ) ( +g  `  M ) ( F `
 y ) )  =  ( ( M 
gsumg  ( z  e.  e 
|->  ( F `  z
) ) ) ( +g  `  M ) ( F `  y
) ) )
138134, 137eqeq12d 2489 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
e  u.  { y } )  C_  A
)  /\  -.  y  e.  e )  ->  (
( M  gsumg  ( F  |`  (
e  u.  { y } ) ) )  =  ( ( M 
gsumg  ( F  |`  e ) ) ( +g  `  M
) ( F `  y ) )  <->  ( M  gsumg  ( z  e.  ( e  u.  { y } )  |->  ( F `  z ) ) )  =  ( ( M 
gsumg  ( z  e.  e 
|->  ( F `  z
) ) ) ( +g  `  M ) ( F `  y
) ) ) )
139138adantr 465 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( e  u.  {
y } )  C_  A )  /\  -.  y  e.  e )  /\  ( M  gsumg  ( F  |`  e
) )  .<_  ( M 
gsumg  ( G  |`  e ) ) )  ->  (
( M  gsumg  ( F  |`  (
e  u.  { y } ) ) )  =  ( ( M 
gsumg  ( F  |`  e ) ) ( +g  `  M
) ( F `  y ) )  <->  ( M  gsumg  ( z  e.  ( e  u.  { y } )  |->  ( F `  z ) ) )  =  ( ( M 
gsumg  ( z  e.  e 
|->  ( F `  z
) ) ) ( +g  `  M ) ( F `  y
) ) ) )
140132, 139mpbird 232 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( e  u.  {
y } )  C_  A )  /\  -.  y  e.  e )  /\  ( M  gsumg  ( F  |`  e
) )  .<_  ( M 
gsumg  ( G  |`  e ) ) )  ->  ( M  gsumg  ( F  |`  (
e  u.  { y } ) ) )  =  ( ( M 
gsumg  ( F  |`  e ) ) ( +g  `  M
) ( F `  y ) ) )
14167adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( e  u.  { y } ) 
C_  A )  ->  G : A --> B )
142141ad2antrr 725 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( e  u.  {
y } )  C_  A )  /\  -.  y  e.  e )  /\  z  e.  e
)  ->  G : A
--> B )
143124adantlr 714 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( e  u.  {
y } )  C_  A )  /\  -.  y  e.  e )  /\  z  e.  e
)  ->  z  e.  A )
144142, 143ffvelrnd 6033 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( e  u.  {
y } )  C_  A )  /\  -.  y  e.  e )  /\  z  e.  e
)  ->  ( G `  z )  e.  B
)
14571a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
e  u.  { y } )  C_  A
)  /\  -.  y  e.  e )  ->  y  e.  _V )
146 simpr 461 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
e  u.  { y } )  C_  A
)  /\  -.  y  e.  e )  ->  -.  y  e.  e )
147 fveq2 5872 . . . . . . . . . . . . . . . 16  |-  ( z  =  y  ->  ( G `  z )  =  ( G `  y ) )
14845, 65, 79, 99, 144, 145, 146, 76, 147gsumunsn 16859 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
e  u.  { y } )  C_  A
)  /\  -.  y  e.  e )  ->  ( M  gsumg  ( z  e.  ( e  u.  { y } )  |->  ( G `
 z ) ) )  =  ( ( M  gsumg  ( z  e.  e 
|->  ( G `  z
) ) ) ( +g  `  M ) ( G `  y
) ) )
149 simpr 461 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( e  u.  { y } ) 
C_  A )  -> 
( e  u.  {
y } )  C_  A )
150141, 149feqresmpt 5928 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( e  u.  { y } ) 
C_  A )  -> 
( G  |`  (
e  u.  { y } ) )  =  ( z  e.  ( e  u.  { y } )  |->  ( G `
 z ) ) )
151150oveq2d 6311 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( e  u.  { y } ) 
C_  A )  -> 
( M  gsumg  ( G  |`  (
e  u.  { y } ) ) )  =  ( M  gsumg  ( z  e.  ( e  u. 
{ y } ) 
|->  ( G `  z
) ) ) )
152 resabs1 5308 . . . . . . . . . . . . . . . . . . . . 21  |-  ( e 
C_  ( e  u. 
{ y } )  ->  ( ( G  |`  ( e  u.  {
y } ) )  |`  e )  =  ( G  |`  e )
)
15357, 152mp1i 12 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( e  u.  { y } ) 
C_  A )  -> 
( ( G  |`  ( e  u.  {
y } ) )  |`  e )  =  ( G  |`  e )
)
15459adantl 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( e  u.  { y } ) 
C_  A )  -> 
e  C_  A )
155141, 154feqresmpt 5928 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( e  u.  { y } ) 
C_  A )  -> 
( G  |`  e
)  =  ( z  e.  e  |->  ( G `
 z ) ) )
156153, 155eqtrd 2508 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( e  u.  { y } ) 
C_  A )  -> 
( ( G  |`  ( e  u.  {
y } ) )  |`  e )  =  ( z  e.  e  |->  ( G `  z ) ) )
157156oveq2d 6311 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( e  u.  { y } ) 
C_  A )  -> 
( M  gsumg  ( ( G  |`  ( e  u.  {
y } ) )  |`  e ) )  =  ( M  gsumg  ( z  e.  e 
|->  ( G `  z
) ) ) )
158 resabs1 5308 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( { y }  C_  (
e  u.  { y } )  ->  (
( G  |`  (
e  u.  { y } ) )  |`  { y } )  =  ( G  |`  { y } ) )
15970, 158mp1i 12 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( e  u.  { y } ) 
C_  A )  -> 
( ( G  |`  ( e  u.  {
y } ) )  |`  { y } )  =  ( G  |`  { y } ) )
16070, 149syl5ss 3520 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( e  u.  { y } ) 
C_  A )  ->  { y }  C_  A )
161141, 160feqresmpt 5928 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( e  u.  { y } ) 
C_  A )  -> 
( G  |`  { y } )  =  ( z  e.  { y }  |->  ( G `  z ) ) )
162159, 161eqtrd 2508 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( e  u.  { y } ) 
C_  A )  -> 
( ( G  |`  ( e  u.  {
y } ) )  |`  { y } )  =  ( z  e. 
{ y }  |->  ( G `  z ) ) )
163162oveq2d 6311 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( e  u.  { y } ) 
C_  A )  -> 
( M  gsumg  ( ( G  |`  ( e  u.  {
y } ) )  |`  { y } ) )  =  ( M 
gsumg  ( z  e.  {
y }  |->  ( G `
 z ) ) ) )
16435, 44syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  M  e.  Mnd )
165164adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( e  u.  { y } ) 
C_  A )  ->  M  e.  Mnd )
16671a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( e  u.  { y } ) 
C_  A )  -> 
y  e.  _V )
16773a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( e  u.  { y } ) 
C_  A )  -> 
y  e.  ( e  u.  { y } ) )
168149, 167sseldd 3510 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( e  u.  { y } ) 
C_  A )  -> 
y  e.  A )
169141, 168ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( e  u.  { y } ) 
C_  A )  -> 
( G `  y
)  e.  B )
170147adantl 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
e  u.  { y } )  C_  A
)  /\  z  =  y )  ->  ( G `  z )  =  ( G `  y ) )
17145, 165, 166, 169, 170gsumsnd 16852 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( e  u.  { y } ) 
C_  A )  -> 
( M  gsumg  ( z  e.  {
y }  |->  ( G `
 z ) ) )  =  ( G `
 y ) )
172163, 171eqtrd 2508 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( e  u.  { y } ) 
C_  A )  -> 
( M  gsumg  ( ( G  |`  ( e  u.  {
y } ) )  |`  { y } ) )  =  ( G `
 y ) )
173157, 172oveq12d 6313 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( e  u.  { y } ) 
C_  A )  -> 
( ( M  gsumg  ( ( G  |`  ( e  u.  { y } ) )  |`  e )
) ( +g  `  M
) ( M  gsumg  ( ( G  |`  ( e  u.  { y } ) )  |`  { y } ) ) )  =  ( ( M 
gsumg  ( z  e.  e 
|->  ( G `  z
) ) ) ( +g  `  M ) ( G `  y
) ) )
174151, 173eqeq12d 2489 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( e  u.  { y } ) 
C_  A )  -> 
( ( M  gsumg  ( G  |`  ( e  u.  {
y } ) ) )  =  ( ( M  gsumg  ( ( G  |`  ( e  u.  {
y } ) )  |`  e ) ) ( +g  `  M ) ( M  gsumg  ( ( G  |`  ( e  u.  {
y } ) )  |`  { y } ) ) )  <->  ( M  gsumg  ( z  e.  ( e  u.  { y } )  |->  ( G `  z ) ) )  =  ( ( M 
gsumg  ( z  e.  e 
|->  ( G `  z
) ) ) ( +g  `  M ) ( G `  y
) ) ) )
175174adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
e  u.  { y } )  C_  A
)  /\  -.  y  e.  e )  ->  (
( M  gsumg  ( G  |`  (
e  u.  { y } ) ) )  =  ( ( M 
gsumg  ( ( G  |`  ( e  u.  {
y } ) )  |`  e ) ) ( +g  `  M ) ( M  gsumg  ( ( G  |`  ( e  u.  {
y } ) )  |`  { y } ) ) )  <->  ( M  gsumg  ( z  e.  ( e  u.  { y } )  |->  ( G `  z ) ) )  =  ( ( M 
gsumg  ( z  e.  e 
|->  ( G `  z
) ) ) ( +g  `  M ) ( G `  y
) ) ) )
176148, 175mpbird 232 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
e  u.  { y } )  C_  A
)  /\  -.  y  e.  e )  ->  ( M  gsumg  ( G  |`  (
e  u.  { y } ) ) )  =  ( ( M 
gsumg  ( ( G  |`  ( e  u.  {
y } ) )  |`  e ) ) ( +g  `  M ) ( M  gsumg  ( ( G  |`  ( e  u.  {
y } ) )  |`  { y } ) ) ) )
17757, 152ax-mp 5 . . . . . . . . . . . . . . . 16  |-  ( ( G  |`  ( e  u.  { y } ) )  |`  e )  =  ( G  |`  e )
178177oveq2i 6306 . . . . . . . . . . . . . . 15  |-  ( M 
gsumg  ( ( G  |`  ( e  u.  {
y } ) )  |`  e ) )  =  ( M  gsumg  ( G  |`  e
) )
17970, 158ax-mp 5 . . . . . . . . . . . . . . . 16  |-  ( ( G  |`  ( e  u.  { y } ) )  |`  { y } )  =  ( G  |`  { y } )
180179oveq2i 6306 . . . . . . . . . . . . . . 15  |-  ( M 
gsumg  ( ( G  |`  ( e  u.  {
y } ) )  |`  { y } ) )  =  ( M 
gsumg  ( G  |`  { y } ) )
181178, 180oveq12i 6307 . . . . . . . . . . . . . 14  |-  ( ( M  gsumg  ( ( G  |`  ( e  u.  {
y } ) )  |`  e ) ) ( +g  `  M ) ( M  gsumg  ( ( G  |`  ( e  u.  {
y } ) )  |`  { y } ) ) )  =  ( ( M  gsumg  ( G  |`  e
) ) ( +g  `  M ) ( M 
gsumg  ( G  |`  { y } ) ) )
182176, 181syl6eq 2524 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
e  u.  { y } )  C_  A
)  /\  -.  y  e.  e )  ->  ( M  gsumg  ( G  |`  (
e  u.  { y } ) ) )  =  ( ( M 
gsumg  ( G  |`  e ) ) ( +g  `  M
) ( M  gsumg  ( G  |`  { y } ) ) ) )
18370, 69syl5ss 3520 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
e  u.  { y } )  C_  A
)  /\  -.  y  e.  e )  ->  { y }  C_  A )
18468, 183feqresmpt 5928 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
e  u.  { y } )  C_  A
)  /\  -.  y  e.  e )  ->  ( G  |`  { y } )  =  ( x  e.  { y } 
|->  ( G `  x
) ) )
185184oveq2d 6311 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
e  u.  { y } )  C_  A
)  /\  -.  y  e.  e )  ->  ( M  gsumg  ( G  |`  { y } ) )  =  ( M  gsumg  ( x  e.  {
y }  |->  ( G `
 x ) ) ) )
186 cmnmnd 16686 . . . . . . . . . . . . . . . . 17  |-  ( M  e. CMnd  ->  M  e.  Mnd )
18779, 186syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
e  u.  { y } )  C_  A
)  /\  -.  y  e.  e )  ->  M  e.  Mnd )
188 fveq2 5872 . . . . . . . . . . . . . . . . 17  |-  ( x  =  y  ->  ( G `  x )  =  ( G `  y ) )
18945, 188gsumsn 16854 . . . . . . . . . . . . . . . 16  |-  ( ( M  e.  Mnd  /\  y  e.  _V  /\  ( G `  y )  e.  B )  ->  ( M  gsumg  ( x  e.  {
y }  |->  ( G `
 x ) ) )  =  ( G `
 y ) )
190187, 145, 76, 189syl3anc 1228 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
e  u.  { y } )  C_  A
)  /\  -.  y  e.  e )  ->  ( M  gsumg  ( x  e.  {
y }  |->  ( G `
 x ) ) )  =  ( G `
 y ) )
191185, 190eqtrd 2508 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
e  u.  { y } )  C_  A
)  /\  -.  y  e.  e )  ->  ( M  gsumg  ( G  |`  { y } ) )  =  ( G `  y
) )
192191oveq2d 6311 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
e  u.  { y } )  C_  A
)  /\  -.  y  e.  e )  ->  (
( M  gsumg  ( G  |`  e
) ) ( +g  `  M ) ( M 
gsumg  ( G  |`  { y } ) ) )  =  ( ( M 
gsumg  ( G  |`  e ) ) ( +g  `  M
) ( G `  y ) ) )
193182, 192eqtrd 2508 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
e  u.  { y } )  C_  A
)  /\  -.  y  e.  e )  ->  ( M  gsumg  ( G  |`  (
e  u.  { y } ) ) )  =  ( ( M 
gsumg  ( G  |`  e ) ) ( +g  `  M
) ( G `  y ) ) )
194193adantr 465 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( e  u.  {
y } )  C_  A )  /\  -.  y  e.  e )  /\  ( M  gsumg  ( F  |`  e
) )  .<_  ( M 
gsumg  ( G  |`  e ) ) )  ->  ( M  gsumg  ( G  |`  (
e  u.  { y } ) ) )  =  ( ( M 
gsumg  ( G  |`  e ) ) ( +g  `  M
) ( G `  y ) ) )
195118, 140, 1943brtr4d 4483 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  ( e  u.  {
y } )  C_  A )  /\  -.  y  e.  e )  /\  ( M  gsumg  ( F  |`  e
) )  .<_  ( M 
gsumg  ( G  |`  e ) ) )  ->  ( M  gsumg  ( F  |`  (
e  u.  { y } ) ) ) 
.<_  ( M  gsumg  ( G  |`  (
e  u.  { y } ) ) ) )
19662, 63, 64, 195syl21anc 1227 . . . . . . . . 9  |-  ( ( ( ( e  e. 
Fin  /\  -.  y  e.  e )  /\  ( ph  /\  ( e  u. 
{ y } ) 
C_  A ) )  /\  ( M  gsumg  ( F  |`  e ) )  .<_  ( M  gsumg  ( G  |`  e
) ) )  -> 
( M  gsumg  ( F  |`  (
e  u.  { y } ) ) ) 
.<_  ( M  gsumg  ( G  |`  (
e  u.  { y } ) ) ) )
197196exp31 604 . . . . . . . 8  |-  ( ( e  e.  Fin  /\  -.  y  e.  e
)  ->  ( ( ph  /\  ( e  u. 
{ y } ) 
C_  A )  -> 
( ( M  gsumg  ( F  |`  e ) )  .<_  ( M  gsumg  ( G  |`  e
) )  ->  ( M  gsumg  ( F  |`  (
e  u.  { y } ) ) ) 
.<_  ( M  gsumg  ( G  |`  (
e  u.  { y } ) ) ) ) ) )
198197a2d 26 . . . . . . 7  |-  ( ( e  e.  Fin  /\  -.  y  e.  e
)  ->  ( (
( ph  /\  (
e  u.  { y } )  C_  A
)  ->  ( M  gsumg  ( F  |`  e )
)  .<_  ( M  gsumg  ( G  |`  e ) ) )  ->  ( ( ph  /\  ( e  u.  {
y } )  C_  A )  ->  ( M  gsumg  ( F  |`  (
e  u.  { y } ) ) ) 
.<_  ( M  gsumg  ( G  |`  (
e  u.  { y } ) ) ) ) ) )
19961, 198syl5 32 . . . . . 6  |-  ( ( e  e.  Fin  /\  -.  y  e.  e
)  ->  ( (
( ph  /\  e  C_  A )  ->  ( M  gsumg  ( F  |`  e
) )  .<_  ( M 
gsumg  ( G  |`  e ) ) )  ->  (
( ph  /\  (
e  u.  { y } )  C_  A
)  ->  ( M  gsumg  ( F  |`  ( e  u.  { y } ) ) )  .<_  ( M 
gsumg  ( G  |`  ( e  u.  { y } ) ) ) ) ) )
20010, 18, 26, 34, 56, 199findcard2s 7773 . . . . 5  |-  ( A  e.  Fin  ->  (
( ph  /\  A  C_  A )  ->  ( M  gsumg  ( F  |`  A ) )  .<_  ( M  gsumg  ( G  |`  A )
) ) )
201200imp 429 . . . 4  |-  ( ( A  e.  Fin  /\  ( ph  /\  A  C_  A ) )  -> 
( M  gsumg  ( F  |`  A ) )  .<_  ( M  gsumg  ( G  |`  A )
) )
2022, 201mpanr2 684 . . 3  |-  ( ( A  e.  Fin  /\  ph )  ->  ( M  gsumg  ( F  |`  A )
)  .<_  ( M  gsumg  ( G  |`  A ) ) )
2031, 202mpancom 669 . 2  |-  ( ph  ->  ( M  gsumg  ( F  |`  A ) )  .<_  ( M  gsumg  ( G  |`  A )
) )
204 fnresdm 5696 . . . 4  |-  ( F  Fn  A  ->  ( F  |`  A )  =  F )
205108, 204syl 16 . . 3  |-  ( ph  ->  ( F  |`  A )  =  F )
206205oveq2d 6311 . 2  |-  ( ph  ->  ( M  gsumg  ( F  |`  A ) )  =  ( M 
gsumg  F ) )
207 fnresdm 5696 . . . 4  |-  ( G  Fn  A  ->  ( G  |`  A )  =  G )
208110, 207syl 16 . . 3  |-  ( ph  ->  ( G  |`  A )  =  G )
209208oveq2d 6311 . 2  |-  ( ph  ->  ( M  gsumg  ( G  |`  A ) )  =  ( M 
gsumg  G ) )
210203, 206, 2093brtr3d 4482 1  |-  ( ph  ->  ( M  gsumg  F )  .<_  ( M 
gsumg  G ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1379    e. wcel 1767   _Vcvv 3118    u. cun 3479    C_ wss 3481   (/)c0 3790   {csn 4033   class class class wbr 4453    |-> cmpt 4511    |` cres 5007    Fn wfn 5589   -->wf 5590   ` cfv 5594  (class class class)co 6295    oRcofr 6534   Fincfn 7528   Basecbs 14507   +g cplusg 14572   lecple 14579   0gc0g 14712    gsumg cgsu 14713   Posetcpo 15444  Tosetctos 15537   Mndcmnd 15793  CMndccmn 16671  oMndcomnd 27511
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4564  ax-sep 4574  ax-nul 4582  ax-pow 4631  ax-pr 4692  ax-un 6587  ax-inf2 8070  ax-cnex 9560  ax-resscn 9561  ax-1cn 9562  ax-icn 9563  ax-addcl 9564  ax-addrcl 9565  ax-mulcl 9566  ax-mulrcl 9567  ax-mulcom 9568  ax-addass 9569  ax-mulass 9570  ax-distr 9571  ax-i2m1 9572  ax-1ne0 9573  ax-1rid 9574  ax-rnegex 9575  ax-rrecex 9576  ax-cnre 9577  ax-pre-lttri 9578  ax-pre-lttrn 9579  ax-pre-ltadd 9580  ax-pre-mulgt0 9581
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2822  df-rex 2823  df-reu 2824  df-rmo 2825  df-rab 2826  df-v 3120  df-sbc 3337  df-csb 3441  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-pss 3497  df-nul 3791  df-if 3946  df-pw 4018  df-sn 4034  df-pr 4036  df-tp 4038  df-op 4040  df-uni 4252  df-int 4289  df-iun 4333  df-iin 4334  df-br 4454  df-opab 4512  df-mpt 4513  df-tr 4547  df-eprel 4797  df-id 4801  df-po 4806  df-so 4807  df-fr 4844  df-se 4845  df-we 4846  df-ord 4887  df-on 4888  df-lim 4889  df-suc 4890  df-xp 5011  df-rel 5012  df-cnv 5013  df-co 5014  df-dm 5015  df-rn 5016  df-res 5017  df-ima 5018  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-isom 5603  df-riota 6256  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-of 6535  df-ofr 6536  df-om 6696  df-1st 6795  df-2nd 6796  df-supp 6914  df-recs 7054  df-rdg 7088  df-1o 7142  df-oadd 7146  df-er 7323  df-en 7529  df-dom 7530  df-sdom 7531  df-fin 7532  df-fsupp 7842  df-oi 7947  df-card 8332  df-pnf 9642  df-mnf 9643  df-xr 9644  df-ltxr 9645  df-le 9646  df-sub 9819  df-neg 9820  df-nn 10549  df-2 10606  df-n0 10808  df-z 10877  df-uz 11095  df-fz 11685  df-fzo 11805  df-seq 12088  df-hash 12386  df-ndx 14510  df-slot 14511  df-base 14512  df-sets 14513  df-ress 14514  df-plusg 14585  df-0g 14714  df-gsum 14715  df-mre 14858  df-mrc 14859  df-acs 14861  df-poset 15450  df-toset 15538  df-mgm 15746  df-sgrp 15785  df-mnd 15795  df-submnd 15840  df-mulg 15932  df-cntz 16227  df-cmn 16673  df-omnd 27513
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator