Theorem gsumval 18435

Description: Expand out the substitutions in df-gsum 17227. (Contributed by Mario Carneiro, 7-Dec-2014.)

Hypotheses

Ref	Expression
gsumval.b	⊢ 𝐵 = (Base‘𝐺)
gsumval.z	⊢ 0 = (0g‘𝐺)
gsumval.p	⊢ + = (+g‘𝐺)
gsumval.o	⊢ 𝑂 = {𝑠 ∈ 𝐵 ∣ ∀𝑡 ∈ 𝐵 ((𝑠 + 𝑡) = 𝑡 ∧ (𝑡 + 𝑠) = 𝑡)}
gsumval.w	⊢ (𝜑 → 𝑊 = (◡𝐹 “ (V ∖ 𝑂)))
gsumval.g	⊢ (𝜑 → 𝐺 ∈ 𝑉)
gsumval.a	⊢ (𝜑 → 𝐴 ∈ 𝑋)
gsumval.f	⊢ (𝜑 → 𝐹:𝐴⟶𝐵)

Assertion

Ref	Expression
gsumval	⊢ (𝜑 → (𝐺 Σg 𝐹) = if(ran 𝐹 ⊆ 𝑂, 0 , if(𝐴 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑥∃𝑓(𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘𝑊)))))))

Distinct variable groups:   𝑡,𝑠,𝑥,𝐵   𝑓,𝑚,𝑛,𝑥,𝜑   𝑓,𝐹,𝑚,𝑛,𝑥   𝑓,𝐺,𝑚,𝑛,𝑥   + ,𝑠,𝑡,𝑥   𝑓,𝑂,𝑚,𝑛,𝑥

Allowed substitution hints:   𝜑(𝑡,𝑠)   𝐴(𝑥,𝑡,𝑓,𝑚,𝑛,𝑠)   𝐵(𝑓,𝑚,𝑛)   + (𝑓,𝑚,𝑛)   𝐹(𝑡,𝑠)   𝐺(𝑡,𝑠)   𝑂(𝑡,𝑠)   𝑉(𝑥,𝑡,𝑓,𝑚,𝑛,𝑠)   𝑊(𝑥,𝑡,𝑓,𝑚,𝑛,𝑠)   𝑋(𝑥,𝑡,𝑓,𝑚,𝑛,𝑠)   0 (𝑥,𝑡,𝑓,𝑚,𝑛,𝑠)

Proof of Theorem gsumval

Step	Hyp	Ref	Expression
1		gsumval.b	. 2 ⊢ 𝐵 = (Base‘𝐺)
2		gsumval.z	. 2 ⊢ 0 = (0g‘𝐺)
3		gsumval.p	. 2 ⊢ + = (+g‘𝐺)
4		gsumval.o	. 2 ⊢ 𝑂 = {𝑠 ∈ 𝐵 ∣ ∀𝑡 ∈ 𝐵 ((𝑠 + 𝑡) = 𝑡 ∧ (𝑡 + 𝑠) = 𝑡)}
5		gsumval.w	. 2 ⊢ (𝜑 → 𝑊 = (◡𝐹 “ (V ∖ 𝑂)))
6		gsumval.g	. 2 ⊢ (𝜑 → 𝐺 ∈ 𝑉)
7		gsumval.f	. . 3 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
8		gsumval.a	. . 3 ⊢ (𝜑 → 𝐴 ∈ 𝑋)
9	1	fvexi 6825	. . . 4 ⊢ 𝐵 ∈ V
10	9	a1i 11	. . 3 ⊢ (𝜑 → 𝐵 ∈ V)
11		fex2 7826	. . 3 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ V) → 𝐹 ∈ V)
12	7, 8, 10, 11	syl3anc 1370	. 2 ⊢ (𝜑 → 𝐹 ∈ V)
13	7	fdmd 6648	. 2 ⊢ (𝜑 → dom 𝐹 = 𝐴)
14	1, 2, 3, 4, 5, 6, 12, 13	gsumvalx 18434	1 ⊢ (𝜑 → (𝐺 Σg 𝐹) = if(ran 𝐹 ⊆ 𝑂, 0 , if(𝐴 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑥∃𝑓(𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘𝑊)))))))

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1540  ∃wex 1780   ∈ wcel 2105  ∀wral 3061  ∃wrex 3070  {crab 3403  Vcvv 3440   ∖ cdif 3893   ⊆ wss 3896  ifcif 4470  ^◡ccnv 5606  ran crn 5608   “ cima 5610   ∘ ccom 5611  ℩cio 6415  ⟶wf 6461  –1-1-onto→wf1o 6464  ‘cfv 6465  (class class class)co 7316  1c1 10951  ℤ_≥cuz 12661  ...cfz 13318  seqcseq 13800  ♯chash 14123  Basecbs 16986  +_gcplusg 17036  0_gc0g 17224   Σ_g cgsu 17225

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-sep 5237  ax-nul 5244  ax-pow 5302  ax-pr 5366  ax-un 7629

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3404  df-v 3442  df-sbc 3726  df-csb 3842  df-dif 3899  df-un 3901  df-in 3903  df-ss 3913  df-nul 4267  df-if 4471  df-pw 4546  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4850  df-br 5087  df-opab 5149  df-mpt 5170  df-id 5506  df-xp 5613  df-rel 5614  df-cnv 5615  df-co 5616  df-dm 5617  df-rn 5618  df-res 5619  df-ima 5620  df-pred 6224  df-iota 6417  df-fun 6467  df-fn 6468  df-f 6469  df-f1 6470  df-fo 6471  df-f1o 6472  df-fv 6473  df-ov 7319  df-oprab 7320  df-mpo 7321  df-frecs 8145  df-wrecs 8176  df-recs 8250  df-rdg 8289  df-seq 13801  df-gsum 17227

This theorem is referenced by:  gsumress  18440  gsumval1  18441  gsumval2a  18443  gsumval3a  19576