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

Theorem gsumvalx 17006
Description: Expand out the substitutions in df-gsum 15831. (Contributed by Mario Carneiro, 18-Sep-2015.)
Hypotheses
Ref Expression
gsumval.b 𝐵 = (Base‘𝐺)
gsumval.z 0 = (0g𝐺)
gsumval.p + = (+g𝐺)
gsumval.o 𝑂 = {𝑠𝐵 ∣ ∀𝑡𝐵 ((𝑠 + 𝑡) = 𝑡 ∧ (𝑡 + 𝑠) = 𝑡)}
gsumval.w (𝜑𝑊 = (𝐹 “ (V ∖ 𝑂)))
gsumval.g (𝜑𝐺𝑉)
gsumvalx.f (𝜑𝐹𝑋)
gsumvalx.a (𝜑 → dom 𝐹 = 𝐴)
Assertion
Ref Expression
gsumvalx (𝜑 → (𝐺 Σg 𝐹) = if(ran 𝐹𝑂, 0 , if(𝐴 ∈ ran ..., (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑥𝑓(𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(#‘𝑊)))))))
Distinct variable groups:   𝑡,𝑠,𝑥,𝐵   𝑓,𝑚,𝑛,𝑥,𝜑   𝑓,𝐹,𝑚,𝑛,𝑥   𝑓,𝐺,𝑚,𝑛,𝑥   + ,𝑠,𝑡,𝑥   𝑓,𝑂,𝑚,𝑛,𝑥
Allowed substitution hints:   𝜑(𝑡,𝑠)   𝐴(𝑥,𝑡,𝑓,𝑚,𝑛,𝑠)   𝐵(𝑓,𝑚,𝑛)   + (𝑓,𝑚,𝑛)   𝐹(𝑡,𝑠)   𝐺(𝑡,𝑠)   𝑂(𝑡,𝑠)   𝑉(𝑥,𝑡,𝑓,𝑚,𝑛,𝑠)   𝑊(𝑥,𝑡,𝑓,𝑚,𝑛,𝑠)   𝑋(𝑥,𝑡,𝑓,𝑚,𝑛,𝑠)   0 (𝑥,𝑡,𝑓,𝑚,𝑛,𝑠)

Proof of Theorem gsumvalx
Dummy variables 𝑔 𝑜 𝑤 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-gsum 15831 . . 3 Σg = (𝑤 ∈ V, 𝑔 ∈ V ↦ {𝑥 ∈ (Base‘𝑤) ∣ ∀𝑦 ∈ (Base‘𝑤)((𝑥(+g𝑤)𝑦) = 𝑦 ∧ (𝑦(+g𝑤)𝑥) = 𝑦)} / 𝑜if(ran 𝑔𝑜, (0g𝑤), if(dom 𝑔 ∈ ran ..., (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝑤), 𝑔)‘𝑛))), (℩𝑥𝑓[(𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(#‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑔𝑓))‘(#‘𝑦)))))))
21a1i 11 . 2 (𝜑 → Σg = (𝑤 ∈ V, 𝑔 ∈ V ↦ {𝑥 ∈ (Base‘𝑤) ∣ ∀𝑦 ∈ (Base‘𝑤)((𝑥(+g𝑤)𝑦) = 𝑦 ∧ (𝑦(+g𝑤)𝑥) = 𝑦)} / 𝑜if(ran 𝑔𝑜, (0g𝑤), if(dom 𝑔 ∈ ran ..., (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝑤), 𝑔)‘𝑛))), (℩𝑥𝑓[(𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(#‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑔𝑓))‘(#‘𝑦))))))))
3 simprl 789 . . . . . . . 8 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → 𝑤 = 𝐺)
43fveq2d 5990 . . . . . . 7 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → (Base‘𝑤) = (Base‘𝐺))
5 gsumval.b . . . . . . 7 𝐵 = (Base‘𝐺)
64, 5syl6eqr 2566 . . . . . 6 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → (Base‘𝑤) = 𝐵)
73fveq2d 5990 . . . . . . . . . . 11 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → (+g𝑤) = (+g𝐺))
8 gsumval.p . . . . . . . . . . 11 + = (+g𝐺)
97, 8syl6eqr 2566 . . . . . . . . . 10 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → (+g𝑤) = + )
109oveqd 6442 . . . . . . . . 9 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → (𝑥(+g𝑤)𝑦) = (𝑥 + 𝑦))
1110eqeq1d 2516 . . . . . . . 8 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → ((𝑥(+g𝑤)𝑦) = 𝑦 ↔ (𝑥 + 𝑦) = 𝑦))
129oveqd 6442 . . . . . . . . 9 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → (𝑦(+g𝑤)𝑥) = (𝑦 + 𝑥))
1312eqeq1d 2516 . . . . . . . 8 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → ((𝑦(+g𝑤)𝑥) = 𝑦 ↔ (𝑦 + 𝑥) = 𝑦))
1411, 13anbi12d 742 . . . . . . 7 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → (((𝑥(+g𝑤)𝑦) = 𝑦 ∧ (𝑦(+g𝑤)𝑥) = 𝑦) ↔ ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)))
156, 14raleqbidv 3033 . . . . . 6 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → (∀𝑦 ∈ (Base‘𝑤)((𝑥(+g𝑤)𝑦) = 𝑦 ∧ (𝑦(+g𝑤)𝑥) = 𝑦) ↔ ∀𝑦𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)))
166, 15rabeqbidv 3072 . . . . 5 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → {𝑥 ∈ (Base‘𝑤) ∣ ∀𝑦 ∈ (Base‘𝑤)((𝑥(+g𝑤)𝑦) = 𝑦 ∧ (𝑦(+g𝑤)𝑥) = 𝑦)} = {𝑥𝐵 ∣ ∀𝑦𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)})
17 gsumval.o . . . . . 6 𝑂 = {𝑠𝐵 ∣ ∀𝑡𝐵 ((𝑠 + 𝑡) = 𝑡 ∧ (𝑡 + 𝑠) = 𝑡)}
18 oveq2 6433 . . . . . . . . . . 11 (𝑡 = 𝑦 → (𝑠 + 𝑡) = (𝑠 + 𝑦))
19 id 22 . . . . . . . . . . 11 (𝑡 = 𝑦𝑡 = 𝑦)
2018, 19eqeq12d 2529 . . . . . . . . . 10 (𝑡 = 𝑦 → ((𝑠 + 𝑡) = 𝑡 ↔ (𝑠 + 𝑦) = 𝑦))
21 oveq1 6432 . . . . . . . . . . 11 (𝑡 = 𝑦 → (𝑡 + 𝑠) = (𝑦 + 𝑠))
2221, 19eqeq12d 2529 . . . . . . . . . 10 (𝑡 = 𝑦 → ((𝑡 + 𝑠) = 𝑡 ↔ (𝑦 + 𝑠) = 𝑦))
2320, 22anbi12d 742 . . . . . . . . 9 (𝑡 = 𝑦 → (((𝑠 + 𝑡) = 𝑡 ∧ (𝑡 + 𝑠) = 𝑡) ↔ ((𝑠 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑠) = 𝑦)))
2423cbvralv 3051 . . . . . . . 8 (∀𝑡𝐵 ((𝑠 + 𝑡) = 𝑡 ∧ (𝑡 + 𝑠) = 𝑡) ↔ ∀𝑦𝐵 ((𝑠 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑠) = 𝑦))
25 oveq1 6432 . . . . . . . . . . 11 (𝑠 = 𝑥 → (𝑠 + 𝑦) = (𝑥 + 𝑦))
2625eqeq1d 2516 . . . . . . . . . 10 (𝑠 = 𝑥 → ((𝑠 + 𝑦) = 𝑦 ↔ (𝑥 + 𝑦) = 𝑦))
27 oveq2 6433 . . . . . . . . . . 11 (𝑠 = 𝑥 → (𝑦 + 𝑠) = (𝑦 + 𝑥))
2827eqeq1d 2516 . . . . . . . . . 10 (𝑠 = 𝑥 → ((𝑦 + 𝑠) = 𝑦 ↔ (𝑦 + 𝑥) = 𝑦))
2926, 28anbi12d 742 . . . . . . . . 9 (𝑠 = 𝑥 → (((𝑠 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑠) = 𝑦) ↔ ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)))
3029ralbidv 2873 . . . . . . . 8 (𝑠 = 𝑥 → (∀𝑦𝐵 ((𝑠 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑠) = 𝑦) ↔ ∀𝑦𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)))
3124, 30syl5bb 270 . . . . . . 7 (𝑠 = 𝑥 → (∀𝑡𝐵 ((𝑠 + 𝑡) = 𝑡 ∧ (𝑡 + 𝑠) = 𝑡) ↔ ∀𝑦𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)))
3231cbvrabv 3076 . . . . . 6 {𝑠𝐵 ∣ ∀𝑡𝐵 ((𝑠 + 𝑡) = 𝑡 ∧ (𝑡 + 𝑠) = 𝑡)} = {𝑥𝐵 ∣ ∀𝑦𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)}
3317, 32eqtri 2536 . . . . 5 𝑂 = {𝑥𝐵 ∣ ∀𝑦𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)}
3416, 33syl6eqr 2566 . . . 4 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → {𝑥 ∈ (Base‘𝑤) ∣ ∀𝑦 ∈ (Base‘𝑤)((𝑥(+g𝑤)𝑦) = 𝑦 ∧ (𝑦(+g𝑤)𝑥) = 𝑦)} = 𝑂)
3534csbeq1d 3410 . . 3 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → {𝑥 ∈ (Base‘𝑤) ∣ ∀𝑦 ∈ (Base‘𝑤)((𝑥(+g𝑤)𝑦) = 𝑦 ∧ (𝑦(+g𝑤)𝑥) = 𝑦)} / 𝑜if(ran 𝑔𝑜, (0g𝑤), if(dom 𝑔 ∈ ran ..., (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝑤), 𝑔)‘𝑛))), (℩𝑥𝑓[(𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(#‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑔𝑓))‘(#‘𝑦)))))) = 𝑂 / 𝑜if(ran 𝑔𝑜, (0g𝑤), if(dom 𝑔 ∈ ran ..., (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝑤), 𝑔)‘𝑛))), (℩𝑥𝑓[(𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(#‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑔𝑓))‘(#‘𝑦)))))))
36 fvex 5996 . . . . . . 7 (Base‘𝐺) ∈ V
375, 36eqeltri 2588 . . . . . 6 𝐵 ∈ V
3817, 37rabex2 4641 . . . . 5 𝑂 ∈ V
3938a1i 11 . . . 4 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → 𝑂 ∈ V)
40 simplrr 796 . . . . . . 7 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → 𝑔 = 𝐹)
4140rneqd 5165 . . . . . 6 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → ran 𝑔 = ran 𝐹)
42 simpr 475 . . . . . 6 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → 𝑜 = 𝑂)
4341, 42sseq12d 3501 . . . . 5 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (ran 𝑔𝑜 ↔ ran 𝐹𝑂))
443adantr 479 . . . . . . 7 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → 𝑤 = 𝐺)
4544fveq2d 5990 . . . . . 6 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (0g𝑤) = (0g𝐺))
46 gsumval.z . . . . . 6 0 = (0g𝐺)
4745, 46syl6eqr 2566 . . . . 5 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (0g𝑤) = 0 )
4840dmeqd 5139 . . . . . . . 8 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → dom 𝑔 = dom 𝐹)
49 gsumvalx.a . . . . . . . . 9 (𝜑 → dom 𝐹 = 𝐴)
5049ad2antrr 757 . . . . . . . 8 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → dom 𝐹 = 𝐴)
5148, 50eqtrd 2548 . . . . . . 7 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → dom 𝑔 = 𝐴)
5251eleq1d 2576 . . . . . 6 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (dom 𝑔 ∈ ran ... ↔ 𝐴 ∈ ran ...))
5351eqeq1d 2516 . . . . . . . . . 10 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (dom 𝑔 = (𝑚...𝑛) ↔ 𝐴 = (𝑚...𝑛)))
549adantr 479 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (+g𝑤) = + )
5554seqeq2d 12535 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → seq𝑚((+g𝑤), 𝑔) = seq𝑚( + , 𝑔))
5640seqeq3d 12536 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → seq𝑚( + , 𝑔) = seq𝑚( + , 𝐹))
5755, 56eqtrd 2548 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → seq𝑚((+g𝑤), 𝑔) = seq𝑚( + , 𝐹))
5857fveq1d 5988 . . . . . . . . . . 11 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (seq𝑚((+g𝑤), 𝑔)‘𝑛) = (seq𝑚( + , 𝐹)‘𝑛))
5958eqeq2d 2524 . . . . . . . . . 10 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (𝑥 = (seq𝑚((+g𝑤), 𝑔)‘𝑛) ↔ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛)))
6053, 59anbi12d 742 . . . . . . . . 9 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → ((dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝑤), 𝑔)‘𝑛)) ↔ (𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))))
6160rexbidv 2938 . . . . . . . 8 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (∃𝑛 ∈ (ℤ𝑚)(dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝑤), 𝑔)‘𝑛)) ↔ ∃𝑛 ∈ (ℤ𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))))
6261exbidv 1803 . . . . . . 7 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (∃𝑚𝑛 ∈ (ℤ𝑚)(dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝑤), 𝑔)‘𝑛)) ↔ ∃𝑚𝑛 ∈ (ℤ𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))))
6362iotabidv 5674 . . . . . 6 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝑤), 𝑔)‘𝑛))) = (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))))
6442difeq2d 3594 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (V ∖ 𝑜) = (V ∖ 𝑂))
6564imaeq2d 5275 . . . . . . . . . . 11 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (𝐹 “ (V ∖ 𝑜)) = (𝐹 “ (V ∖ 𝑂)))
6640cnveqd 5112 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → 𝑔 = 𝐹)
6766imaeq1d 5274 . . . . . . . . . . 11 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (𝑔 “ (V ∖ 𝑜)) = (𝐹 “ (V ∖ 𝑜)))
68 gsumval.w . . . . . . . . . . . 12 (𝜑𝑊 = (𝐹 “ (V ∖ 𝑂)))
6968ad2antrr 757 . . . . . . . . . . 11 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → 𝑊 = (𝐹 “ (V ∖ 𝑂)))
7065, 67, 693eqtr4d 2558 . . . . . . . . . 10 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (𝑔 “ (V ∖ 𝑜)) = 𝑊)
7170sbceq1d 3311 . . . . . . . . 9 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → ([(𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(#‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑔𝑓))‘(#‘𝑦))) ↔ [𝑊 / 𝑦](𝑓:(1...(#‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑔𝑓))‘(#‘𝑦)))))
72 gsumvalx.f . . . . . . . . . . . . 13 (𝜑𝐹𝑋)
73 cnvexg 6878 . . . . . . . . . . . . 13 (𝐹𝑋𝐹 ∈ V)
74 imaexg 6869 . . . . . . . . . . . . 13 (𝐹 ∈ V → (𝐹 “ (V ∖ 𝑂)) ∈ V)
7572, 73, 743syl 18 . . . . . . . . . . . 12 (𝜑 → (𝐹 “ (V ∖ 𝑂)) ∈ V)
7668, 75eqeltrd 2592 . . . . . . . . . . 11 (𝜑𝑊 ∈ V)
7776ad2antrr 757 . . . . . . . . . 10 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → 𝑊 ∈ V)
78 fveq2 5986 . . . . . . . . . . . . . . 15 (𝑦 = 𝑊 → (#‘𝑦) = (#‘𝑊))
7978adantl 480 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (#‘𝑦) = (#‘𝑊))
8079oveq2d 6441 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (1...(#‘𝑦)) = (1...(#‘𝑊)))
81 f1oeq2 5924 . . . . . . . . . . . . 13 ((1...(#‘𝑦)) = (1...(#‘𝑊)) → (𝑓:(1...(#‘𝑦))–1-1-onto𝑦𝑓:(1...(#‘𝑊))–1-1-onto𝑦))
8280, 81syl 17 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (𝑓:(1...(#‘𝑦))–1-1-onto𝑦𝑓:(1...(#‘𝑊))–1-1-onto𝑦))
83 f1oeq3 5925 . . . . . . . . . . . . 13 (𝑦 = 𝑊 → (𝑓:(1...(#‘𝑊))–1-1-onto𝑦𝑓:(1...(#‘𝑊))–1-1-onto𝑊))
8483adantl 480 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (𝑓:(1...(#‘𝑊))–1-1-onto𝑦𝑓:(1...(#‘𝑊))–1-1-onto𝑊))
8582, 84bitrd 266 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (𝑓:(1...(#‘𝑦))–1-1-onto𝑦𝑓:(1...(#‘𝑊))–1-1-onto𝑊))
8654seqeq2d 12535 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → seq1((+g𝑤), (𝑔𝑓)) = seq1( + , (𝑔𝑓)))
8740coeq1d 5097 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (𝑔𝑓) = (𝐹𝑓))
8887seqeq3d 12536 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → seq1( + , (𝑔𝑓)) = seq1( + , (𝐹𝑓)))
8986, 88eqtrd 2548 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → seq1((+g𝑤), (𝑔𝑓)) = seq1( + , (𝐹𝑓)))
9089adantr 479 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → seq1((+g𝑤), (𝑔𝑓)) = seq1( + , (𝐹𝑓)))
9190, 79fveq12d 5992 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (seq1((+g𝑤), (𝑔𝑓))‘(#‘𝑦)) = (seq1( + , (𝐹𝑓))‘(#‘𝑊)))
9291eqeq2d 2524 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (𝑥 = (seq1((+g𝑤), (𝑔𝑓))‘(#‘𝑦)) ↔ 𝑥 = (seq1( + , (𝐹𝑓))‘(#‘𝑊))))
9385, 92anbi12d 742 . . . . . . . . . 10 ((((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → ((𝑓:(1...(#‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑔𝑓))‘(#‘𝑦))) ↔ (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(#‘𝑊)))))
9477, 93sbcied 3343 . . . . . . . . 9 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → ([𝑊 / 𝑦](𝑓:(1...(#‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑔𝑓))‘(#‘𝑦))) ↔ (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(#‘𝑊)))))
9571, 94bitrd 266 . . . . . . . 8 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → ([(𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(#‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑔𝑓))‘(#‘𝑦))) ↔ (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(#‘𝑊)))))
9695exbidv 1803 . . . . . . 7 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (∃𝑓[(𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(#‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑔𝑓))‘(#‘𝑦))) ↔ ∃𝑓(𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(#‘𝑊)))))
9796iotabidv 5674 . . . . . 6 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (℩𝑥𝑓[(𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(#‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑔𝑓))‘(#‘𝑦)))) = (℩𝑥𝑓(𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(#‘𝑊)))))
9852, 63, 97ifbieq12d 3966 . . . . 5 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → if(dom 𝑔 ∈ ran ..., (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝑤), 𝑔)‘𝑛))), (℩𝑥𝑓[(𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(#‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑔𝑓))‘(#‘𝑦))))) = if(𝐴 ∈ ran ..., (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑥𝑓(𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(#‘𝑊))))))
9943, 47, 98ifbieq12d 3966 . . . 4 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → if(ran 𝑔𝑜, (0g𝑤), if(dom 𝑔 ∈ ran ..., (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝑤), 𝑔)‘𝑛))), (℩𝑥𝑓[(𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(#‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑔𝑓))‘(#‘𝑦)))))) = if(ran 𝐹𝑂, 0 , if(𝐴 ∈ ran ..., (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑥𝑓(𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(#‘𝑊)))))))
10039, 99csbied 3430 . . 3 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → 𝑂 / 𝑜if(ran 𝑔𝑜, (0g𝑤), if(dom 𝑔 ∈ ran ..., (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝑤), 𝑔)‘𝑛))), (℩𝑥𝑓[(𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(#‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑔𝑓))‘(#‘𝑦)))))) = if(ran 𝐹𝑂, 0 , if(𝐴 ∈ ran ..., (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑥𝑓(𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(#‘𝑊)))))))
10135, 100eqtrd 2548 . 2 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → {𝑥 ∈ (Base‘𝑤) ∣ ∀𝑦 ∈ (Base‘𝑤)((𝑥(+g𝑤)𝑦) = 𝑦 ∧ (𝑦(+g𝑤)𝑥) = 𝑦)} / 𝑜if(ran 𝑔𝑜, (0g𝑤), if(dom 𝑔 ∈ ran ..., (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝑤), 𝑔)‘𝑛))), (℩𝑥𝑓[(𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(#‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑔𝑓))‘(#‘𝑦)))))) = if(ran 𝐹𝑂, 0 , if(𝐴 ∈ ran ..., (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑥𝑓(𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(#‘𝑊)))))))
102 gsumval.g . . 3 (𝜑𝐺𝑉)
103102elexd 3091 . 2 (𝜑𝐺 ∈ V)
10472elexd 3091 . 2 (𝜑𝐹 ∈ V)
105 fvex 5996 . . . . 5 (0g𝐺) ∈ V
10646, 105eqeltri 2588 . . . 4 0 ∈ V
107 iotaex 5670 . . . . 5 (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))) ∈ V
108 iotaex 5670 . . . . 5 (℩𝑥𝑓(𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(#‘𝑊)))) ∈ V
109107, 108ifex 4009 . . . 4 if(𝐴 ∈ ran ..., (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑥𝑓(𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(#‘𝑊))))) ∈ V
110106, 109ifex 4009 . . 3 if(ran 𝐹𝑂, 0 , if(𝐴 ∈ ran ..., (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑥𝑓(𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(#‘𝑊)))))) ∈ V
111110a1i 11 . 2 (𝜑 → if(ran 𝐹𝑂, 0 , if(𝐴 ∈ ran ..., (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑥𝑓(𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(#‘𝑊)))))) ∈ V)
1122, 101, 103, 104, 111ovmpt2d 6561 1 (𝜑 → (𝐺 Σg 𝐹) = if(ran 𝐹𝑂, 0 , if(𝐴 ∈ ran ..., (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑥𝑓(𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(#‘𝑊)))))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382   = wceq 1474  wex 1694  wcel 1938  wral 2800  wrex 2801  {crab 2804  Vcvv 3077  [wsbc 3306  csb 3403  cdif 3441  wss 3444  ifcif 3939  ccnv 4931  dom cdm 4932  ran crn 4933  cima 4935  ccom 4936  cio 5651  1-1-ontowf1o 5688  cfv 5689  (class class class)co 6425  cmpt2 6427  1c1 9690  cuz 11423  ...cfz 12062  seqcseq 12528  #chash 12844  Basecbs 15600  +gcplusg 15673  0gc0g 15828   Σg cgsu 15829
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-8 1940  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-sep 4607  ax-nul 4616  ax-pow 4668  ax-pr 4732  ax-un 6721
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-eu 2366  df-mo 2367  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ral 2805  df-rex 2806  df-rab 2809  df-v 3079  df-sbc 3307  df-csb 3404  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-nul 3778  df-if 3940  df-pw 4013  df-sn 4029  df-pr 4031  df-op 4035  df-uni 4271  df-br 4482  df-opab 4542  df-mpt 4543  df-id 4847  df-xp 4938  df-rel 4939  df-cnv 4940  df-co 4941  df-dm 4942  df-rn 4943  df-res 4944  df-ima 4945  df-pred 5487  df-iota 5653  df-fun 5691  df-fn 5692  df-f 5693  df-f1 5694  df-fo 5695  df-f1o 5696  df-fv 5697  df-ov 6428  df-oprab 6429  df-mpt2 6430  df-wrecs 7167  df-recs 7229  df-rdg 7267  df-seq 12529  df-gsum 15831
This theorem is referenced by:  gsumval  17007  gsumpropd  17008  gsumpropd2lem  17009
  Copyright terms: Public domain W3C validator