Theorem gsumvalx 17270

Description: Expand out the substitutions in df-gsum 16103. (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.

Step	Hyp	Ref	Expression
1		df-gsum 16103	. . 3 ⊢ Σg = (𝑤 ∈ V, 𝑔 ∈ V ↦ ⦋{𝑥 ∈ (Base‘𝑤) ∣ ∀𝑦 ∈ (Base‘𝑤)((𝑥(+g‘𝑤)𝑦) = 𝑦 ∧ (𝑦(+g‘𝑤)𝑥) = 𝑦)} / 𝑜⦌if(ran 𝑔 ⊆ 𝑜, (0g‘𝑤), if(dom 𝑔 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑔)‘𝑛))), (℩𝑥∃𝑓[(◡𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(#‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑔 ∘ 𝑓))‘(#‘𝑦)))))))
2	1	a1i 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 794	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → 𝑤 = 𝐺)
4	3	fveq2d 6195	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → (Base‘𝑤) = (Base‘𝐺))
5		gsumval.b	. . . . . . 7 ⊢ 𝐵 = (Base‘𝐺)
6	4, 5	syl6eqr 2674	. . . . . 6 ⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → (Base‘𝑤) = 𝐵)
7	3	fveq2d 6195	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → (+g‘𝑤) = (+g‘𝐺))
8		gsumval.p	. . . . . . . . . . 11 ⊢ + = (+g‘𝐺)
9	7, 8	syl6eqr 2674	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → (+g‘𝑤) = + )
10	9	oveqd 6667	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → (𝑥(+g‘𝑤)𝑦) = (𝑥 + 𝑦))
11	10	eqeq1d 2624	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → ((𝑥(+g‘𝑤)𝑦) = 𝑦 ↔ (𝑥 + 𝑦) = 𝑦))
12	9	oveqd 6667	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → (𝑦(+g‘𝑤)𝑥) = (𝑦 + 𝑥))
13	12	eqeq1d 2624	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → ((𝑦(+g‘𝑤)𝑥) = 𝑦 ↔ (𝑦 + 𝑥) = 𝑦))
14	11, 13	anbi12d 747	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → (((𝑥(+g‘𝑤)𝑦) = 𝑦 ∧ (𝑦(+g‘𝑤)𝑥) = 𝑦) ↔ ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)))
15	6, 14	raleqbidv 3152	. . . . . 6 ⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → (∀𝑦 ∈ (Base‘𝑤)((𝑥(+g‘𝑤)𝑦) = 𝑦 ∧ (𝑦(+g‘𝑤)𝑥) = 𝑦) ↔ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)))
16	6, 15	rabeqbidv 3195	. . . . 5 ⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → {𝑥 ∈ (Base‘𝑤) ∣ ∀𝑦 ∈ (Base‘𝑤)((𝑥(+g‘𝑤)𝑦) = 𝑦 ∧ (𝑦(+g‘𝑤)𝑥) = 𝑦)} = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)})
17		gsumval.o	. . . . . 6 ⊢ 𝑂 = {𝑠 ∈ 𝐵 ∣ ∀𝑡 ∈ 𝐵 ((𝑠 + 𝑡) = 𝑡 ∧ (𝑡 + 𝑠) = 𝑡)}
18		oveq2 6658	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑦 → (𝑠 + 𝑡) = (𝑠 + 𝑦))
19		id 22	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑦 → 𝑡 = 𝑦)
20	18, 19	eqeq12d 2637	. . . . . . . . . 10 ⊢ (𝑡 = 𝑦 → ((𝑠 + 𝑡) = 𝑡 ↔ (𝑠 + 𝑦) = 𝑦))
21		oveq1 6657	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑦 → (𝑡 + 𝑠) = (𝑦 + 𝑠))
22	21, 19	eqeq12d 2637	. . . . . . . . . 10 ⊢ (𝑡 = 𝑦 → ((𝑡 + 𝑠) = 𝑡 ↔ (𝑦 + 𝑠) = 𝑦))
23	20, 22	anbi12d 747	. . . . . . . . 9 ⊢ (𝑡 = 𝑦 → (((𝑠 + 𝑡) = 𝑡 ∧ (𝑡 + 𝑠) = 𝑡) ↔ ((𝑠 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑠) = 𝑦)))
24	23	cbvralv 3171	. . . . . . . 8 ⊢ (∀𝑡 ∈ 𝐵 ((𝑠 + 𝑡) = 𝑡 ∧ (𝑡 + 𝑠) = 𝑡) ↔ ∀𝑦 ∈ 𝐵 ((𝑠 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑠) = 𝑦))
25		oveq1 6657	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑥 → (𝑠 + 𝑦) = (𝑥 + 𝑦))
26	25	eqeq1d 2624	. . . . . . . . . 10 ⊢ (𝑠 = 𝑥 → ((𝑠 + 𝑦) = 𝑦 ↔ (𝑥 + 𝑦) = 𝑦))
27		oveq2 6658	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑥 → (𝑦 + 𝑠) = (𝑦 + 𝑥))
28	27	eqeq1d 2624	. . . . . . . . . 10 ⊢ (𝑠 = 𝑥 → ((𝑦 + 𝑠) = 𝑦 ↔ (𝑦 + 𝑥) = 𝑦))
29	26, 28	anbi12d 747	. . . . . . . . 9 ⊢ (𝑠 = 𝑥 → (((𝑠 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑠) = 𝑦) ↔ ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)))
30	29	ralbidv 2986	. . . . . . . 8 ⊢ (𝑠 = 𝑥 → (∀𝑦 ∈ 𝐵 ((𝑠 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑠) = 𝑦) ↔ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)))
31	24, 30	syl5bb 272	. . . . . . 7 ⊢ (𝑠 = 𝑥 → (∀𝑡 ∈ 𝐵 ((𝑠 + 𝑡) = 𝑡 ∧ (𝑡 + 𝑠) = 𝑡) ↔ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)))
32	31	cbvrabv 3199	. . . . . 6 ⊢ {𝑠 ∈ 𝐵 ∣ ∀𝑡 ∈ 𝐵 ((𝑠 + 𝑡) = 𝑡 ∧ (𝑡 + 𝑠) = 𝑡)} = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)}
33	17, 32	eqtri 2644	. . . . 5 ⊢ 𝑂 = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)}
34	16, 33	syl6eqr 2674	. . . 4 ⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → {𝑥 ∈ (Base‘𝑤) ∣ ∀𝑦 ∈ (Base‘𝑤)((𝑥(+g‘𝑤)𝑦) = 𝑦 ∧ (𝑦(+g‘𝑤)𝑥) = 𝑦)} = 𝑂)
35	34	csbeq1d 3540	. . 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 6201	. . . . . . 7 ⊢ (Base‘𝐺) ∈ V
37	5, 36	eqeltri 2697	. . . . . 6 ⊢ 𝐵 ∈ V
38	17, 37	rabex2 4815	. . . . 5 ⊢ 𝑂 ∈ V
39	38	a1i 11	. . . 4 ⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → 𝑂 ∈ V)
40		simplrr 801	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → 𝑔 = 𝐹)
41	40	rneqd 5353	. . . . . 6 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → ran 𝑔 = ran 𝐹)
42		simpr 477	. . . . . 6 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → 𝑜 = 𝑂)
43	41, 42	sseq12d 3634	. . . . 5 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (ran 𝑔 ⊆ 𝑜 ↔ ran 𝐹 ⊆ 𝑂))
44	3	adantr 481	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → 𝑤 = 𝐺)
45	44	fveq2d 6195	. . . . . 6 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (0g‘𝑤) = (0g‘𝐺))
46		gsumval.z	. . . . . 6 ⊢ 0 = (0g‘𝐺)
47	45, 46	syl6eqr 2674	. . . . 5 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (0g‘𝑤) = 0 )
48	40	dmeqd 5326	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → dom 𝑔 = dom 𝐹)
49		gsumvalx.a	. . . . . . . . 9 ⊢ (𝜑 → dom 𝐹 = 𝐴)
50	49	ad2antrr 762	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → dom 𝐹 = 𝐴)
51	48, 50	eqtrd 2656	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → dom 𝑔 = 𝐴)
52	51	eleq1d 2686	. . . . . 6 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (dom 𝑔 ∈ ran ... ↔ 𝐴 ∈ ran ...))
53	51	eqeq1d 2624	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (dom 𝑔 = (𝑚...𝑛) ↔ 𝐴 = (𝑚...𝑛)))
54	9	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (+g‘𝑤) = + )
55	54	seqeq2d 12808	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → seq𝑚((+g‘𝑤), 𝑔) = seq𝑚( + , 𝑔))
56	40	seqeq3d 12809	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → seq𝑚( + , 𝑔) = seq𝑚( + , 𝐹))
57	55, 56	eqtrd 2656	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → seq𝑚((+g‘𝑤), 𝑔) = seq𝑚( + , 𝐹))
58	57	fveq1d 6193	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (seq𝑚((+g‘𝑤), 𝑔)‘𝑛) = (seq𝑚( + , 𝐹)‘𝑛))
59	58	eqeq2d 2632	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (𝑥 = (seq𝑚((+g‘𝑤), 𝑔)‘𝑛) ↔ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛)))
60	53, 59	anbi12d 747	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → ((dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑔)‘𝑛)) ↔ (𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))))
61	60	rexbidv 3052	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑔)‘𝑛)) ↔ ∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))))
62	61	exbidv 1850	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑔)‘𝑛)) ↔ ∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))))
63	62	iotabidv 5872	. . . . . 6 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑔)‘𝑛))) = (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))))
64	42	difeq2d 3728	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (V ∖ 𝑜) = (V ∖ 𝑂))
65	64	imaeq2d 5466	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (◡𝐹 “ (V ∖ 𝑜)) = (◡𝐹 “ (V ∖ 𝑂)))
66	40	cnveqd 5298	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → ◡𝑔 = ◡𝐹)
67	66	imaeq1d 5465	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (◡𝑔 “ (V ∖ 𝑜)) = (◡𝐹 “ (V ∖ 𝑜)))
68		gsumval.w	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑊 = (◡𝐹 “ (V ∖ 𝑂)))
69	68	ad2antrr 762	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → 𝑊 = (◡𝐹 “ (V ∖ 𝑂)))
70	65, 67, 69	3eqtr4d 2666	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (◡𝑔 “ (V ∖ 𝑜)) = 𝑊)
71	70	sbceq1d 3440	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → ([(◡𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(#‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑔 ∘ 𝑓))‘(#‘𝑦))) ↔ [𝑊 / 𝑦](𝑓:(1...(#‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑔 ∘ 𝑓))‘(#‘𝑦)))))
72		gsumvalx.f	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 ∈ 𝑋)
73		cnvexg 7112	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ 𝑋 → ◡𝐹 ∈ V)
74		imaexg 7103	. . . . . . . . . . . . 13 ⊢ (◡𝐹 ∈ V → (◡𝐹 “ (V ∖ 𝑂)) ∈ V)
75	72, 73, 74	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → (◡𝐹 “ (V ∖ 𝑂)) ∈ V)
76	68, 75	eqeltrd 2701	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑊 ∈ V)
77	76	ad2antrr 762	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → 𝑊 ∈ V)
78		fveq2 6191	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑊 → (#‘𝑦) = (#‘𝑊))
79	78	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (#‘𝑦) = (#‘𝑊))
80	79	oveq2d 6666	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (1...(#‘𝑦)) = (1...(#‘𝑊)))
81		f1oeq2 6128	. . . . . . . . . . . . 13 ⊢ ((1...(#‘𝑦)) = (1...(#‘𝑊)) → (𝑓:(1...(#‘𝑦))–1-1-onto→𝑦 ↔ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑦))
82	80, 81	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (𝑓:(1...(#‘𝑦))–1-1-onto→𝑦 ↔ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑦))
83		f1oeq3 6129	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑊 → (𝑓:(1...(#‘𝑊))–1-1-onto→𝑦 ↔ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊))
84	83	adantl 482	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (𝑓:(1...(#‘𝑊))–1-1-onto→𝑦 ↔ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊))
85	82, 84	bitrd 268	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (𝑓:(1...(#‘𝑦))–1-1-onto→𝑦 ↔ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊))
86	54	seqeq2d 12808	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → seq1((+g‘𝑤), (𝑔 ∘ 𝑓)) = seq1( + , (𝑔 ∘ 𝑓)))
87	40	coeq1d 5283	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (𝑔 ∘ 𝑓) = (𝐹 ∘ 𝑓))
88	87	seqeq3d 12809	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → seq1( + , (𝑔 ∘ 𝑓)) = seq1( + , (𝐹 ∘ 𝑓)))
89	86, 88	eqtrd 2656	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → seq1((+g‘𝑤), (𝑔 ∘ 𝑓)) = seq1( + , (𝐹 ∘ 𝑓)))
90	89	adantr 481	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → seq1((+g‘𝑤), (𝑔 ∘ 𝑓)) = seq1( + , (𝐹 ∘ 𝑓)))
91	90, 79	fveq12d 6197	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (seq1((+g‘𝑤), (𝑔 ∘ 𝑓))‘(#‘𝑦)) = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊)))
92	91	eqeq2d 2632	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (𝑥 = (seq1((+g‘𝑤), (𝑔 ∘ 𝑓))‘(#‘𝑦)) ↔ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊))))
93	85, 92	anbi12d 747	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → ((𝑓:(1...(#‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑔 ∘ 𝑓))‘(#‘𝑦))) ↔ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊)))))
94	77, 93	sbcied 3472	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → ([𝑊 / 𝑦](𝑓:(1...(#‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑔 ∘ 𝑓))‘(#‘𝑦))) ↔ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊)))))
95	71, 94	bitrd 268	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → ([(◡𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(#‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑔 ∘ 𝑓))‘(#‘𝑦))) ↔ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊)))))
96	95	exbidv 1850	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (∃𝑓[(◡𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(#‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑔 ∘ 𝑓))‘(#‘𝑦))) ↔ ∃𝑓(𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊)))))
97	96	iotabidv 5872	. . . . . 6 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (℩𝑥∃𝑓[(◡𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(#‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑔 ∘ 𝑓))‘(#‘𝑦)))) = (℩𝑥∃𝑓(𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊)))))
98	52, 63, 97	ifbieq12d 4113	. . . . 5 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → if(dom 𝑔 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑔)‘𝑛))), (℩𝑥∃𝑓[(◡𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(#‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑔 ∘ 𝑓))‘(#‘𝑦))))) = if(𝐴 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑥∃𝑓(𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊))))))
99	43, 47, 98	ifbieq12d 4113	. . . 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( + , (𝐹 ∘ 𝑓))‘(#‘𝑊)))))))
100	39, 99	csbied 3560	. . 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( + , (𝐹 ∘ 𝑓))‘(#‘𝑊)))))))
101	35, 100	eqtrd 2656	. 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 ⊢ (𝜑 → 𝐺 ∈ 𝑉)
103	102	elexd 3214	. 2 ⊢ (𝜑 → 𝐺 ∈ V)
104	72	elexd 3214	. 2 ⊢ (𝜑 → 𝐹 ∈ V)
105		fvex 6201	. . . . 5 ⊢ (0g‘𝐺) ∈ V
106	46, 105	eqeltri 2697	. . . 4 ⊢ 0 ∈ V
107		iotaex 5868	. . . . 5 ⊢ (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))) ∈ V
108		iotaex 5868	. . . . 5 ⊢ (℩𝑥∃𝑓(𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊)))) ∈ V
109	107, 108	ifex 4156	. . . 4 ⊢ if(𝐴 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑥∃𝑓(𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊))))) ∈ V
110	106, 109	ifex 4156	. . 3 ⊢ if(ran 𝐹 ⊆ 𝑂, 0 , if(𝐴 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑥∃𝑓(𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊)))))) ∈ V
111	110	a1i 11	. 2 ⊢ (𝜑 → if(ran 𝐹 ⊆ 𝑂, 0 , if(𝐴 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑥∃𝑓(𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊)))))) ∈ V)
112	2, 101, 103, 104, 111	ovmpt2d 6788	1 ⊢ (𝜑 → (𝐺 Σg 𝐹) = if(ran 𝐹 ⊆ 𝑂, 0 , if(𝐴 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑥∃𝑓(𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊)))))))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   = wceq 1483  ∃wex 1704   ∈ wcel 1990  ∀wral 2912  ∃wrex 2913  {crab 2916  Vcvv 3200  [wsbc 3435  ⦋csb 3533   ∖ cdif 3571   ⊆ wss 3574  ifcif 4086  ^◡ccnv 5113  dom cdm 5114  ran crn 5115   “ cima 5117   ∘ ccom 5118  ℩cio 5849  –1-1-onto→wf1o 5887  ‘cfv 5888  (class class class)co 6650   ↦ cmpt2 6652  1c1 9937  ℤ_≥cuz 11687  ...cfz 12326  seqcseq 12801  #chash 13117  Basecbs 15857  +_gcplusg 15941  0_gc0g 16100   Σ_g cgsu 16101

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-seq 12802  df-gsum 16103

This theorem is referenced by:  gsumval  17271  gsumpropd  17272  gsumpropd2lem  17273