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
gsumle.l
gsumle.m oMnd
gsumle.n CMnd
gsumle.a
gsumle.f
gsumle.g
gsumle.c
Assertion
Ref Expression
gsumle g g

Proof of Theorem gsumle
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 gsumle.a . . 3
2 ssid 3528 . . . 4
3 sseq1 3530 . . . . . . . 8
43anbi2d 703 . . . . . . 7
5 reseq2 5274 . . . . . . . . 9
65oveq2d 6311 . . . . . . . 8 g g
7 reseq2 5274 . . . . . . . . 9
87oveq2d 6311 . . . . . . . 8 g g
96, 8breq12d 4466 . . . . . . 7 g g g g
104, 9imbi12d 320 . . . . . 6 g g g g
11 sseq1 3530 . . . . . . . 8
1211anbi2d 703 . . . . . . 7
13 reseq2 5274 . . . . . . . . 9
1413oveq2d 6311 . . . . . . . 8 g g
15 reseq2 5274 . . . . . . . . 9
1615oveq2d 6311 . . . . . . . 8 g g
1714, 16breq12d 4466 . . . . . . 7 g g g g
1812, 17imbi12d 320 . . . . . 6 g g g g
19 sseq1 3530 . . . . . . . 8
2019anbi2d 703 . . . . . . 7
21 reseq2 5274 . . . . . . . . 9
2221oveq2d 6311 . . . . . . . 8 g g
23 reseq2 5274 . . . . . . . . 9
2423oveq2d 6311 . . . . . . . 8 g g
2522, 24breq12d 4466 . . . . . . 7 g g g g
2620, 25imbi12d 320 . . . . . 6 g g g g
27 sseq1 3530 . . . . . . . 8
2827anbi2d 703 . . . . . . 7
29 reseq2 5274 . . . . . . . . 9
3029oveq2d 6311 . . . . . . . 8 g g
31 reseq2 5274 . . . . . . . . 9
3231oveq2d 6311 . . . . . . . 8 g g
3330, 32breq12d 4466 . . . . . . 7 g g g g
3428, 33imbi12d 320 . . . . . 6 g g g g
35 gsumle.m . . . . . . . . . 10 oMnd
36 omndtos 27519 . . . . . . . . . 10 oMnd Toset
37 tospos 27470 . . . . . . . . . 10 Toset
3835, 36, 373syl 20 . . . . . . . . 9
39 res0 5284 . . . . . . . . . . . 12
4039oveq2i 6306 . . . . . . . . . . 11 g g
41 eqid 2467 . . . . . . . . . . . 12
4241gsum0 15779 . . . . . . . . . . 11 g
4340, 42eqtri 2496 . . . . . . . . . 10 g
44 omndmnd 27518 . . . . . . . . . . 11 oMnd
45 gsumle.b . . . . . . . . . . . 12
4645, 41mndidcl 15811 . . . . . . . . . . 11
4735, 44, 463syl 20 . . . . . . . . . 10
4843, 47syl5eqel 2559 . . . . . . . . 9 g
49 gsumle.l . . . . . . . . . 10
5045, 49posref 15455 . . . . . . . . 9 g g g
5138, 48, 50syl2anc 661 . . . . . . . 8 g g
52 res0 5284 . . . . . . . . . 10
5339, 52eqtr4i 2499 . . . . . . . . 9
5453oveq2i 6306 . . . . . . . 8 g g
5551, 54syl6breq 4492 . . . . . . 7 g g
5655adantr 465 . . . . . 6 g g
57 ssun1 3672 . . . . . . . . . 10
58 sstr2 3516 . . . . . . . . . 10
5957, 58ax-mp 5 . . . . . . . . 9
6059anim2i 569 . . . . . . . 8
6160imim1i 58 . . . . . . 7 g g g g
62 simplr 754 . . . . . . . . . 10 g g
63 simpllr 758 . . . . . . . . . 10 g g
64 simpr 461 . . . . . . . . . 10 g g g g
65 eqid 2467 . . . . . . . . . . . 12
6635ad3antrrr 729 . . . . . . . . . . . 12 g g oMnd
67 gsumle.g . . . . . . . . . . . . . . 15
6867ad2antrr 725 . . . . . . . . . . . . . 14
69 simplr 754 . . . . . . . . . . . . . . 15
70 ssun2 3673 . . . . . . . . . . . . . . . . 17
71 vex 3121 . . . . . . . . . . . . . . . . . 18
7271snss 4157 . . . . . . . . . . . . . . . . 17
7370, 72mpbir 209 . . . . . . . . . . . . . . . 16
7473a1i 11 . . . . . . . . . . . . . . 15
7569, 74sseldd 3510 . . . . . . . . . . . . . 14
7668, 75ffvelrnd 6033 . . . . . . . . . . . . 13
7776adantr 465 . . . . . . . . . . . 12 g g
78 gsumle.n . . . . . . . . . . . . . . 15 CMnd
7978ad2antrr 725 . . . . . . . . . . . . . 14 CMnd
80 vex 3121 . . . . . . . . . . . . . . 15
8180a1i 11 . . . . . . . . . . . . . 14
82 gsumle.f . . . . . . . . . . . . . . . 16
8382ad2antrr 725 . . . . . . . . . . . . . . 15
8457, 69syl5ss 3520 . . . . . . . . . . . . . . 15
85 fssres 5757 . . . . . . . . . . . . . . 15
8683, 84, 85syl2anc 661 . . . . . . . . . . . . . 14
871ad2antrr 725 . . . . . . . . . . . . . . . 16
88 fvex 5882 . . . . . . . . . . . . . . . . 17
8988a1i 11 . . . . . . . . . . . . . . . 16
9083, 87, 89fdmfifsupp 7851 . . . . . . . . . . . . . . 15 finSupp
9190, 89fsuppres 7866 . . . . . . . . . . . . . 14 finSupp
9245, 41, 79, 81, 86, 91gsumcl 16796 . . . . . . . . . . . . 13 g
9392adantr 465 . . . . . . . . . . . 12 g g g
9483, 75ffvelrnd 6033 . . . . . . . . . . . . 13
9594adantr 465 . . . . . . . . . . . 12 g g
96 fssres 5757 . . . . . . . . . . . . . . 15
9768, 84, 96syl2anc 661 . . . . . . . . . . . . . 14
98 ssfi 7752 . . . . . . . . . . . . . . . 16
9987, 84, 98syl2anc 661 . . . . . . . . . . . . . . 15
10097, 99, 89fdmfifsupp 7851 . . . . . . . . . . . . . 14 finSupp
10145, 41, 79, 81, 97, 100gsumcl 16796 . . . . . . . . . . . . 13 g
102101adantr 465 . . . . . . . . . . . 12 g g g
103 simpr 461 . . . . . . . . . . . 12 g g g g
104 simpll 753 . . . . . . . . . . . . . 14
105 gsumle.c . . . . . . . . . . . . . . 15
106105ad2antrr 725 . . . . . . . . . . . . . 14
107 ffn 5737 . . . . . . . . . . . . . . . 16
10882, 107syl 16 . . . . . . . . . . . . . . 15
109 ffn 5737 . . . . . . . . . . . . . . . 16
11067, 109syl 16 . . . . . . . . . . . . . . 15
111 inidm 3712 . . . . . . . . . . . . . . 15
112 eqidd 2468 . . . . . . . . . . . . . . 15
113 eqidd 2468 . . . . . . . . . . . . . . 15
114108, 110, 1, 1, 111, 112, 113ofrval 6545 . . . . . . . . . . . . . 14
115104, 106, 75, 114syl3anc 1228 . . . . . . . . . . . . 13
116115adantr 465 . . . . . . . . . . . 12 g g
11779adantr 465 . . . . . . . . . . . 12 g g CMnd
11845, 49, 65, 66, 77, 93, 95, 102, 103, 116, 117omndadd2d 27522 . . . . . . . . . . 11 g g g g
11999adantr 465 . . . . . . . . . . . . 13 g g
12082ad2antrr 725 . . . . . . . . . . . . . . . . 17
121 simplr 754 . . . . . . . . . . . . . . . . . 18
122 elun1 3676 . . . . . . . . . . . . . . . . . . 19
123122adantl 466 . . . . . . . . . . . . . . . . . 18
124121, 123sseldd 3510 . . . . . . . . . . . . . . . . 17
125120, 124ffvelrnd 6033 . . . . . . . . . . . . . . . 16
126125ex 434 . . . . . . . . . . . . . . 15
127126ad2antrr 725 . . . . . . . . . . . . . 14 g g
128127imp 429 . . . . . . . . . . . . 13 g g
12971a1i 11 . . . . . . . . . . . . 13 g g
130 simplr 754 . . . . . . . . . . . . 13 g g
131 fveq2 5872 . . . . . . . . . . . . 13
13245, 65, 117, 119, 128, 129, 130, 95, 131gsumunsn 16859 . . . . . . . . . . . 12 g g g g
13383, 69feqresmpt 5928 . . . . . . . . . . . . . . 15
134133oveq2d 6311 . . . . . . . . . . . . . 14 g g
13583, 84feqresmpt 5928 . . . . . . . . . . . . . . . 16
136135oveq2d 6311 . . . . . . . . . . . . . . 15 g g
137136oveq1d 6310 . . . . . . . . . . . . . 14 g g
138134, 137eqeq12d 2489 . . . . . . . . . . . . 13 g g g g
139138adantr 465 . . . . . . . . . . . 12 g g g g g g
140132, 139mpbird 232 . . . . . . . . . . 11 g g g g
14167adantr 465 . . . . . . . . . . . . . . . . . 18
142141ad2antrr 725 . . . . . . . . . . . . . . . . 17
143124adantlr 714 . . . . . . . . . . . . . . . . 17
144142, 143ffvelrnd 6033 . . . . . . . . . . . . . . . 16
14571a1i 11 . . . . . . . . . . . . . . . 16
146 simpr 461 . . . . . . . . . . . . . . . 16
147 fveq2 5872 . . . . . . . . . . . . . . . 16
14845, 65, 79, 99, 144, 145, 146, 76, 147gsumunsn 16859 . . . . . . . . . . . . . . 15 g g
149 simpr 461 . . . . . . . . . . . . . . . . . . 19
150141, 149feqresmpt 5928 . . . . . . . . . . . . . . . . . 18
151150oveq2d 6311 . . . . . . . . . . . . . . . . 17 g g
152 resabs1 5308 . . . . . . . . . . . . . . . . . . . . 21
15357, 152mp1i 12 . . . . . . . . . . . . . . . . . . . 20
15459adantl 466 . . . . . . . . . . . . . . . . . . . . 21
155141, 154feqresmpt 5928 . . . . . . . . . . . . . . . . . . . 20
156153, 155eqtrd 2508 . . . . . . . . . . . . . . . . . . 19
157156oveq2d 6311 . . . . . . . . . . . . . . . . . 18 g g
158 resabs1 5308 . . . . . . . . . . . . . . . . . . . . . 22
15970, 158mp1i 12 . . . . . . . . . . . . . . . . . . . . 21
16070, 149syl5ss 3520 . . . . . . . . . . . . . . . . . . . . . 22
161141, 160feqresmpt 5928 . . . . . . . . . . . . . . . . . . . . 21
162159, 161eqtrd 2508 . . . . . . . . . . . . . . . . . . . 20
163162oveq2d 6311 . . . . . . . . . . . . . . . . . . 19 g g
16435, 44syl 16 . . . . . . . . . . . . . . . . . . . . 21
165164adantr 465 . . . . . . . . . . . . . . . . . . . 20
16671a1i 11 . . . . . . . . . . . . . . . . . . . 20
16773a1i 11 . . . . . . . . . . . . . . . . . . . . . 22
168149, 167sseldd 3510 . . . . . . . . . . . . . . . . . . . . 21
169141, 168ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . 20
170147adantl 466 . . . . . . . . . . . . . . . . . . . 20
17145, 165, 166, 169, 170gsumsnd 16852 . . . . . . . . . . . . . . . . . . 19 g
172163, 171eqtrd 2508 . . . . . . . . . . . . . . . . . 18 g
173157, 172oveq12d 6313 . . . . . . . . . . . . . . . . 17 g g g
174151, 173eqeq12d 2489 . . . . . . . . . . . . . . . 16 g g g g g
175174adantr 465 . . . . . . . . . . . . . . 15 g g g g g
176148, 175mpbird 232 . . . . . . . . . . . . . 14 g g g
17757, 152ax-mp 5 . . . . . . . . . . . . . . . 16
178177oveq2i 6306 . . . . . . . . . . . . . . 15 g g
17970, 158ax-mp 5 . . . . . . . . . . . . . . . 16
180179oveq2i 6306 . . . . . . . . . . . . . . 15 g g
181178, 180oveq12i 6307 . . . . . . . . . . . . . 14 g g g g
182176, 181syl6eq 2524 . . . . . . . . . . . . 13 g g g
18370, 69syl5ss 3520 . . . . . . . . . . . . . . . . 17
18468, 183feqresmpt 5928 . . . . . . . . . . . . . . . 16
185184oveq2d 6311 . . . . . . . . . . . . . . 15 g g
186 cmnmnd 16686 . . . . . . . . . . . . . . . . 17 CMnd
18779, 186syl 16 . . . . . . . . . . . . . . . 16
188 fveq2 5872 . . . . . . . . . . . . . . . . 17
18945, 188gsumsn 16854 . . . . . . . . . . . . . . . 16 g
190187, 145, 76, 189syl3anc 1228 . . . . . . . . . . . . . . 15 g
191185, 190eqtrd 2508 . . . . . . . . . . . . . 14 g
192191oveq2d 6311 . . . . . . . . . . . . 13 g g g
193182, 192eqtrd 2508 . . . . . . . . . . . 12 g g
194193adantr 465 . . . . . . . . . . 11 g g g g
195118, 140, 1943brtr4d 4483 . . . . . . . . . 10 g g g g
19662, 63, 64, 195syl21anc 1227 . . . . . . . . 9 g g g g
197196exp31 604 . . . . . . . 8 g g g g
198197a2d 26 . . . . . . 7 g g g g
19961, 198syl5 32 . . . . . 6 g g g g
20010, 18, 26, 34, 56, 199findcard2s 7773 . . . . 5 g g
201200imp 429 . . . 4 g g
2022, 201mpanr2 684 . . 3 g g
2031, 202mpancom 669 . 2 g g
204 fnresdm 5696 . . . 4
205108, 204syl 16 . . 3
206205oveq2d 6311 . 2 g g
207 fnresdm 5696 . . . 4
208110, 207syl 16 . . 3
209208oveq2d 6311 . 2 g g
210203, 206, 2093brtr3d 4482 1 g g
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 184   wa 369   wceq 1379   wcel 1767  cvv 3118   cun 3479   wss 3481  c0 3790  csn 4033   class class class wbr 4453   cmpt 4511   cres 5007   wfn 5589  wf 5590  cfv 5594  (class class class)co 6295   cofr 6534  cfn 7528  cbs 14507   cplusg 14572  cple 14579  c0g 14712   g cgsu 14713  cpo 15444  Tosetctos 15537  cmnd 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