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

Theorem gsumvalx 17660
Description: Expand out the substitutions in df-gsum 16493. (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 16493 . . 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 761 . . . . . . . 8 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → 𝑤 = 𝐺)
43fveq2d 6452 . . . . . . 7 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → (Base‘𝑤) = (Base‘𝐺))
5 gsumval.b . . . . . . 7 𝐵 = (Base‘𝐺)
64, 5syl6eqr 2832 . . . . . 6 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → (Base‘𝑤) = 𝐵)
73fveq2d 6452 . . . . . . . . . . 11 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → (+g𝑤) = (+g𝐺))
8 gsumval.p . . . . . . . . . . 11 + = (+g𝐺)
97, 8syl6eqr 2832 . . . . . . . . . 10 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → (+g𝑤) = + )
109oveqd 6941 . . . . . . . . 9 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → (𝑥(+g𝑤)𝑦) = (𝑥 + 𝑦))
1110eqeq1d 2780 . . . . . . . 8 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → ((𝑥(+g𝑤)𝑦) = 𝑦 ↔ (𝑥 + 𝑦) = 𝑦))
129oveqd 6941 . . . . . . . . 9 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → (𝑦(+g𝑤)𝑥) = (𝑦 + 𝑥))
1312eqeq1d 2780 . . . . . . . 8 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → ((𝑦(+g𝑤)𝑥) = 𝑦 ↔ (𝑦 + 𝑥) = 𝑦))
1411, 13anbi12d 624 . . . . . . 7 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → (((𝑥(+g𝑤)𝑦) = 𝑦 ∧ (𝑦(+g𝑤)𝑥) = 𝑦) ↔ ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)))
156, 14raleqbidv 3326 . . . . . 6 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → (∀𝑦 ∈ (Base‘𝑤)((𝑥(+g𝑤)𝑦) = 𝑦 ∧ (𝑦(+g𝑤)𝑥) = 𝑦) ↔ ∀𝑦𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)))
166, 15rabeqbidv 3392 . . . . 5 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → {𝑥 ∈ (Base‘𝑤) ∣ ∀𝑦 ∈ (Base‘𝑤)((𝑥(+g𝑤)𝑦) = 𝑦 ∧ (𝑦(+g𝑤)𝑥) = 𝑦)} = {𝑥𝐵 ∣ ∀𝑦𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)})
17 gsumval.o . . . . . 6 𝑂 = {𝑠𝐵 ∣ ∀𝑡𝐵 ((𝑠 + 𝑡) = 𝑡 ∧ (𝑡 + 𝑠) = 𝑡)}
18 oveq2 6932 . . . . . . . . . . 11 (𝑡 = 𝑦 → (𝑠 + 𝑡) = (𝑠 + 𝑦))
19 id 22 . . . . . . . . . . 11 (𝑡 = 𝑦𝑡 = 𝑦)
2018, 19eqeq12d 2793 . . . . . . . . . 10 (𝑡 = 𝑦 → ((𝑠 + 𝑡) = 𝑡 ↔ (𝑠 + 𝑦) = 𝑦))
21 oveq1 6931 . . . . . . . . . . 11 (𝑡 = 𝑦 → (𝑡 + 𝑠) = (𝑦 + 𝑠))
2221, 19eqeq12d 2793 . . . . . . . . . 10 (𝑡 = 𝑦 → ((𝑡 + 𝑠) = 𝑡 ↔ (𝑦 + 𝑠) = 𝑦))
2320, 22anbi12d 624 . . . . . . . . 9 (𝑡 = 𝑦 → (((𝑠 + 𝑡) = 𝑡 ∧ (𝑡 + 𝑠) = 𝑡) ↔ ((𝑠 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑠) = 𝑦)))
2423cbvralv 3367 . . . . . . . 8 (∀𝑡𝐵 ((𝑠 + 𝑡) = 𝑡 ∧ (𝑡 + 𝑠) = 𝑡) ↔ ∀𝑦𝐵 ((𝑠 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑠) = 𝑦))
25 oveq1 6931 . . . . . . . . . 10 (𝑠 = 𝑥 → (𝑠 + 𝑦) = (𝑥 + 𝑦))
2625eqeq1d 2780 . . . . . . . . 9 (𝑠 = 𝑥 → ((𝑠 + 𝑦) = 𝑦 ↔ (𝑥 + 𝑦) = 𝑦))
2726ovanraleqv 6948 . . . . . . . 8 (𝑠 = 𝑥 → (∀𝑦𝐵 ((𝑠 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑠) = 𝑦) ↔ ∀𝑦𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)))
2824, 27syl5bb 275 . . . . . . 7 (𝑠 = 𝑥 → (∀𝑡𝐵 ((𝑠 + 𝑡) = 𝑡 ∧ (𝑡 + 𝑠) = 𝑡) ↔ ∀𝑦𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)))
2928cbvrabv 3396 . . . . . 6 {𝑠𝐵 ∣ ∀𝑡𝐵 ((𝑠 + 𝑡) = 𝑡 ∧ (𝑡 + 𝑠) = 𝑡)} = {𝑥𝐵 ∣ ∀𝑦𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)}
3017, 29eqtri 2802 . . . . 5 𝑂 = {𝑥𝐵 ∣ ∀𝑦𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)}
3116, 30syl6eqr 2832 . . . 4 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → {𝑥 ∈ (Base‘𝑤) ∣ ∀𝑦 ∈ (Base‘𝑤)((𝑥(+g𝑤)𝑦) = 𝑦 ∧ (𝑦(+g𝑤)𝑥) = 𝑦)} = 𝑂)
3231csbeq1d 3758 . . 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 6462 . . . . . 6 𝐵 ∈ V
3417, 33rabex2 5053 . . . . 5 𝑂 ∈ V
3534a1i 11 . . . 4 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → 𝑂 ∈ V)
36 simplrr 768 . . . . . . 7 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → 𝑔 = 𝐹)
3736rneqd 5600 . . . . . 6 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → ran 𝑔 = ran 𝐹)
38 simpr 479 . . . . . 6 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → 𝑜 = 𝑂)
3937, 38sseq12d 3853 . . . . 5 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (ran 𝑔𝑜 ↔ ran 𝐹𝑂))
403adantr 474 . . . . . . 7 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → 𝑤 = 𝐺)
4140fveq2d 6452 . . . . . 6 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (0g𝑤) = (0g𝐺))
42 gsumval.z . . . . . 6 0 = (0g𝐺)
4341, 42syl6eqr 2832 . . . . 5 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (0g𝑤) = 0 )
4436dmeqd 5573 . . . . . . . 8 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → dom 𝑔 = dom 𝐹)
45 gsumvalx.a . . . . . . . . 9 (𝜑 → dom 𝐹 = 𝐴)
4645ad2antrr 716 . . . . . . . 8 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → dom 𝐹 = 𝐴)
4744, 46eqtrd 2814 . . . . . . 7 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → dom 𝑔 = 𝐴)
4847eleq1d 2844 . . . . . 6 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (dom 𝑔 ∈ ran ... ↔ 𝐴 ∈ ran ...))
4947eqeq1d 2780 . . . . . . . . . 10 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (dom 𝑔 = (𝑚...𝑛) ↔ 𝐴 = (𝑚...𝑛)))
509adantr 474 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (+g𝑤) = + )
5150seqeq2d 13130 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → seq𝑚((+g𝑤), 𝑔) = seq𝑚( + , 𝑔))
5236seqeq3d 13131 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → seq𝑚( + , 𝑔) = seq𝑚( + , 𝐹))
5351, 52eqtrd 2814 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → seq𝑚((+g𝑤), 𝑔) = seq𝑚( + , 𝐹))
5453fveq1d 6450 . . . . . . . . . . 11 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (seq𝑚((+g𝑤), 𝑔)‘𝑛) = (seq𝑚( + , 𝐹)‘𝑛))
5554eqeq2d 2788 . . . . . . . . . 10 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (𝑥 = (seq𝑚((+g𝑤), 𝑔)‘𝑛) ↔ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛)))
5649, 55anbi12d 624 . . . . . . . . 9 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → ((dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝑤), 𝑔)‘𝑛)) ↔ (𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))))
5756rexbidv 3237 . . . . . . . 8 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (∃𝑛 ∈ (ℤ𝑚)(dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝑤), 𝑔)‘𝑛)) ↔ ∃𝑛 ∈ (ℤ𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))))
5857exbidv 1964 . . . . . . 7 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (∃𝑚𝑛 ∈ (ℤ𝑚)(dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝑤), 𝑔)‘𝑛)) ↔ ∃𝑚𝑛 ∈ (ℤ𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))))
5958iotabidv 6122 . . . . . 6 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝑤), 𝑔)‘𝑛))) = (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))))
6038difeq2d 3951 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (V ∖ 𝑜) = (V ∖ 𝑂))
6160imaeq2d 5722 . . . . . . . . . . 11 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (𝐹 “ (V ∖ 𝑜)) = (𝐹 “ (V ∖ 𝑂)))
6236cnveqd 5545 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → 𝑔 = 𝐹)
6362imaeq1d 5721 . . . . . . . . . . 11 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (𝑔 “ (V ∖ 𝑜)) = (𝐹 “ (V ∖ 𝑜)))
64 gsumval.w . . . . . . . . . . . 12 (𝜑𝑊 = (𝐹 “ (V ∖ 𝑂)))
6564ad2antrr 716 . . . . . . . . . . 11 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → 𝑊 = (𝐹 “ (V ∖ 𝑂)))
6661, 63, 653eqtr4d 2824 . . . . . . . . . 10 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (𝑔 “ (V ∖ 𝑜)) = 𝑊)
6766sbceq1d 3657 . . . . . . . . 9 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → ([(𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(♯‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑔𝑓))‘(♯‘𝑦))) ↔ [𝑊 / 𝑦](𝑓:(1...(♯‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑔𝑓))‘(♯‘𝑦)))))
68 gsumvalx.f . . . . . . . . . . . . 13 (𝜑𝐹𝑋)
69 cnvexg 7393 . . . . . . . . . . . . 13 (𝐹𝑋𝐹 ∈ V)
70 imaexg 7384 . . . . . . . . . . . . 13 (𝐹 ∈ V → (𝐹 “ (V ∖ 𝑂)) ∈ V)
7168, 69, 703syl 18 . . . . . . . . . . . 12 (𝜑 → (𝐹 “ (V ∖ 𝑂)) ∈ V)
7264, 71eqeltrd 2859 . . . . . . . . . . 11 (𝜑𝑊 ∈ V)
7372ad2antrr 716 . . . . . . . . . 10 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → 𝑊 ∈ V)
74 fveq2 6448 . . . . . . . . . . . . . . 15 (𝑦 = 𝑊 → (♯‘𝑦) = (♯‘𝑊))
7574adantl 475 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (♯‘𝑦) = (♯‘𝑊))
7675oveq2d 6940 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (1...(♯‘𝑦)) = (1...(♯‘𝑊)))
7776f1oeq2d 6389 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (𝑓:(1...(♯‘𝑦))–1-1-onto𝑦𝑓:(1...(♯‘𝑊))–1-1-onto𝑦))
78 f1oeq3 6384 . . . . . . . . . . . . 13 (𝑦 = 𝑊 → (𝑓:(1...(♯‘𝑊))–1-1-onto𝑦𝑓:(1...(♯‘𝑊))–1-1-onto𝑊))
7978adantl 475 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (𝑓:(1...(♯‘𝑊))–1-1-onto𝑦𝑓:(1...(♯‘𝑊))–1-1-onto𝑊))
8077, 79bitrd 271 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (𝑓:(1...(♯‘𝑦))–1-1-onto𝑦𝑓:(1...(♯‘𝑊))–1-1-onto𝑊))
8150seqeq2d 13130 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → seq1((+g𝑤), (𝑔𝑓)) = seq1( + , (𝑔𝑓)))
8236coeq1d 5531 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (𝑔𝑓) = (𝐹𝑓))
8382seqeq3d 13131 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → seq1( + , (𝑔𝑓)) = seq1( + , (𝐹𝑓)))
8481, 83eqtrd 2814 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → seq1((+g𝑤), (𝑔𝑓)) = seq1( + , (𝐹𝑓)))
8584adantr 474 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → seq1((+g𝑤), (𝑔𝑓)) = seq1( + , (𝐹𝑓)))
8685, 75fveq12d 6455 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (seq1((+g𝑤), (𝑔𝑓))‘(♯‘𝑦)) = (seq1( + , (𝐹𝑓))‘(♯‘𝑊)))
8786eqeq2d 2788 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (𝑥 = (seq1((+g𝑤), (𝑔𝑓))‘(♯‘𝑦)) ↔ 𝑥 = (seq1( + , (𝐹𝑓))‘(♯‘𝑊))))
8880, 87anbi12d 624 . . . . . . . . . 10 ((((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → ((𝑓:(1...(♯‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑔𝑓))‘(♯‘𝑦))) ↔ (𝑓:(1...(♯‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(♯‘𝑊)))))
8973, 88sbcied 3689 . . . . . . . . 9 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → ([𝑊 / 𝑦](𝑓:(1...(♯‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑔𝑓))‘(♯‘𝑦))) ↔ (𝑓:(1...(♯‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(♯‘𝑊)))))
9067, 89bitrd 271 . . . . . . . 8 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → ([(𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(♯‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑔𝑓))‘(♯‘𝑦))) ↔ (𝑓:(1...(♯‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(♯‘𝑊)))))
9190exbidv 1964 . . . . . . 7 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (∃𝑓[(𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(♯‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑔𝑓))‘(♯‘𝑦))) ↔ ∃𝑓(𝑓:(1...(♯‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(♯‘𝑊)))))
9291iotabidv 6122 . . . . . 6 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (℩𝑥𝑓[(𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(♯‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑔𝑓))‘(♯‘𝑦)))) = (℩𝑥𝑓(𝑓:(1...(♯‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(♯‘𝑊)))))
9348, 59, 92ifbieq12d 4334 . . . . 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 4334 . . . 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 3778 . . 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 2814 . 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 3416 . 2 (𝜑𝐺 ∈ V)
9968elexd 3416 . 2 (𝜑𝐹 ∈ V)
10042fvexi 6462 . . . 4 0 ∈ V
101 iotaex 6118 . . . . 5 (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))) ∈ V
102 iotaex 6118 . . . . 5 (℩𝑥𝑓(𝑓:(1...(♯‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(♯‘𝑊)))) ∈ V
103101, 102ifex 4355 . . . 4 if(𝐴 ∈ ran ..., (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑥𝑓(𝑓:(1...(♯‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(♯‘𝑊))))) ∈ V
104100, 103ifex 4355 . . 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, 105ovmpt2d 7067 1 (𝜑 → (𝐺 Σg 𝐹) = if(ran 𝐹𝑂, 0 , if(𝐴 ∈ ran ..., (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑥𝑓(𝑓:(1...(♯‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(♯‘𝑊)))))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 386   = wceq 1601  wex 1823  wcel 2107  wral 3090  wrex 3091  {crab 3094  Vcvv 3398  [wsbc 3652  csb 3751  cdif 3789  wss 3792  ifcif 4307  ccnv 5356  dom cdm 5357  ran crn 5358  cima 5360  ccom 5361  cio 6099  1-1-ontowf1o 6136  cfv 6137  (class class class)co 6924  cmpt2 6926  1c1 10275  cuz 11996  ...cfz 12647  seqcseq 13123  chash 13439  Basecbs 16259  +gcplusg 16342  0gc0g 16490   Σg cgsu 16491
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5019  ax-nul 5027  ax-pow 5079  ax-pr 5140  ax-un 7228
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4674  df-br 4889  df-opab 4951  df-mpt 4968  df-id 5263  df-xp 5363  df-rel 5364  df-cnv 5365  df-co 5366  df-dm 5367  df-rn 5368  df-res 5369  df-ima 5370  df-pred 5935  df-iota 6101  df-fun 6139  df-fn 6140  df-f 6141  df-f1 6142  df-fo 6143  df-f1o 6144  df-fv 6145  df-ov 6927  df-oprab 6928  df-mpt2 6929  df-wrecs 7691  df-recs 7753  df-rdg 7791  df-seq 13124  df-gsum 16493
This theorem is referenced by:  gsumval  17661  gsumpropd  17662  gsumpropd2lem  17663
  Copyright terms: Public domain W3C validator