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

Theorem gsumvalx 17886
Description: Expand out the substitutions in df-gsum 16716. (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 16716 . . 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 770 . . . . . . . 8 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → 𝑤 = 𝐺)
43fveq2d 6665 . . . . . . 7 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → (Base‘𝑤) = (Base‘𝐺))
5 gsumval.b . . . . . . 7 𝐵 = (Base‘𝐺)
64, 5syl6eqr 2877 . . . . . 6 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → (Base‘𝑤) = 𝐵)
73fveq2d 6665 . . . . . . . . . . 11 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → (+g𝑤) = (+g𝐺))
8 gsumval.p . . . . . . . . . . 11 + = (+g𝐺)
97, 8syl6eqr 2877 . . . . . . . . . 10 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → (+g𝑤) = + )
109oveqd 7166 . . . . . . . . 9 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → (𝑥(+g𝑤)𝑦) = (𝑥 + 𝑦))
1110eqeq1d 2826 . . . . . . . 8 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → ((𝑥(+g𝑤)𝑦) = 𝑦 ↔ (𝑥 + 𝑦) = 𝑦))
129oveqd 7166 . . . . . . . . 9 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → (𝑦(+g𝑤)𝑥) = (𝑦 + 𝑥))
1312eqeq1d 2826 . . . . . . . 8 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → ((𝑦(+g𝑤)𝑥) = 𝑦 ↔ (𝑦 + 𝑥) = 𝑦))
1411, 13anbi12d 633 . . . . . . 7 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → (((𝑥(+g𝑤)𝑦) = 𝑦 ∧ (𝑦(+g𝑤)𝑥) = 𝑦) ↔ ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)))
156, 14raleqbidv 3392 . . . . . 6 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → (∀𝑦 ∈ (Base‘𝑤)((𝑥(+g𝑤)𝑦) = 𝑦 ∧ (𝑦(+g𝑤)𝑥) = 𝑦) ↔ ∀𝑦𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)))
166, 15rabeqbidv 3471 . . . . 5 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → {𝑥 ∈ (Base‘𝑤) ∣ ∀𝑦 ∈ (Base‘𝑤)((𝑥(+g𝑤)𝑦) = 𝑦 ∧ (𝑦(+g𝑤)𝑥) = 𝑦)} = {𝑥𝐵 ∣ ∀𝑦𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)})
17 gsumval.o . . . . . 6 𝑂 = {𝑠𝐵 ∣ ∀𝑡𝐵 ((𝑠 + 𝑡) = 𝑡 ∧ (𝑡 + 𝑠) = 𝑡)}
18 oveq2 7157 . . . . . . . . . . 11 (𝑡 = 𝑦 → (𝑠 + 𝑡) = (𝑠 + 𝑦))
19 id 22 . . . . . . . . . . 11 (𝑡 = 𝑦𝑡 = 𝑦)
2018, 19eqeq12d 2840 . . . . . . . . . 10 (𝑡 = 𝑦 → ((𝑠 + 𝑡) = 𝑡 ↔ (𝑠 + 𝑦) = 𝑦))
21 oveq1 7156 . . . . . . . . . . 11 (𝑡 = 𝑦 → (𝑡 + 𝑠) = (𝑦 + 𝑠))
2221, 19eqeq12d 2840 . . . . . . . . . 10 (𝑡 = 𝑦 → ((𝑡 + 𝑠) = 𝑡 ↔ (𝑦 + 𝑠) = 𝑦))
2320, 22anbi12d 633 . . . . . . . . 9 (𝑡 = 𝑦 → (((𝑠 + 𝑡) = 𝑡 ∧ (𝑡 + 𝑠) = 𝑡) ↔ ((𝑠 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑠) = 𝑦)))
2423cbvralvw 3434 . . . . . . . 8 (∀𝑡𝐵 ((𝑠 + 𝑡) = 𝑡 ∧ (𝑡 + 𝑠) = 𝑡) ↔ ∀𝑦𝐵 ((𝑠 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑠) = 𝑦))
25 oveq1 7156 . . . . . . . . . 10 (𝑠 = 𝑥 → (𝑠 + 𝑦) = (𝑥 + 𝑦))
2625eqeq1d 2826 . . . . . . . . 9 (𝑠 = 𝑥 → ((𝑠 + 𝑦) = 𝑦 ↔ (𝑥 + 𝑦) = 𝑦))
2726ovanraleqv 7173 . . . . . . . 8 (𝑠 = 𝑥 → (∀𝑦𝐵 ((𝑠 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑠) = 𝑦) ↔ ∀𝑦𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)))
2824, 27syl5bb 286 . . . . . . 7 (𝑠 = 𝑥 → (∀𝑡𝐵 ((𝑠 + 𝑡) = 𝑡 ∧ (𝑡 + 𝑠) = 𝑡) ↔ ∀𝑦𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)))
2928cbvrabv 3477 . . . . . 6 {𝑠𝐵 ∣ ∀𝑡𝐵 ((𝑠 + 𝑡) = 𝑡 ∧ (𝑡 + 𝑠) = 𝑡)} = {𝑥𝐵 ∣ ∀𝑦𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)}
3017, 29eqtri 2847 . . . . 5 𝑂 = {𝑥𝐵 ∣ ∀𝑦𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)}
3116, 30syl6eqr 2877 . . . 4 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → {𝑥 ∈ (Base‘𝑤) ∣ ∀𝑦 ∈ (Base‘𝑤)((𝑥(+g𝑤)𝑦) = 𝑦 ∧ (𝑦(+g𝑤)𝑥) = 𝑦)} = 𝑂)
3231csbeq1d 3870 . . 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𝑤), (𝑔𝑓))‘(♯‘𝑦)))))))
335fvexi 6675 . . . . . 6 𝐵 ∈ V
3417, 33rabex2 5223 . . . . 5 𝑂 ∈ V
3534a1i 11 . . . 4 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → 𝑂 ∈ V)
36 simplrr 777 . . . . . . 7 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → 𝑔 = 𝐹)
3736rneqd 5795 . . . . . 6 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → ran 𝑔 = ran 𝐹)
38 simpr 488 . . . . . 6 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → 𝑜 = 𝑂)
3937, 38sseq12d 3986 . . . . 5 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (ran 𝑔𝑜 ↔ ran 𝐹𝑂))
403adantr 484 . . . . . . 7 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → 𝑤 = 𝐺)
4140fveq2d 6665 . . . . . 6 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (0g𝑤) = (0g𝐺))
42 gsumval.z . . . . . 6 0 = (0g𝐺)
4341, 42syl6eqr 2877 . . . . 5 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (0g𝑤) = 0 )
4436dmeqd 5761 . . . . . . . 8 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → dom 𝑔 = dom 𝐹)
45 gsumvalx.a . . . . . . . . 9 (𝜑 → dom 𝐹 = 𝐴)
4645ad2antrr 725 . . . . . . . 8 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → dom 𝐹 = 𝐴)
4744, 46eqtrd 2859 . . . . . . 7 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → dom 𝑔 = 𝐴)
4847eleq1d 2900 . . . . . 6 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (dom 𝑔 ∈ ran ... ↔ 𝐴 ∈ ran ...))
4947eqeq1d 2826 . . . . . . . . . 10 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (dom 𝑔 = (𝑚...𝑛) ↔ 𝐴 = (𝑚...𝑛)))
509adantr 484 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (+g𝑤) = + )
5150seqeq2d 13380 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → seq𝑚((+g𝑤), 𝑔) = seq𝑚( + , 𝑔))
5236seqeq3d 13381 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → seq𝑚( + , 𝑔) = seq𝑚( + , 𝐹))
5351, 52eqtrd 2859 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → seq𝑚((+g𝑤), 𝑔) = seq𝑚( + , 𝐹))
5453fveq1d 6663 . . . . . . . . . . 11 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (seq𝑚((+g𝑤), 𝑔)‘𝑛) = (seq𝑚( + , 𝐹)‘𝑛))
5554eqeq2d 2835 . . . . . . . . . 10 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (𝑥 = (seq𝑚((+g𝑤), 𝑔)‘𝑛) ↔ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛)))
5649, 55anbi12d 633 . . . . . . . . 9 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → ((dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝑤), 𝑔)‘𝑛)) ↔ (𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))))
5756rexbidv 3289 . . . . . . . 8 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (∃𝑛 ∈ (ℤ𝑚)(dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝑤), 𝑔)‘𝑛)) ↔ ∃𝑛 ∈ (ℤ𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))))
5857exbidv 1923 . . . . . . 7 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (∃𝑚𝑛 ∈ (ℤ𝑚)(dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝑤), 𝑔)‘𝑛)) ↔ ∃𝑚𝑛 ∈ (ℤ𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))))
5958iotabidv 6327 . . . . . 6 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝑤), 𝑔)‘𝑛))) = (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))))
6038difeq2d 4085 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (V ∖ 𝑜) = (V ∖ 𝑂))
6160imaeq2d 5916 . . . . . . . . . . 11 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (𝐹 “ (V ∖ 𝑜)) = (𝐹 “ (V ∖ 𝑂)))
6236cnveqd 5733 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → 𝑔 = 𝐹)
6362imaeq1d 5915 . . . . . . . . . . 11 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (𝑔 “ (V ∖ 𝑜)) = (𝐹 “ (V ∖ 𝑜)))
64 gsumval.w . . . . . . . . . . . 12 (𝜑𝑊 = (𝐹 “ (V ∖ 𝑂)))
6564ad2antrr 725 . . . . . . . . . . 11 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → 𝑊 = (𝐹 “ (V ∖ 𝑂)))
6661, 63, 653eqtr4d 2869 . . . . . . . . . 10 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (𝑔 “ (V ∖ 𝑜)) = 𝑊)
6766sbceq1d 3763 . . . . . . . . 9 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → ([(𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(♯‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑔𝑓))‘(♯‘𝑦))) ↔ [𝑊 / 𝑦](𝑓:(1...(♯‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑔𝑓))‘(♯‘𝑦)))))
68 gsumvalx.f . . . . . . . . . . . . 13 (𝜑𝐹𝑋)
69 cnvexg 7624 . . . . . . . . . . . . 13 (𝐹𝑋𝐹 ∈ V)
70 imaexg 7615 . . . . . . . . . . . . 13 (𝐹 ∈ V → (𝐹 “ (V ∖ 𝑂)) ∈ V)
7168, 69, 703syl 18 . . . . . . . . . . . 12 (𝜑 → (𝐹 “ (V ∖ 𝑂)) ∈ V)
7264, 71eqeltrd 2916 . . . . . . . . . . 11 (𝜑𝑊 ∈ V)
7372ad2antrr 725 . . . . . . . . . 10 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → 𝑊 ∈ V)
74 fveq2 6661 . . . . . . . . . . . . . . 15 (𝑦 = 𝑊 → (♯‘𝑦) = (♯‘𝑊))
7574adantl 485 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (♯‘𝑦) = (♯‘𝑊))
7675oveq2d 7165 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (1...(♯‘𝑦)) = (1...(♯‘𝑊)))
7776f1oeq2d 6602 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (𝑓:(1...(♯‘𝑦))–1-1-onto𝑦𝑓:(1...(♯‘𝑊))–1-1-onto𝑦))
78 f1oeq3 6597 . . . . . . . . . . . . 13 (𝑦 = 𝑊 → (𝑓:(1...(♯‘𝑊))–1-1-onto𝑦𝑓:(1...(♯‘𝑊))–1-1-onto𝑊))
7978adantl 485 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (𝑓:(1...(♯‘𝑊))–1-1-onto𝑦𝑓:(1...(♯‘𝑊))–1-1-onto𝑊))
8077, 79bitrd 282 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (𝑓:(1...(♯‘𝑦))–1-1-onto𝑦𝑓:(1...(♯‘𝑊))–1-1-onto𝑊))
8150seqeq2d 13380 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → seq1((+g𝑤), (𝑔𝑓)) = seq1( + , (𝑔𝑓)))
8236coeq1d 5719 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (𝑔𝑓) = (𝐹𝑓))
8382seqeq3d 13381 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → seq1( + , (𝑔𝑓)) = seq1( + , (𝐹𝑓)))
8481, 83eqtrd 2859 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → seq1((+g𝑤), (𝑔𝑓)) = seq1( + , (𝐹𝑓)))
8584adantr 484 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → seq1((+g𝑤), (𝑔𝑓)) = seq1( + , (𝐹𝑓)))
8685, 75fveq12d 6668 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (seq1((+g𝑤), (𝑔𝑓))‘(♯‘𝑦)) = (seq1( + , (𝐹𝑓))‘(♯‘𝑊)))
8786eqeq2d 2835 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (𝑥 = (seq1((+g𝑤), (𝑔𝑓))‘(♯‘𝑦)) ↔ 𝑥 = (seq1( + , (𝐹𝑓))‘(♯‘𝑊))))
8880, 87anbi12d 633 . . . . . . . . . 10 ((((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → ((𝑓:(1...(♯‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑔𝑓))‘(♯‘𝑦))) ↔ (𝑓:(1...(♯‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(♯‘𝑊)))))
8973, 88sbcied 3800 . . . . . . . . 9 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → ([𝑊 / 𝑦](𝑓:(1...(♯‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑔𝑓))‘(♯‘𝑦))) ↔ (𝑓:(1...(♯‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(♯‘𝑊)))))
9067, 89bitrd 282 . . . . . . . 8 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → ([(𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(♯‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑔𝑓))‘(♯‘𝑦))) ↔ (𝑓:(1...(♯‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(♯‘𝑊)))))
9190exbidv 1923 . . . . . . 7 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (∃𝑓[(𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(♯‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑔𝑓))‘(♯‘𝑦))) ↔ ∃𝑓(𝑓:(1...(♯‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(♯‘𝑊)))))
9291iotabidv 6327 . . . . . 6 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (℩𝑥𝑓[(𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(♯‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑔𝑓))‘(♯‘𝑦)))) = (℩𝑥𝑓(𝑓:(1...(♯‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(♯‘𝑊)))))
9348, 59, 92ifbieq12d 4477 . . . . 5 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → if(dom 𝑔 ∈ ran ..., (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝑤), 𝑔)‘𝑛))), (℩𝑥𝑓[(𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(♯‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑔𝑓))‘(♯‘𝑦))))) = if(𝐴 ∈ ran ..., (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑥𝑓(𝑓:(1...(♯‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(♯‘𝑊))))))
9439, 43, 93ifbieq12d 4477 . . . 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( + , (𝐹𝑓))‘(♯‘𝑊)))))))
9535, 94csbied 3902 . . 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( + , (𝐹𝑓))‘(♯‘𝑊)))))))
9632, 95eqtrd 2859 . 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( + , (𝐹𝑓))‘(♯‘𝑊)))))))
97 gsumval.g . . 3 (𝜑𝐺𝑉)
9897elexd 3500 . 2 (𝜑𝐺 ∈ V)
9968elexd 3500 . 2 (𝜑𝐹 ∈ V)
10042fvexi 6675 . . . 4 0 ∈ V
101 iotaex 6323 . . . . 5 (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))) ∈ V
102 iotaex 6323 . . . . 5 (℩𝑥𝑓(𝑓:(1...(♯‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(♯‘𝑊)))) ∈ V
103101, 102ifex 4498 . . . 4 if(𝐴 ∈ ran ..., (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑥𝑓(𝑓:(1...(♯‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(♯‘𝑊))))) ∈ V
104100, 103ifex 4498 . . 3 if(ran 𝐹𝑂, 0 , if(𝐴 ∈ ran ..., (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑥𝑓(𝑓:(1...(♯‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(♯‘𝑊)))))) ∈ V
105104a1i 11 . 2 (𝜑 → if(ran 𝐹𝑂, 0 , if(𝐴 ∈ ran ..., (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑥𝑓(𝑓:(1...(♯‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(♯‘𝑊)))))) ∈ V)
1062, 96, 98, 99, 105ovmpod 7295 1 (𝜑 → (𝐺 Σg 𝐹) = if(ran 𝐹𝑂, 0 , if(𝐴 ∈ ran ..., (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑥𝑓(𝑓:(1...(♯‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(♯‘𝑊)))))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1538  wex 1781  wcel 2115  wral 3133  wrex 3134  {crab 3137  Vcvv 3480  [wsbc 3758  csb 3866  cdif 3916  wss 3919  ifcif 4450  ccnv 5541  dom cdm 5542  ran crn 5543  cima 5545  ccom 5546  cio 6300  1-1-ontowf1o 6342  cfv 6343  (class class class)co 7149  cmpo 7151  1c1 10536  cuz 12240  ...cfz 12894  seqcseq 13373  chash 13695  Basecbs 16483  +gcplusg 16565  0gc0g 16713   Σg cgsu 16714
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317  ax-un 7455
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ral 3138  df-rex 3139  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-op 4557  df-uni 4825  df-br 5053  df-opab 5115  df-mpt 5133  df-id 5447  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-pred 6135  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350  df-fv 6351  df-ov 7152  df-oprab 7153  df-mpo 7154  df-wrecs 7943  df-recs 8004  df-rdg 8042  df-seq 13374  df-gsum 16716
This theorem is referenced by:  gsumval  17887  gsumpropd  17888  gsumpropd2lem  17889
  Copyright terms: Public domain W3C validator