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

Theorem gsumvalx 17317
Description: Expand out the substitutions in df-gsum 16150. (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 16150 . . 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 809 . . . . . . . 8 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → 𝑤 = 𝐺)
43fveq2d 6233 . . . . . . 7 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → (Base‘𝑤) = (Base‘𝐺))
5 gsumval.b . . . . . . 7 𝐵 = (Base‘𝐺)
64, 5syl6eqr 2703 . . . . . 6 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → (Base‘𝑤) = 𝐵)
73fveq2d 6233 . . . . . . . . . . 11 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → (+g𝑤) = (+g𝐺))
8 gsumval.p . . . . . . . . . . 11 + = (+g𝐺)
97, 8syl6eqr 2703 . . . . . . . . . 10 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → (+g𝑤) = + )
109oveqd 6707 . . . . . . . . 9 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → (𝑥(+g𝑤)𝑦) = (𝑥 + 𝑦))
1110eqeq1d 2653 . . . . . . . 8 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → ((𝑥(+g𝑤)𝑦) = 𝑦 ↔ (𝑥 + 𝑦) = 𝑦))
129oveqd 6707 . . . . . . . . 9 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → (𝑦(+g𝑤)𝑥) = (𝑦 + 𝑥))
1312eqeq1d 2653 . . . . . . . 8 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → ((𝑦(+g𝑤)𝑥) = 𝑦 ↔ (𝑦 + 𝑥) = 𝑦))
1411, 13anbi12d 747 . . . . . . 7 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → (((𝑥(+g𝑤)𝑦) = 𝑦 ∧ (𝑦(+g𝑤)𝑥) = 𝑦) ↔ ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)))
156, 14raleqbidv 3182 . . . . . 6 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → (∀𝑦 ∈ (Base‘𝑤)((𝑥(+g𝑤)𝑦) = 𝑦 ∧ (𝑦(+g𝑤)𝑥) = 𝑦) ↔ ∀𝑦𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)))
166, 15rabeqbidv 3226 . . . . 5 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → {𝑥 ∈ (Base‘𝑤) ∣ ∀𝑦 ∈ (Base‘𝑤)((𝑥(+g𝑤)𝑦) = 𝑦 ∧ (𝑦(+g𝑤)𝑥) = 𝑦)} = {𝑥𝐵 ∣ ∀𝑦𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)})
17 gsumval.o . . . . . 6 𝑂 = {𝑠𝐵 ∣ ∀𝑡𝐵 ((𝑠 + 𝑡) = 𝑡 ∧ (𝑡 + 𝑠) = 𝑡)}
18 oveq2 6698 . . . . . . . . . . 11 (𝑡 = 𝑦 → (𝑠 + 𝑡) = (𝑠 + 𝑦))
19 id 22 . . . . . . . . . . 11 (𝑡 = 𝑦𝑡 = 𝑦)
2018, 19eqeq12d 2666 . . . . . . . . . 10 (𝑡 = 𝑦 → ((𝑠 + 𝑡) = 𝑡 ↔ (𝑠 + 𝑦) = 𝑦))
21 oveq1 6697 . . . . . . . . . . 11 (𝑡 = 𝑦 → (𝑡 + 𝑠) = (𝑦 + 𝑠))
2221, 19eqeq12d 2666 . . . . . . . . . 10 (𝑡 = 𝑦 → ((𝑡 + 𝑠) = 𝑡 ↔ (𝑦 + 𝑠) = 𝑦))
2320, 22anbi12d 747 . . . . . . . . 9 (𝑡 = 𝑦 → (((𝑠 + 𝑡) = 𝑡 ∧ (𝑡 + 𝑠) = 𝑡) ↔ ((𝑠 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑠) = 𝑦)))
2423cbvralv 3201 . . . . . . . 8 (∀𝑡𝐵 ((𝑠 + 𝑡) = 𝑡 ∧ (𝑡 + 𝑠) = 𝑡) ↔ ∀𝑦𝐵 ((𝑠 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑠) = 𝑦))
25 oveq1 6697 . . . . . . . . . . 11 (𝑠 = 𝑥 → (𝑠 + 𝑦) = (𝑥 + 𝑦))
2625eqeq1d 2653 . . . . . . . . . 10 (𝑠 = 𝑥 → ((𝑠 + 𝑦) = 𝑦 ↔ (𝑥 + 𝑦) = 𝑦))
27 oveq2 6698 . . . . . . . . . . 11 (𝑠 = 𝑥 → (𝑦 + 𝑠) = (𝑦 + 𝑥))
2827eqeq1d 2653 . . . . . . . . . 10 (𝑠 = 𝑥 → ((𝑦 + 𝑠) = 𝑦 ↔ (𝑦 + 𝑥) = 𝑦))
2926, 28anbi12d 747 . . . . . . . . 9 (𝑠 = 𝑥 → (((𝑠 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑠) = 𝑦) ↔ ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)))
3029ralbidv 3015 . . . . . . . 8 (𝑠 = 𝑥 → (∀𝑦𝐵 ((𝑠 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑠) = 𝑦) ↔ ∀𝑦𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)))
3124, 30syl5bb 272 . . . . . . 7 (𝑠 = 𝑥 → (∀𝑡𝐵 ((𝑠 + 𝑡) = 𝑡 ∧ (𝑡 + 𝑠) = 𝑡) ↔ ∀𝑦𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)))
3231cbvrabv 3230 . . . . . 6 {𝑠𝐵 ∣ ∀𝑡𝐵 ((𝑠 + 𝑡) = 𝑡 ∧ (𝑡 + 𝑠) = 𝑡)} = {𝑥𝐵 ∣ ∀𝑦𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)}
3317, 32eqtri 2673 . . . . 5 𝑂 = {𝑥𝐵 ∣ ∀𝑦𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)}
3416, 33syl6eqr 2703 . . . 4 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → {𝑥 ∈ (Base‘𝑤) ∣ ∀𝑦 ∈ (Base‘𝑤)((𝑥(+g𝑤)𝑦) = 𝑦 ∧ (𝑦(+g𝑤)𝑥) = 𝑦)} = 𝑂)
3534csbeq1d 3573 . . 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 6239 . . . . . . 7 (Base‘𝐺) ∈ V
375, 36eqeltri 2726 . . . . . 6 𝐵 ∈ V
3817, 37rabex2 4847 . . . . 5 𝑂 ∈ V
3938a1i 11 . . . 4 ((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) → 𝑂 ∈ V)
40 simplrr 818 . . . . . . 7 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → 𝑔 = 𝐹)
4140rneqd 5385 . . . . . 6 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → ran 𝑔 = ran 𝐹)
42 simpr 476 . . . . . 6 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → 𝑜 = 𝑂)
4341, 42sseq12d 3667 . . . . 5 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (ran 𝑔𝑜 ↔ ran 𝐹𝑂))
443adantr 480 . . . . . . 7 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → 𝑤 = 𝐺)
4544fveq2d 6233 . . . . . 6 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (0g𝑤) = (0g𝐺))
46 gsumval.z . . . . . 6 0 = (0g𝐺)
4745, 46syl6eqr 2703 . . . . 5 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (0g𝑤) = 0 )
4840dmeqd 5358 . . . . . . . 8 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → dom 𝑔 = dom 𝐹)
49 gsumvalx.a . . . . . . . . 9 (𝜑 → dom 𝐹 = 𝐴)
5049ad2antrr 762 . . . . . . . 8 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → dom 𝐹 = 𝐴)
5148, 50eqtrd 2685 . . . . . . 7 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → dom 𝑔 = 𝐴)
5251eleq1d 2715 . . . . . 6 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (dom 𝑔 ∈ ran ... ↔ 𝐴 ∈ ran ...))
5351eqeq1d 2653 . . . . . . . . . 10 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (dom 𝑔 = (𝑚...𝑛) ↔ 𝐴 = (𝑚...𝑛)))
549adantr 480 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (+g𝑤) = + )
5554seqeq2d 12848 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → seq𝑚((+g𝑤), 𝑔) = seq𝑚( + , 𝑔))
5640seqeq3d 12849 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → seq𝑚( + , 𝑔) = seq𝑚( + , 𝐹))
5755, 56eqtrd 2685 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → seq𝑚((+g𝑤), 𝑔) = seq𝑚( + , 𝐹))
5857fveq1d 6231 . . . . . . . . . . 11 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (seq𝑚((+g𝑤), 𝑔)‘𝑛) = (seq𝑚( + , 𝐹)‘𝑛))
5958eqeq2d 2661 . . . . . . . . . 10 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (𝑥 = (seq𝑚((+g𝑤), 𝑔)‘𝑛) ↔ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛)))
6053, 59anbi12d 747 . . . . . . . . 9 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → ((dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝑤), 𝑔)‘𝑛)) ↔ (𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))))
6160rexbidv 3081 . . . . . . . 8 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (∃𝑛 ∈ (ℤ𝑚)(dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝑤), 𝑔)‘𝑛)) ↔ ∃𝑛 ∈ (ℤ𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))))
6261exbidv 1890 . . . . . . 7 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (∃𝑚𝑛 ∈ (ℤ𝑚)(dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝑤), 𝑔)‘𝑛)) ↔ ∃𝑚𝑛 ∈ (ℤ𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))))
6362iotabidv 5910 . . . . . 6 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g𝑤), 𝑔)‘𝑛))) = (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))))
6442difeq2d 3761 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (V ∖ 𝑜) = (V ∖ 𝑂))
6564imaeq2d 5501 . . . . . . . . . . 11 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (𝐹 “ (V ∖ 𝑜)) = (𝐹 “ (V ∖ 𝑂)))
6640cnveqd 5330 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → 𝑔 = 𝐹)
6766imaeq1d 5500 . . . . . . . . . . 11 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (𝑔 “ (V ∖ 𝑜)) = (𝐹 “ (V ∖ 𝑜)))
68 gsumval.w . . . . . . . . . . . 12 (𝜑𝑊 = (𝐹 “ (V ∖ 𝑂)))
6968ad2antrr 762 . . . . . . . . . . 11 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → 𝑊 = (𝐹 “ (V ∖ 𝑂)))
7065, 67, 693eqtr4d 2695 . . . . . . . . . 10 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (𝑔 “ (V ∖ 𝑜)) = 𝑊)
7170sbceq1d 3473 . . . . . . . . 9 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → ([(𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(#‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑔𝑓))‘(#‘𝑦))) ↔ [𝑊 / 𝑦](𝑓:(1...(#‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑔𝑓))‘(#‘𝑦)))))
72 gsumvalx.f . . . . . . . . . . . . 13 (𝜑𝐹𝑋)
73 cnvexg 7154 . . . . . . . . . . . . 13 (𝐹𝑋𝐹 ∈ V)
74 imaexg 7145 . . . . . . . . . . . . 13 (𝐹 ∈ V → (𝐹 “ (V ∖ 𝑂)) ∈ V)
7572, 73, 743syl 18 . . . . . . . . . . . 12 (𝜑 → (𝐹 “ (V ∖ 𝑂)) ∈ V)
7668, 75eqeltrd 2730 . . . . . . . . . . 11 (𝜑𝑊 ∈ V)
7776ad2antrr 762 . . . . . . . . . 10 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → 𝑊 ∈ V)
78 fveq2 6229 . . . . . . . . . . . . . . 15 (𝑦 = 𝑊 → (#‘𝑦) = (#‘𝑊))
7978adantl 481 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (#‘𝑦) = (#‘𝑊))
8079oveq2d 6706 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (1...(#‘𝑦)) = (1...(#‘𝑊)))
81 f1oeq2 6166 . . . . . . . . . . . . 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 6167 . . . . . . . . . . . . 13 (𝑦 = 𝑊 → (𝑓:(1...(#‘𝑊))–1-1-onto𝑦𝑓:(1...(#‘𝑊))–1-1-onto𝑊))
8483adantl 481 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (𝑓:(1...(#‘𝑊))–1-1-onto𝑦𝑓:(1...(#‘𝑊))–1-1-onto𝑊))
8582, 84bitrd 268 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (𝑓:(1...(#‘𝑦))–1-1-onto𝑦𝑓:(1...(#‘𝑊))–1-1-onto𝑊))
8654seqeq2d 12848 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → seq1((+g𝑤), (𝑔𝑓)) = seq1( + , (𝑔𝑓)))
8740coeq1d 5316 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (𝑔𝑓) = (𝐹𝑓))
8887seqeq3d 12849 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → seq1( + , (𝑔𝑓)) = seq1( + , (𝐹𝑓)))
8986, 88eqtrd 2685 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → seq1((+g𝑤), (𝑔𝑓)) = seq1( + , (𝐹𝑓)))
9089adantr 480 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → seq1((+g𝑤), (𝑔𝑓)) = seq1( + , (𝐹𝑓)))
9190, 79fveq12d 6235 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (seq1((+g𝑤), (𝑔𝑓))‘(#‘𝑦)) = (seq1( + , (𝐹𝑓))‘(#‘𝑊)))
9291eqeq2d 2661 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (𝑥 = (seq1((+g𝑤), (𝑔𝑓))‘(#‘𝑦)) ↔ 𝑥 = (seq1( + , (𝐹𝑓))‘(#‘𝑊))))
9385, 92anbi12d 747 . . . . . . . . . 10 ((((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → ((𝑓:(1...(#‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑔𝑓))‘(#‘𝑦))) ↔ (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(#‘𝑊)))))
9477, 93sbcied 3505 . . . . . . . . 9 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → ([𝑊 / 𝑦](𝑓:(1...(#‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑔𝑓))‘(#‘𝑦))) ↔ (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(#‘𝑊)))))
9571, 94bitrd 268 . . . . . . . 8 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → ([(𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(#‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑔𝑓))‘(#‘𝑦))) ↔ (𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(#‘𝑊)))))
9695exbidv 1890 . . . . . . 7 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (∃𝑓[(𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(#‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑔𝑓))‘(#‘𝑦))) ↔ ∃𝑓(𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(#‘𝑊)))))
9796iotabidv 5910 . . . . . 6 (((𝜑 ∧ (𝑤 = 𝐺𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (℩𝑥𝑓[(𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(#‘𝑦))–1-1-onto𝑦𝑥 = (seq1((+g𝑤), (𝑔𝑓))‘(#‘𝑦)))) = (℩𝑥𝑓(𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(#‘𝑊)))))
9852, 63, 97ifbieq12d 4146 . . . . 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 4146 . . . 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 3593 . . 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 2685 . 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 3245 . 2 (𝜑𝐺 ∈ V)
10472elexd 3245 . 2 (𝜑𝐹 ∈ V)
105 fvex 6239 . . . . 5 (0g𝐺) ∈ V
10646, 105eqeltri 2726 . . . 4 0 ∈ V
107 iotaex 5906 . . . . 5 (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))) ∈ V
108 iotaex 5906 . . . . 5 (℩𝑥𝑓(𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(#‘𝑊)))) ∈ V
109107, 108ifex 4189 . . . 4 if(𝐴 ∈ ran ..., (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑥𝑓(𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(#‘𝑊))))) ∈ V
110106, 109ifex 4189 . . 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 6830 1 (𝜑 → (𝐺 Σg 𝐹) = if(ran 𝐹𝑂, 0 , if(𝐴 ∈ ran ..., (℩𝑥𝑚𝑛 ∈ (ℤ𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑥𝑓(𝑓:(1...(#‘𝑊))–1-1-onto𝑊𝑥 = (seq1( + , (𝐹𝑓))‘(#‘𝑊)))))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1523  wex 1744  wcel 2030  wral 2941  wrex 2942  {crab 2945  Vcvv 3231  [wsbc 3468  csb 3566  cdif 3604  wss 3607  ifcif 4119  ccnv 5142  dom cdm 5143  ran crn 5144  cima 5146  ccom 5147  cio 5887  1-1-ontowf1o 5925  cfv 5926  (class class class)co 6690  cmpt2 6692  1c1 9975  cuz 11725  ...cfz 12364  seqcseq 12841  #chash 13157  Basecbs 15904  +gcplusg 15988  0gc0g 16147   Σg cgsu 16148
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-seq 12842  df-gsum 16150
This theorem is referenced by:  gsumval  17318  gsumpropd  17319  gsumpropd2lem  17320
  Copyright terms: Public domain W3C validator