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

Theorem gsumvalx 18358
Description: Expand out the substitutions in df-gsum 17151. (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 17151 . . 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 768 . . . . . . . 8 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → 𝑤 = 𝐺)
43fveq2d 6775 . . . . . . 7 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → (Base‘𝑤) = (Base‘𝐺))
5 gsumval.b . . . . . . 7 𝐵 = (Base‘𝐺)
64, 5eqtr4di 2798 . . . . . 6 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → (Base‘𝑤) = 𝐵)
73fveq2d 6775 . . . . . . . . . . 11 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → (+g𝑤) = (+g𝐺))
8 gsumval.p . . . . . . . . . . 11 + = (+g𝐺)
97, 8eqtr4di 2798 . . . . . . . . . 10 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → (+g𝑤) = + )
109oveqd 7288 . . . . . . . . 9 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → (𝑥(+g𝑤)𝑦) = (𝑥 + 𝑦))
1110eqeq1d 2742 . . . . . . . 8 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → ((𝑥(+g𝑤)𝑦) = 𝑦 ↔ (𝑥 + 𝑦) = 𝑦))
129oveqd 7288 . . . . . . . . 9 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → (𝑦(+g𝑤)𝑥) = (𝑦 + 𝑥))
1312eqeq1d 2742 . . . . . . . 8 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → ((𝑦(+g𝑤)𝑥) = 𝑦 ↔ (𝑦 + 𝑥) = 𝑦))
1411, 13anbi12d 631 . . . . . . 7 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → (((𝑥(+g𝑤)𝑦) = 𝑦 ∧ (𝑦(+g𝑤)𝑥) = 𝑦) ↔ ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)))
156, 14raleqbidv 3335 . . . . . 6 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → (∀𝑦 ∈ (Base‘𝑤)((𝑥(+g𝑤)𝑦) = 𝑦 ∧ (𝑦(+g𝑤)𝑥) = 𝑦) ↔ ∀𝑦𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)))
166, 15rabeqbidv 3419 . . . . 5 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → {𝑥 ∈ (Base‘𝑤) ∣ ∀𝑦 ∈ (Base‘𝑤)((𝑥(+g𝑤)𝑦) = 𝑦 ∧ (𝑦(+g𝑤)𝑥) = 𝑦)} = {𝑥𝐵 ∣ ∀𝑦𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)})
17 gsumval.o . . . . . 6 𝑂 = {𝑠𝐵 ∣ ∀𝑡𝐵 ((𝑠 + 𝑡) = 𝑡 ∧ (𝑡 + 𝑠) = 𝑡)}
18 oveq2 7279 . . . . . . . . . . 11 (𝑡 = 𝑦 → (𝑠 + 𝑡) = (𝑠 + 𝑦))
19 id 22 . . . . . . . . . . 11 (𝑡 = 𝑦𝑡 = 𝑦)
2018, 19eqeq12d 2756 . . . . . . . . . 10 (𝑡 = 𝑦 → ((𝑠 + 𝑡) = 𝑡 ↔ (𝑠 + 𝑦) = 𝑦))
21 oveq1 7278 . . . . . . . . . . 11 (𝑡 = 𝑦 → (𝑡 + 𝑠) = (𝑦 + 𝑠))
2221, 19eqeq12d 2756 . . . . . . . . . 10 (𝑡 = 𝑦 → ((𝑡 + 𝑠) = 𝑡 ↔ (𝑦 + 𝑠) = 𝑦))
2320, 22anbi12d 631 . . . . . . . . 9 (𝑡 = 𝑦 → (((𝑠 + 𝑡) = 𝑡 ∧ (𝑡 + 𝑠) = 𝑡) ↔ ((𝑠 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑠) = 𝑦)))
2423cbvralvw 3381 . . . . . . . 8 (∀𝑡𝐵 ((𝑠 + 𝑡) = 𝑡 ∧ (𝑡 + 𝑠) = 𝑡) ↔ ∀𝑦𝐵 ((𝑠 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑠) = 𝑦))
25 oveq1 7278 . . . . . . . . . 10 (𝑠 = 𝑥 → (𝑠 + 𝑦) = (𝑥 + 𝑦))
2625eqeq1d 2742 . . . . . . . . 9 (𝑠 = 𝑥 → ((𝑠 + 𝑦) = 𝑦 ↔ (𝑥 + 𝑦) = 𝑦))
2726ovanraleqv 7295 . . . . . . . 8 (𝑠 = 𝑥 → (∀𝑦𝐵 ((𝑠 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑠) = 𝑦) ↔ ∀𝑦𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)))
2824, 27syl5bb 283 . . . . . . 7 (𝑠 = 𝑥 → (∀𝑡𝐵 ((𝑠 + 𝑡) = 𝑡 ∧ (𝑡 + 𝑠) = 𝑡) ↔ ∀𝑦𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)))
2928cbvrabv 3425 . . . . . 6 {𝑠𝐵 ∣ ∀𝑡𝐵 ((𝑠 + 𝑡) = 𝑡 ∧ (𝑡 + 𝑠) = 𝑡)} = {𝑥𝐵 ∣ ∀𝑦𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)}
3017, 29eqtri 2768 . . . . 5 𝑂 = {𝑥𝐵 ∣ ∀𝑦𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)}
3116, 30eqtr4di 2798 . . . 4 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → {𝑥 ∈ (Base‘𝑤) ∣ ∀𝑦 ∈ (Base‘𝑤)((𝑥(+g𝑤)𝑦) = 𝑦 ∧ (𝑦(+g𝑤)𝑥) = 𝑦)} = 𝑂)
3231csbeq1d 3841 . . 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 6785 . . . . . 6 𝐵 ∈ V
3417, 33rabex2 5262 . . . . 5 𝑂 ∈ V
3534a1i 11 . . . 4 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → 𝑂 ∈ V)
36 simplrr 775 . . . . . . 7 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → 𝑔 = 𝐹)
3736rneqd 5846 . . . . . 6 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → ran 𝑔 = ran 𝐹)
38 simpr 485 . . . . . 6 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → 𝑜 = 𝑂)
3937, 38sseq12d 3959 . . . . 5 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (ran 𝑔𝑜 ↔ ran 𝐹𝑂))
403adantr 481 . . . . . . 7 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → 𝑤 = 𝐺)
4140fveq2d 6775 . . . . . 6 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (0g𝑤) = (0g𝐺))
42 gsumval.z . . . . . 6 0 = (0g𝐺)
4341, 42eqtr4di 2798 . . . . 5 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (0g𝑤) = 0 )
4436dmeqd 5813 . . . . . . . 8 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → dom 𝑔 = dom 𝐹)
45 gsumvalx.a . . . . . . . . 9 (𝜑 → dom 𝐹 = 𝐴)
4645ad2antrr 723 . . . . . . . 8 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → dom 𝐹 = 𝐴)
4744, 46eqtrd 2780 . . . . . . 7 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → dom 𝑔 = 𝐴)
4847eleq1d 2825 . . . . . 6 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (dom 𝑔 ∈ ran ... ↔ 𝐴 ∈ ran ...))
4947eqeq1d 2742 . . . . . . . . . 10 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (dom 𝑔 = (𝑚...𝑛) ↔ 𝐴 = (𝑚...𝑛)))
509adantr 481 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (+g𝑤) = + )
5150seqeq2d 13726 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → seq𝑚((+g𝑤), 𝑔) = seq𝑚( + , 𝑔))
5236seqeq3d 13727 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → seq𝑚( + , 𝑔) = seq𝑚( + , 𝐹))
5351, 52eqtrd 2780 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → seq𝑚((+g𝑤), 𝑔) = seq𝑚( + , 𝐹))
5453fveq1d 6773 . . . . . . . . . . 11 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (seq𝑚((+g𝑤), 𝑔)‘𝑛) = (seq𝑚( + , 𝐹)‘𝑛))
5554eqeq2d 2751 . . . . . . . . . 10 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (𝑥 = (seq𝑚((+g𝑤), 𝑔)‘𝑛) ↔ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛)))
5649, 55anbi12d 631 . . . . . . . . 9 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → ((dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝑤), 𝑔)‘𝑛)) ↔ (𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))))
5756rexbidv 3228 . . . . . . . 8 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (∃𝑛 ∈ (ℤ𝑚)(dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝑤), 𝑔)‘𝑛)) ↔ ∃𝑛 ∈ (ℤ𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))))
5857exbidv 1928 . . . . . . 7 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (∃𝑚𝑛 ∈ (ℤ𝑚)(dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝑤), 𝑔)‘𝑛)) ↔ ∃𝑚𝑛 ∈ (ℤ𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))))
5958iotabidv 6416 . . . . . 6 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝑤), 𝑔)‘𝑛))) = (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))))
6038difeq2d 4062 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (V ∖ 𝑜) = (V ∖ 𝑂))
6160imaeq2d 5968 . . . . . . . . . . 11 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (𝐹 “ (V ∖ 𝑜)) = (𝐹 “ (V ∖ 𝑂)))
6236cnveqd 5783 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → 𝑔 = 𝐹)
6362imaeq1d 5967 . . . . . . . . . . 11 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (𝑔 “ (V ∖ 𝑜)) = (𝐹 “ (V ∖ 𝑜)))
64 gsumval.w . . . . . . . . . . . 12 (𝜑𝑊 = (𝐹 “ (V ∖ 𝑂)))
6564ad2antrr 723 . . . . . . . . . . 11 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → 𝑊 = (𝐹 “ (V ∖ 𝑂)))
6661, 63, 653eqtr4d 2790 . . . . . . . . . 10 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (𝑔 “ (V ∖ 𝑜)) = 𝑊)
6766sbceq1d 3725 . . . . . . . . 9 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → ([(𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(♯‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑔𝑓))‘(♯‘𝑦))) ↔ [𝑊 / 𝑦](𝑓:(1...(♯‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑔𝑓))‘(♯‘𝑦)))))
68 gsumvalx.f . . . . . . . . . . . . 13 (𝜑𝐹𝑋)
69 cnvexg 7765 . . . . . . . . . . . . 13 (𝐹𝑋𝐹 ∈ V)
70 imaexg 7756 . . . . . . . . . . . . 13 (𝐹 ∈ V → (𝐹 “ (V ∖ 𝑂)) ∈ V)
7168, 69, 703syl 18 . . . . . . . . . . . 12 (𝜑 → (𝐹 “ (V ∖ 𝑂)) ∈ V)
7264, 71eqeltrd 2841 . . . . . . . . . . 11 (𝜑𝑊 ∈ V)
7372ad2antrr 723 . . . . . . . . . 10 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → 𝑊 ∈ V)
74 fveq2 6771 . . . . . . . . . . . . . . 15 (𝑦 = 𝑊 → (♯‘𝑦) = (♯‘𝑊))
7574adantl 482 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (♯‘𝑦) = (♯‘𝑊))
7675oveq2d 7287 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (1...(♯‘𝑦)) = (1...(♯‘𝑊)))
7776f1oeq2d 6710 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (𝑓:(1...(♯‘𝑦))–1-1-onto𝑦𝑓:(1...(♯‘𝑊))–1-1-onto𝑦))
78 f1oeq3 6704 . . . . . . . . . . . . 13 (𝑦 = 𝑊 → (𝑓:(1...(♯‘𝑊))–1-1-onto𝑦𝑓:(1...(♯‘𝑊))–1-1-onto𝑊))
7978adantl 482 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (𝑓:(1...(♯‘𝑊))–1-1-onto𝑦𝑓:(1...(♯‘𝑊))–1-1-onto𝑊))
8077, 79bitrd 278 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (𝑓:(1...(♯‘𝑦))–1-1-onto𝑦𝑓:(1...(♯‘𝑊))–1-1-onto𝑊))
8150seqeq2d 13726 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → seq1((+g𝑤), (𝑔𝑓)) = seq1( + , (𝑔𝑓)))
8236coeq1d 5769 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (𝑔𝑓) = (𝐹𝑓))
8382seqeq3d 13727 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → seq1( + , (𝑔𝑓)) = seq1( + , (𝐹𝑓)))
8481, 83eqtrd 2780 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → seq1((+g𝑤), (𝑔𝑓)) = seq1( + , (𝐹𝑓)))
8584adantr 481 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → seq1((+g𝑤), (𝑔𝑓)) = seq1( + , (𝐹𝑓)))
8685, 75fveq12d 6778 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (seq1((+g𝑤), (𝑔𝑓))‘(♯‘𝑦)) = (seq1( + , (𝐹𝑓))‘(♯‘𝑊)))
8786eqeq2d 2751 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (𝑥 = (seq1((+g𝑤), (𝑔𝑓))‘(♯‘𝑦)) ↔ 𝑥 = (seq1( + , (𝐹𝑓))‘(♯‘𝑊))))
8880, 87anbi12d 631 . . . . . . . . . 10 ((((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → ((𝑓:(1...(♯‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑔𝑓))‘(♯‘𝑦))) ↔ (𝑓:(1...(♯‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(♯‘𝑊)))))
8973, 88sbcied 3765 . . . . . . . . 9 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → ([𝑊 / 𝑦](𝑓:(1...(♯‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑔𝑓))‘(♯‘𝑦))) ↔ (𝑓:(1...(♯‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(♯‘𝑊)))))
9067, 89bitrd 278 . . . . . . . 8 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → ([(𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(♯‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑔𝑓))‘(♯‘𝑦))) ↔ (𝑓:(1...(♯‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(♯‘𝑊)))))
9190exbidv 1928 . . . . . . 7 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (∃𝑓[(𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(♯‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑔𝑓))‘(♯‘𝑦))) ↔ ∃𝑓(𝑓:(1...(♯‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(♯‘𝑊)))))
9291iotabidv 6416 . . . . . 6 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (℩𝑥𝑓[(𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(♯‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑔𝑓))‘(♯‘𝑦)))) = (℩𝑥𝑓(𝑓:(1...(♯‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(♯‘𝑊)))))
9348, 59, 92ifbieq12d 4493 . . . . 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 4493 . . . 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 3875 . . 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 2780 . 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 3451 . 2 (𝜑𝐺 ∈ V)
9968elexd 3451 . 2 (𝜑𝐹 ∈ V)
10042fvexi 6785 . . . 4 0 ∈ V
101 iotaex 6412 . . . . 5 (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))) ∈ V
102 iotaex 6412 . . . . 5 (℩𝑥𝑓(𝑓:(1...(♯‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(♯‘𝑊)))) ∈ V
103101, 102ifex 4515 . . . 4 if(𝐴 ∈ ran ..., (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑥𝑓(𝑓:(1...(♯‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(♯‘𝑊))))) ∈ V
104100, 103ifex 4515 . . 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 7419 1 (𝜑 → (𝐺 Σg 𝐹) = if(ran 𝐹𝑂, 0 , if(𝐴 ∈ ran ..., (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑥𝑓(𝑓:(1...(♯‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(♯‘𝑊)))))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1542  wex 1786  wcel 2110  wral 3066  wrex 3067  {crab 3070  Vcvv 3431  [wsbc 3720  csb 3837  cdif 3889  wss 3892  ifcif 4465  ccnv 5589  dom cdm 5590  ran crn 5591  cima 5593  ccom 5594  cio 6388  1-1-ontowf1o 6431  cfv 6432  (class class class)co 7271  cmpo 7273  1c1 10873  cuz 12581  ...cfz 13238  seqcseq 13719  chash 14042  Basecbs 16910  +gcplusg 16960  0gc0g 17148   Σg cgsu 17149
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pow 5292  ax-pr 5356  ax-un 7582
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ral 3071  df-rex 3072  df-rab 3075  df-v 3433  df-sbc 3721  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5163  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-pred 6201  df-iota 6390  df-fun 6434  df-fn 6435  df-f 6436  df-f1 6437  df-fo 6438  df-f1o 6439  df-fv 6440  df-ov 7274  df-oprab 7275  df-mpo 7276  df-frecs 8088  df-wrecs 8119  df-recs 8193  df-rdg 8232  df-seq 13720  df-gsum 17151
This theorem is referenced by:  gsumval  18359  gsumpropd  18360  gsumpropd2lem  18361
  Copyright terms: Public domain W3C validator