gsumvalx - Metamath Proof Explorer

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

Theorem gsumvalx 18755

Description: Expand out the substitutions in df-gsum 17512. (Contributed by Mario Carneiro, 18-Sep-2015.)

**Hypotheses**
Ref	Expression
gsumval.b	⊢ 𝐵 = (Base‘𝐺)
gsumval.z	⊢ 0 = (0_g‘𝐺)
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 17512	. . 3 ⊢ Σ_g = (𝑤 ∈ V, 𝑔 ∈ V ↦ ⦋{𝑥 ∈ (Base‘𝑤) ∣ ∀𝑦 ∈ (Base‘𝑤)((𝑥(+_g‘𝑤)𝑦) = 𝑦 ∧ (𝑦(+_g‘𝑤)𝑥) = 𝑦)} / 𝑜⦌if(ran 𝑔 ⊆ 𝑜, (0_g‘𝑤), 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 𝑔 ⊆ 𝑜, (0_g‘𝑤), if(dom 𝑔 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ_≥‘𝑚)(dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+_g‘𝑤), 𝑔)‘𝑛))), (℩𝑥∃𝑓[(^◡𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(♯‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+_g‘𝑤), (𝑔 ∘ 𝑓))‘(♯‘𝑦))))))))
3		simprl 783	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → 𝑤 = 𝐺)
4	3	fveq2d 6889	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → (Base‘𝑤) = (Base‘𝐺))
5		gsumval.b	. . . . . . 7 ⊢ 𝐵 = (Base‘𝐺)
6	4, 5	eqtr4di 2818	. . . . . 6 ⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → (Base‘𝑤) = 𝐵)
7	3	fveq2d 6889	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → (+_g‘𝑤) = (+_g‘𝐺))
8		gsumval.p	. . . . . . . . . . 11 ⊢ + = (+_g‘𝐺)
9	7, 8	eqtr4di 2818	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → (+_g‘𝑤) = + )
10	9	oveqd 7433	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → (𝑥(+_g‘𝑤)𝑦) = (𝑥 + 𝑦))
11	10	eqeq1d 2767	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → ((𝑥(+_g‘𝑤)𝑦) = 𝑦 ↔ (𝑥 + 𝑦) = 𝑦))
12	9	oveqd 7433	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → (𝑦(+_g‘𝑤)𝑥) = (𝑦 + 𝑥))
13	12	eqeq1d 2767	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → ((𝑦(+_g‘𝑤)𝑥) = 𝑦 ↔ (𝑦 + 𝑥) = 𝑦))
14	11, 13	anbi12d 644	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → (((𝑥(+_g‘𝑤)𝑦) = 𝑦 ∧ (𝑦(+_g‘𝑤)𝑥) = 𝑦) ↔ ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)))
15	6, 14	raleqbidv 3340	. . . . . 6 ⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → (∀𝑦 ∈ (Base‘𝑤)((𝑥(+_g‘𝑤)𝑦) = 𝑦 ∧ (𝑦(+_g‘𝑤)𝑥) = 𝑦) ↔ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)))
16	6, 15	rabeqbidv 3436	. . . . 5 ⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → {𝑥 ∈ (Base‘𝑤) ∣ ∀𝑦 ∈ (Base‘𝑤)((𝑥(+_g‘𝑤)𝑦) = 𝑦 ∧ (𝑦(+_g‘𝑤)𝑥) = 𝑦)} = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)})
17		gsumval.o	. . . . . 6 ⊢ 𝑂 = {𝑠 ∈ 𝐵 ∣ ∀𝑡 ∈ 𝐵 ((𝑠 + 𝑡) = 𝑡 ∧ (𝑡 + 𝑠) = 𝑡)}
18		oveq2 7424	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑦 → (𝑠 + 𝑡) = (𝑠 + 𝑦))
19		id 23	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑦 → 𝑡 = 𝑦)
20	18, 19	eqeq12d 2781	. . . . . . . . . 10 ⊢ (𝑡 = 𝑦 → ((𝑠 + 𝑡) = 𝑡 ↔ (𝑠 + 𝑦) = 𝑦))
21		oveq1 7423	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑦 → (𝑡 + 𝑠) = (𝑦 + 𝑠))
22	21, 19	eqeq12d 2781	. . . . . . . . . 10 ⊢ (𝑡 = 𝑦 → ((𝑡 + 𝑠) = 𝑡 ↔ (𝑦 + 𝑠) = 𝑦))
23	20, 22	anbi12d 644	. . . . . . . . 9 ⊢ (𝑡 = 𝑦 → (((𝑠 + 𝑡) = 𝑡 ∧ (𝑡 + 𝑠) = 𝑡) ↔ ((𝑠 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑠) = 𝑦)))
24	23	cbvralvw 3245	. . . . . . . 8 ⊢ (∀𝑡 ∈ 𝐵 ((𝑠 + 𝑡) = 𝑡 ∧ (𝑡 + 𝑠) = 𝑡) ↔ ∀𝑦 ∈ 𝐵 ((𝑠 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑠) = 𝑦))
25		oveq1 7423	. . . . . . . . . 10 ⊢ (𝑠 = 𝑥 → (𝑠 + 𝑦) = (𝑥 + 𝑦))
26	25	eqeq1d 2767	. . . . . . . . 9 ⊢ (𝑠 = 𝑥 → ((𝑠 + 𝑦) = 𝑦 ↔ (𝑥 + 𝑦) = 𝑦))
27	26	ovanraleqv 7440	. . . . . . . 8 ⊢ (𝑠 = 𝑥 → (∀𝑦 ∈ 𝐵 ((𝑠 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑠) = 𝑦) ↔ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)))
28	24, 27	bitrid 286	. . . . . . 7 ⊢ (𝑠 = 𝑥 → (∀𝑡 ∈ 𝐵 ((𝑠 + 𝑡) = 𝑡 ∧ (𝑡 + 𝑠) = 𝑡) ↔ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)))
29	28	cbvrabv 3428	. . . . . 6 ⊢ {𝑠 ∈ 𝐵 ∣ ∀𝑡 ∈ 𝐵 ((𝑠 + 𝑡) = 𝑡 ∧ (𝑡 + 𝑠) = 𝑡)} = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)}
30	17, 29	eqtri 2788	. . . . 5 ⊢ 𝑂 = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)}
31	16, 30	eqtr4di 2818	. . . 4 ⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → {𝑥 ∈ (Base‘𝑤) ∣ ∀𝑦 ∈ (Base‘𝑤)((𝑥(+_g‘𝑤)𝑦) = 𝑦 ∧ (𝑦(+_g‘𝑤)𝑥) = 𝑦)} = 𝑂)
32	31	csbeq1d 3858	. . 3 ⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → ⦋{𝑥 ∈ (Base‘𝑤) ∣ ∀𝑦 ∈ (Base‘𝑤)((𝑥(+_g‘𝑤)𝑦) = 𝑦 ∧ (𝑦(+_g‘𝑤)𝑥) = 𝑦)} / 𝑜⦌if(ran 𝑔 ⊆ 𝑜, (0_g‘𝑤), if(dom 𝑔 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ_≥‘𝑚)(dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+_g‘𝑤), 𝑔)‘𝑛))), (℩𝑥∃𝑓[(^◡𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(♯‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+_g‘𝑤), (𝑔 ∘ 𝑓))‘(♯‘𝑦)))))) = ⦋𝑂 / 𝑜⦌if(ran 𝑔 ⊆ 𝑜, (0_g‘𝑤), if(dom 𝑔 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ_≥‘𝑚)(dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+_g‘𝑤), 𝑔)‘𝑛))), (℩𝑥∃𝑓[(^◡𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(♯‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+_g‘𝑤), (𝑔 ∘ 𝑓))‘(♯‘𝑦)))))))
33	5	fvexi 6899	. . . . . 6 ⊢ 𝐵 ∈ V
34	17, 33	rabex2 5313	. . . . 5 ⊢ 𝑂 ∈ V
35	34	a1i 11	. . . 4 ⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → 𝑂 ∈ V)
36		simplrr 790	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → 𝑔 = 𝐹)
37	36	rneqd 5930	. . . . . 6 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → ran 𝑔 = ran 𝐹)
38		simpr 490	. . . . . 6 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → 𝑜 = 𝑂)
39	37, 38	sseq12d 3971	. . . . 5 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (ran 𝑔 ⊆ 𝑜 ↔ ran 𝐹 ⊆ 𝑂))
40	3	adantr 486	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → 𝑤 = 𝐺)
41	40	fveq2d 6889	. . . . . 6 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (0_g‘𝑤) = (0_g‘𝐺))
42		gsumval.z	. . . . . 6 ⊢ 0 = (0_g‘𝐺)
43	41, 42	eqtr4di 2818	. . . . 5 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (0_g‘𝑤) = 0 )
44	36	dmeqd 5897	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → dom 𝑔 = dom 𝐹)
45		gsumvalx.a	. . . . . . . . 9 ⊢ (𝜑 → dom 𝐹 = 𝐴)
46	45	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → dom 𝐹 = 𝐴)
47	44, 46	eqtrd 2800	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → dom 𝑔 = 𝐴)
48	47	eleq1d 2850	. . . . . 6 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (dom 𝑔 ∈ ran ... ↔ 𝐴 ∈ ran ...))
49	47	eqeq1d 2767	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (dom 𝑔 = (𝑚...𝑛) ↔ 𝐴 = (𝑚...𝑛)))
50	9	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (+_g‘𝑤) = + )
51	50	seqeq2d 14057	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → seq𝑚((+_g‘𝑤), 𝑔) = seq𝑚( + , 𝑔))
52	36	seqeq3d 14058	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → seq𝑚( + , 𝑔) = seq𝑚( + , 𝐹))
53	51, 52	eqtrd 2800	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → seq𝑚((+_g‘𝑤), 𝑔) = seq𝑚( + , 𝐹))
54	53	fveq1d 6887	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (seq𝑚((+_g‘𝑤), 𝑔)‘𝑛) = (seq𝑚( + , 𝐹)‘𝑛))
55	54	eqeq2d 2776	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (𝑥 = (seq𝑚((+_g‘𝑤), 𝑔)‘𝑛) ↔ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛)))
56	49, 55	anbi12d 644	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → ((dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+_g‘𝑤), 𝑔)‘𝑛)) ↔ (𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))))
57	56	rexbidv 3191	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (∃𝑛 ∈ (ℤ_≥‘𝑚)(dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+_g‘𝑤), 𝑔)‘𝑛)) ↔ ∃𝑛 ∈ (ℤ_≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))))
58	57	exbidv 1954	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (∃𝑚∃𝑛 ∈ (ℤ_≥‘𝑚)(dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+_g‘𝑤), 𝑔)‘𝑛)) ↔ ∃𝑚∃𝑛 ∈ (ℤ_≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))))
59	58	iotabidv 6524	. . . . . 6 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (℩𝑥∃𝑚∃𝑛 ∈ (ℤ_≥‘𝑚)(dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+_g‘𝑤), 𝑔)‘𝑛))) = (℩𝑥∃𝑚∃𝑛 ∈ (ℤ_≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))))
60	38	difeq2d 4081	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (V ∖ 𝑜) = (V ∖ 𝑂))
61	60	imaeq2d 6064	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (^◡𝐹 “ (V ∖ 𝑜)) = (^◡𝐹 “ (V ∖ 𝑂)))
62	36	cnveqd 5863	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → ^◡𝑔 = ^◡𝐹)
63	62	imaeq1d 6063	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (^◡𝑔 “ (V ∖ 𝑜)) = (^◡𝐹 “ (V ∖ 𝑜)))
64		gsumval.w	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑊 = (^◡𝐹 “ (V ∖ 𝑂)))
65	64	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → 𝑊 = (^◡𝐹 “ (V ∖ 𝑂)))
66	61, 63, 65	3eqtr4d 2810	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (^◡𝑔 “ (V ∖ 𝑜)) = 𝑊)
67	66	sbceq1d 3751	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → ([(^◡𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(♯‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+_g‘𝑤), (𝑔 ∘ 𝑓))‘(♯‘𝑦))) ↔ [𝑊 / 𝑦](𝑓:(1...(♯‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+_g‘𝑤), (𝑔 ∘ 𝑓))‘(♯‘𝑦)))))
68		gsumvalx.f	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 ∈ 𝑋)
69		cnvexg 7923	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ 𝑋 → ^◡𝐹 ∈ V)
70		imaexg 7912	. . . . . . . . . . . . 13 ⊢ (^◡𝐹 ∈ V → (^◡𝐹 “ (V ∖ 𝑂)) ∈ V)
71	68, 69, 70	3syl 19	. . . . . . . . . . . 12 ⊢ (𝜑 → (^◡𝐹 “ (V ∖ 𝑂)) ∈ V)
72	64, 71	eqeltrd 2865	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑊 ∈ V)
73	72	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → 𝑊 ∈ V)
74		fveq2 6885	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑊 → (♯‘𝑦) = (♯‘𝑊))
75	74	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (♯‘𝑦) = (♯‘𝑊))
76	75	oveq2d 7432	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (1...(♯‘𝑦)) = (1...(♯‘𝑊)))
77	76	f1oeq2d 6820	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (𝑓:(1...(♯‘𝑦))–1-1-onto→𝑦 ↔ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑦))
78		f1oeq3 6814	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑊 → (𝑓:(1...(♯‘𝑊))–1-1-onto→𝑦 ↔ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊))
79	78	adantl 487	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (𝑓:(1...(♯‘𝑊))–1-1-onto→𝑦 ↔ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊))
80	77, 79	bitrd 282	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (𝑓:(1...(♯‘𝑦))–1-1-onto→𝑦 ↔ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊))
81	50	seqeq2d 14057	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → seq1((+_g‘𝑤), (𝑔 ∘ 𝑓)) = seq1( + , (𝑔 ∘ 𝑓)))
82	36	coeq1d 5849	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (𝑔 ∘ 𝑓) = (𝐹 ∘ 𝑓))
83	82	seqeq3d 14058	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → seq1( + , (𝑔 ∘ 𝑓)) = seq1( + , (𝐹 ∘ 𝑓)))
84	81, 83	eqtrd 2800	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → seq1((+_g‘𝑤), (𝑔 ∘ 𝑓)) = seq1( + , (𝐹 ∘ 𝑓)))
85	84	adantr 486	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → seq1((+_g‘𝑤), (𝑔 ∘ 𝑓)) = seq1( + , (𝐹 ∘ 𝑓)))
86	85, 75	fveq12d 6892	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (seq1((+_g‘𝑤), (𝑔 ∘ 𝑓))‘(♯‘𝑦)) = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘𝑊)))
87	86	eqeq2d 2776	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → (𝑥 = (seq1((+_g‘𝑤), (𝑔 ∘ 𝑓))‘(♯‘𝑦)) ↔ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘𝑊))))
88	80, 87	anbi12d 644	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) ∧ 𝑦 = 𝑊) → ((𝑓:(1...(♯‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+_g‘𝑤), (𝑔 ∘ 𝑓))‘(♯‘𝑦))) ↔ (𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘𝑊)))))
89	73, 88	sbcied 3789	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → ([𝑊 / 𝑦](𝑓:(1...(♯‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+_g‘𝑤), (𝑔 ∘ 𝑓))‘(♯‘𝑦))) ↔ (𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘𝑊)))))
90	67, 89	bitrd 282	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → ([(^◡𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(♯‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+_g‘𝑤), (𝑔 ∘ 𝑓))‘(♯‘𝑦))) ↔ (𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘𝑊)))))
91	90	exbidv 1954	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (∃𝑓[(^◡𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(♯‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+_g‘𝑤), (𝑔 ∘ 𝑓))‘(♯‘𝑦))) ↔ ∃𝑓(𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘𝑊)))))
92	91	iotabidv 6524	. . . . . 6 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → (℩𝑥∃𝑓[(^◡𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(♯‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+_g‘𝑤), (𝑔 ∘ 𝑓))‘(♯‘𝑦)))) = (℩𝑥∃𝑓(𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘𝑊)))))
93	48, 59, 92	ifbieq12d 4518	. . . . 5 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → if(dom 𝑔 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ_≥‘𝑚)(dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+_g‘𝑤), 𝑔)‘𝑛))), (℩𝑥∃𝑓[(^◡𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(♯‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+_g‘𝑤), (𝑔 ∘ 𝑓))‘(♯‘𝑦))))) = if(𝐴 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ_≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑥∃𝑓(𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘𝑊))))))
94	39, 43, 93	ifbieq12d 4518	. . . 4 ⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) ∧ 𝑜 = 𝑂) → if(ran 𝑔 ⊆ 𝑜, (0_g‘𝑤), if(dom 𝑔 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ_≥‘𝑚)(dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+_g‘𝑤), 𝑔)‘𝑛))), (℩𝑥∃𝑓[(^◡𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(♯‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+_g‘𝑤), (𝑔 ∘ 𝑓))‘(♯‘𝑦)))))) = if(ran 𝐹 ⊆ 𝑂, 0 , if(𝐴 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ_≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑥∃𝑓(𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘𝑊)))))))
95	35, 94	csbied 3890	. . 3 ⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → ⦋𝑂 / 𝑜⦌if(ran 𝑔 ⊆ 𝑜, (0_g‘𝑤), if(dom 𝑔 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ_≥‘𝑚)(dom 𝑔 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+_g‘𝑤), 𝑔)‘𝑛))), (℩𝑥∃𝑓[(^◡𝑔 “ (V ∖ 𝑜)) / 𝑦](𝑓:(1...(♯‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+_g‘𝑤), (𝑔 ∘ 𝑓))‘(♯‘𝑦)))))) = if(ran 𝐹 ⊆ 𝑂, 0 , if(𝐴 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ_≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑥∃𝑓(𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘𝑊)))))))
96	32, 95	eqtrd 2800	. 2 ⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑔 = 𝐹)) → ⦋{𝑥 ∈ (Base‘𝑤) ∣ ∀𝑦 ∈ (Base‘𝑤)((𝑥(+_g‘𝑤)𝑦) = 𝑦 ∧ (𝑦(+_g‘𝑤)𝑥) = 𝑦)} / 𝑜⦌if(ran 𝑔 ⊆ 𝑜, (0_g‘𝑤), 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 ⊢ (𝜑 → 𝐺 ∈ 𝑉)
98	97	elexd 3480	. 2 ⊢ (𝜑 → 𝐺 ∈ V)
99	68	elexd 3480	. 2 ⊢ (𝜑 → 𝐹 ∈ V)
100	42	fvexi 6899	. . . 4 ⊢ 0 ∈ V
101		iotaex 6516	. . . . 5 ⊢ (℩𝑥∃𝑚∃𝑛 ∈ (ℤ_≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))) ∈ V
102		iotaex 6516	. . . . 5 ⊢ (℩𝑥∃𝑓(𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘𝑊)))) ∈ V
103	101, 102	ifex 4540	. . . 4 ⊢ if(𝐴 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ_≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑥∃𝑓(𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘𝑊))))) ∈ V
104	100, 103	ifex 4540	. . 3 ⊢ if(ran 𝐹 ⊆ 𝑂, 0 , if(𝐴 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ_≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑥∃𝑓(𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘𝑊)))))) ∈ V
105	104	a1i 11	. 2 ⊢ (𝜑 → if(ran 𝐹 ⊆ 𝑂, 0 , if(𝐴 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ_≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑥∃𝑓(𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘𝑊)))))) ∈ V)
106	2, 96, 98, 99, 105	ovmpod 7568	1 ⊢ (𝜑 → (𝐺 Σ_g 𝐹) = if(ran 𝐹 ⊆ 𝑂, 0 , if(𝐴 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ_≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑥∃𝑓(𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘𝑊)))))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∃wex 1812 ∈ wcel 2146 ∀wral 3081 ∃wrex 3091 {crab 3418 Vcvv 3457 [wsbc 3746 ⦋csb 3854 ∖ cdif 3903 ⊆ wss 3906 ifcif 4489 ^◡ccnv 5662 dom cdm 5663 ran crn 5664 “ cima 5666 ∘ ccom 5667 ℩cio 6494 –1-1-onto→wf1o 6539 ‘cfv 6540 (class class class)co 7416 ∈ cmpo 7418 1c1 11112 ℤ_≥cuz 12873 ...cfz 13546 seqcseq 14050 ♯chash 14379 Basecbs 17286 +_gcplusg 17327 0_gc0g 17509 Σ_g cgsu 17510

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7738

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-ral 3082 df-rex 3092 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4875 df-br 5112 df-opab 5176 df-mpt 5195 df-id 5558 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6306 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-ov 7419 df-oprab 7420 df-mpo 7421 df-frecs 8280 df-wrecs 8311 df-recs 8360 df-rdg 8399 df-seq 14051 df-gsum 17512

This theorem is used by: gsumval 18756 gsumpropd 18757 gsumpropd2lem 18758

W3C validator