MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  gsumval2a Structured version   Visualization version   GIF version

Theorem gsumval2a 17195
Description: Value of the group sum operation over a finite set of sequential integers. (Contributed by Mario Carneiro, 7-Dec-2014.)
Hypotheses
Ref Expression
gsumval2.b 𝐵 = (Base‘𝐺)
gsumval2.p + = (+g𝐺)
gsumval2.g (𝜑𝐺𝑉)
gsumval2.n (𝜑𝑁 ∈ (ℤ𝑀))
gsumval2.f (𝜑𝐹:(𝑀...𝑁)⟶𝐵)
gsumval2a.o 𝑂 = {𝑥𝐵 ∣ ∀𝑦𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)}
gsumval2a.f (𝜑 → ¬ ran 𝐹𝑂)
Assertion
Ref Expression
gsumval2a (𝜑 → (𝐺 Σg 𝐹) = (seq𝑀( + , 𝐹)‘𝑁))
Distinct variable groups:   𝑥,𝑦,𝐵   𝑥,𝐺,𝑦   𝑥,𝑉   𝑥, + ,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐹(𝑥,𝑦)   𝑀(𝑥,𝑦)   𝑁(𝑥,𝑦)   𝑂(𝑥,𝑦)   𝑉(𝑦)

Proof of Theorem gsumval2a
Dummy variables 𝑧 𝑓 𝑚 𝑛 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 gsumval2.b . . . 4 𝐵 = (Base‘𝐺)
2 eqid 2626 . . . 4 (0g𝐺) = (0g𝐺)
3 gsumval2.p . . . 4 + = (+g𝐺)
4 gsumval2a.o . . . 4 𝑂 = {𝑥𝐵 ∣ ∀𝑦𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)}
5 eqidd 2627 . . . 4 (𝜑 → (𝐹 “ (V ∖ 𝑂)) = (𝐹 “ (V ∖ 𝑂)))
6 gsumval2.g . . . 4 (𝜑𝐺𝑉)
7 ovex 6633 . . . . 5 (𝑀...𝑁) ∈ V
87a1i 11 . . . 4 (𝜑 → (𝑀...𝑁) ∈ V)
9 gsumval2.f . . . 4 (𝜑𝐹:(𝑀...𝑁)⟶𝐵)
101, 2, 3, 4, 5, 6, 8, 9gsumval 17187 . . 3 (𝜑 → (𝐺 Σg 𝐹) = if(ran 𝐹𝑂, (0g𝐺), if((𝑀...𝑁) ∈ ran ..., (℩𝑧𝑚𝑛 ∈ (ℤ𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑧𝑓(𝑓:(1...(#‘(𝐹 “ (V ∖ 𝑂))))–1-1-onto→(𝐹 “ (V ∖ 𝑂)) ∧ 𝑧 = (seq1( + , (𝐹𝑓))‘(#‘(𝐹 “ (V ∖ 𝑂)))))))))
11 gsumval2a.f . . . . 5 (𝜑 → ¬ ran 𝐹𝑂)
1211iffalsed 4074 . . . 4 (𝜑 → if(ran 𝐹𝑂, (0g𝐺), if((𝑀...𝑁) ∈ ran ..., (℩𝑧𝑚𝑛 ∈ (ℤ𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑧𝑓(𝑓:(1...(#‘(𝐹 “ (V ∖ 𝑂))))–1-1-onto→(𝐹 “ (V ∖ 𝑂)) ∧ 𝑧 = (seq1( + , (𝐹𝑓))‘(#‘(𝐹 “ (V ∖ 𝑂)))))))) = if((𝑀...𝑁) ∈ ran ..., (℩𝑧𝑚𝑛 ∈ (ℤ𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑧𝑓(𝑓:(1...(#‘(𝐹 “ (V ∖ 𝑂))))–1-1-onto→(𝐹 “ (V ∖ 𝑂)) ∧ 𝑧 = (seq1( + , (𝐹𝑓))‘(#‘(𝐹 “ (V ∖ 𝑂))))))))
13 gsumval2.n . . . . . . 7 (𝜑𝑁 ∈ (ℤ𝑀))
14 eluzel2 11636 . . . . . . 7 (𝑁 ∈ (ℤ𝑀) → 𝑀 ∈ ℤ)
1513, 14syl 17 . . . . . 6 (𝜑𝑀 ∈ ℤ)
16 eluzelz 11641 . . . . . . 7 (𝑁 ∈ (ℤ𝑀) → 𝑁 ∈ ℤ)
1713, 16syl 17 . . . . . 6 (𝜑𝑁 ∈ ℤ)
18 fzf 12269 . . . . . . . 8 ...:(ℤ × ℤ)⟶𝒫 ℤ
19 ffn 6004 . . . . . . . 8 (...:(ℤ × ℤ)⟶𝒫 ℤ → ... Fn (ℤ × ℤ))
2018, 19ax-mp 5 . . . . . . 7 ... Fn (ℤ × ℤ)
21 fnovrn 6763 . . . . . . 7 ((... Fn (ℤ × ℤ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀...𝑁) ∈ ran ...)
2220, 21mp3an1 1408 . . . . . 6 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀...𝑁) ∈ ran ...)
2315, 17, 22syl2anc 692 . . . . 5 (𝜑 → (𝑀...𝑁) ∈ ran ...)
2423iftrued 4071 . . . 4 (𝜑 → if((𝑀...𝑁) ∈ ran ..., (℩𝑧𝑚𝑛 ∈ (ℤ𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑧𝑓(𝑓:(1...(#‘(𝐹 “ (V ∖ 𝑂))))–1-1-onto→(𝐹 “ (V ∖ 𝑂)) ∧ 𝑧 = (seq1( + , (𝐹𝑓))‘(#‘(𝐹 “ (V ∖ 𝑂))))))) = (℩𝑧𝑚𝑛 ∈ (ℤ𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛))))
2512, 24eqtrd 2660 . . 3 (𝜑 → if(ran 𝐹𝑂, (0g𝐺), if((𝑀...𝑁) ∈ ran ..., (℩𝑧𝑚𝑛 ∈ (ℤ𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑧𝑓(𝑓:(1...(#‘(𝐹 “ (V ∖ 𝑂))))–1-1-onto→(𝐹 “ (V ∖ 𝑂)) ∧ 𝑧 = (seq1( + , (𝐹𝑓))‘(#‘(𝐹 “ (V ∖ 𝑂)))))))) = (℩𝑧𝑚𝑛 ∈ (ℤ𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛))))
2610, 25eqtrd 2660 . 2 (𝜑 → (𝐺 Σg 𝐹) = (℩𝑧𝑚𝑛 ∈ (ℤ𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛))))
27 fvex 6160 . . 3 (seq𝑀( + , 𝐹)‘𝑁) ∈ V
28 fzopth 12317 . . . . . . . . . . 11 (𝑁 ∈ (ℤ𝑀) → ((𝑀...𝑁) = (𝑚...𝑛) ↔ (𝑀 = 𝑚𝑁 = 𝑛)))
2913, 28syl 17 . . . . . . . . . 10 (𝜑 → ((𝑀...𝑁) = (𝑚...𝑛) ↔ (𝑀 = 𝑚𝑁 = 𝑛)))
30 simpl 473 . . . . . . . . . . . . . 14 ((𝑀 = 𝑚𝑁 = 𝑛) → 𝑀 = 𝑚)
3130seqeq1d 12744 . . . . . . . . . . . . 13 ((𝑀 = 𝑚𝑁 = 𝑛) → seq𝑀( + , 𝐹) = seq𝑚( + , 𝐹))
32 simpr 477 . . . . . . . . . . . . 13 ((𝑀 = 𝑚𝑁 = 𝑛) → 𝑁 = 𝑛)
3331, 32fveq12d 6156 . . . . . . . . . . . 12 ((𝑀 = 𝑚𝑁 = 𝑛) → (seq𝑀( + , 𝐹)‘𝑁) = (seq𝑚( + , 𝐹)‘𝑛))
3433eqcomd 2632 . . . . . . . . . . 11 ((𝑀 = 𝑚𝑁 = 𝑛) → (seq𝑚( + , 𝐹)‘𝑛) = (seq𝑀( + , 𝐹)‘𝑁))
35 eqeq1 2630 . . . . . . . . . . 11 (𝑧 = (seq𝑚( + , 𝐹)‘𝑛) → (𝑧 = (seq𝑀( + , 𝐹)‘𝑁) ↔ (seq𝑚( + , 𝐹)‘𝑛) = (seq𝑀( + , 𝐹)‘𝑁)))
3634, 35syl5ibrcom 237 . . . . . . . . . 10 ((𝑀 = 𝑚𝑁 = 𝑛) → (𝑧 = (seq𝑚( + , 𝐹)‘𝑛) → 𝑧 = (seq𝑀( + , 𝐹)‘𝑁)))
3729, 36syl6bi 243 . . . . . . . . 9 (𝜑 → ((𝑀...𝑁) = (𝑚...𝑛) → (𝑧 = (seq𝑚( + , 𝐹)‘𝑛) → 𝑧 = (seq𝑀( + , 𝐹)‘𝑁))))
3837impd 447 . . . . . . . 8 (𝜑 → (((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛)) → 𝑧 = (seq𝑀( + , 𝐹)‘𝑁)))
3938rexlimdvw 3032 . . . . . . 7 (𝜑 → (∃𝑛 ∈ (ℤ𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛)) → 𝑧 = (seq𝑀( + , 𝐹)‘𝑁)))
4039exlimdv 1863 . . . . . 6 (𝜑 → (∃𝑚𝑛 ∈ (ℤ𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛)) → 𝑧 = (seq𝑀( + , 𝐹)‘𝑁)))
4115adantr 481 . . . . . . . 8 ((𝜑𝑧 = (seq𝑀( + , 𝐹)‘𝑁)) → 𝑀 ∈ ℤ)
42 oveq2 6613 . . . . . . . . . . . . 13 (𝑛 = 𝑁 → (𝑀...𝑛) = (𝑀...𝑁))
4342eqcomd 2632 . . . . . . . . . . . 12 (𝑛 = 𝑁 → (𝑀...𝑁) = (𝑀...𝑛))
4443biantrurd 529 . . . . . . . . . . 11 (𝑛 = 𝑁 → (𝑧 = (seq𝑀( + , 𝐹)‘𝑛) ↔ ((𝑀...𝑁) = (𝑀...𝑛) ∧ 𝑧 = (seq𝑀( + , 𝐹)‘𝑛))))
45 fveq2 6150 . . . . . . . . . . . 12 (𝑛 = 𝑁 → (seq𝑀( + , 𝐹)‘𝑛) = (seq𝑀( + , 𝐹)‘𝑁))
4645eqeq2d 2636 . . . . . . . . . . 11 (𝑛 = 𝑁 → (𝑧 = (seq𝑀( + , 𝐹)‘𝑛) ↔ 𝑧 = (seq𝑀( + , 𝐹)‘𝑁)))
4744, 46bitr3d 270 . . . . . . . . . 10 (𝑛 = 𝑁 → (((𝑀...𝑁) = (𝑀...𝑛) ∧ 𝑧 = (seq𝑀( + , 𝐹)‘𝑛)) ↔ 𝑧 = (seq𝑀( + , 𝐹)‘𝑁)))
4847rspcev 3300 . . . . . . . . 9 ((𝑁 ∈ (ℤ𝑀) ∧ 𝑧 = (seq𝑀( + , 𝐹)‘𝑁)) → ∃𝑛 ∈ (ℤ𝑀)((𝑀...𝑁) = (𝑀...𝑛) ∧ 𝑧 = (seq𝑀( + , 𝐹)‘𝑛)))
4913, 48sylan 488 . . . . . . . 8 ((𝜑𝑧 = (seq𝑀( + , 𝐹)‘𝑁)) → ∃𝑛 ∈ (ℤ𝑀)((𝑀...𝑁) = (𝑀...𝑛) ∧ 𝑧 = (seq𝑀( + , 𝐹)‘𝑛)))
50 fveq2 6150 . . . . . . . . . 10 (𝑚 = 𝑀 → (ℤ𝑚) = (ℤ𝑀))
51 oveq1 6612 . . . . . . . . . . . 12 (𝑚 = 𝑀 → (𝑚...𝑛) = (𝑀...𝑛))
5251eqeq2d 2636 . . . . . . . . . . 11 (𝑚 = 𝑀 → ((𝑀...𝑁) = (𝑚...𝑛) ↔ (𝑀...𝑁) = (𝑀...𝑛)))
53 seqeq1 12741 . . . . . . . . . . . . 13 (𝑚 = 𝑀 → seq𝑚( + , 𝐹) = seq𝑀( + , 𝐹))
5453fveq1d 6152 . . . . . . . . . . . 12 (𝑚 = 𝑀 → (seq𝑚( + , 𝐹)‘𝑛) = (seq𝑀( + , 𝐹)‘𝑛))
5554eqeq2d 2636 . . . . . . . . . . 11 (𝑚 = 𝑀 → (𝑧 = (seq𝑚( + , 𝐹)‘𝑛) ↔ 𝑧 = (seq𝑀( + , 𝐹)‘𝑛)))
5652, 55anbi12d 746 . . . . . . . . . 10 (𝑚 = 𝑀 → (((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛)) ↔ ((𝑀...𝑁) = (𝑀...𝑛) ∧ 𝑧 = (seq𝑀( + , 𝐹)‘𝑛))))
5750, 56rexeqbidv 3147 . . . . . . . . 9 (𝑚 = 𝑀 → (∃𝑛 ∈ (ℤ𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛)) ↔ ∃𝑛 ∈ (ℤ𝑀)((𝑀...𝑁) = (𝑀...𝑛) ∧ 𝑧 = (seq𝑀( + , 𝐹)‘𝑛))))
5857spcegv 3285 . . . . . . . 8 (𝑀 ∈ ℤ → (∃𝑛 ∈ (ℤ𝑀)((𝑀...𝑁) = (𝑀...𝑛) ∧ 𝑧 = (seq𝑀( + , 𝐹)‘𝑛)) → ∃𝑚𝑛 ∈ (ℤ𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛))))
5941, 49, 58sylc 65 . . . . . . 7 ((𝜑𝑧 = (seq𝑀( + , 𝐹)‘𝑁)) → ∃𝑚𝑛 ∈ (ℤ𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛)))
6059ex 450 . . . . . 6 (𝜑 → (𝑧 = (seq𝑀( + , 𝐹)‘𝑁) → ∃𝑚𝑛 ∈ (ℤ𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛))))
6140, 60impbid 202 . . . . 5 (𝜑 → (∃𝑚𝑛 ∈ (ℤ𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛)) ↔ 𝑧 = (seq𝑀( + , 𝐹)‘𝑁)))
6261adantr 481 . . . 4 ((𝜑 ∧ (seq𝑀( + , 𝐹)‘𝑁) ∈ V) → (∃𝑚𝑛 ∈ (ℤ𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛)) ↔ 𝑧 = (seq𝑀( + , 𝐹)‘𝑁)))
6362iota5 5833 . . 3 ((𝜑 ∧ (seq𝑀( + , 𝐹)‘𝑁) ∈ V) → (℩𝑧𝑚𝑛 ∈ (ℤ𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛))) = (seq𝑀( + , 𝐹)‘𝑁))
6427, 63mpan2 706 . 2 (𝜑 → (℩𝑧𝑚𝑛 ∈ (ℤ𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛))) = (seq𝑀( + , 𝐹)‘𝑁))
6526, 64eqtrd 2660 1 (𝜑 → (𝐺 Σg 𝐹) = (seq𝑀( + , 𝐹)‘𝑁))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384   = wceq 1480  wex 1701  wcel 1992  wral 2912  wrex 2913  {crab 2916  Vcvv 3191  cdif 3557  wss 3560  ifcif 4063  𝒫 cpw 4135   × cxp 5077  ccnv 5078  ran crn 5080  cima 5082  ccom 5083  cio 5811   Fn wfn 5845  wf 5846  1-1-ontowf1o 5849  cfv 5850  (class class class)co 6605  1c1 9882  cz 11322  cuz 11631  ...cfz 12265  seqcseq 12738  #chash 13054  Basecbs 15776  +gcplusg 15857  0gc0g 16016   Σg cgsu 16017
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-8 1994  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6903  ax-cnex 9937  ax-resscn 9938  ax-pre-lttri 9955  ax-pre-lttrn 9956
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-eu 2478  df-mo 2479  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ne 2797  df-nel 2900  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3193  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-id 4994  df-po 5000  df-so 5001  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5642  df-iota 5813  df-fun 5852  df-fn 5853  df-f 5854  df-f1 5855  df-fo 5856  df-f1o 5857  df-fv 5858  df-ov 6608  df-oprab 6609  df-mpt2 6610  df-1st 7116  df-2nd 7117  df-wrecs 7353  df-recs 7414  df-rdg 7452  df-er 7688  df-en 7901  df-dom 7902  df-sdom 7903  df-pnf 10021  df-mnf 10022  df-xr 10023  df-ltxr 10024  df-le 10025  df-neg 10214  df-z 11323  df-uz 11632  df-fz 12266  df-seq 12739  df-gsum 16019
This theorem is referenced by:  gsumval2  17196
  Copyright terms: Public domain W3C validator