Theorem gsum2dfilem2 14272

Description: Lemma for gsum2dfi 14273. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by AV, 8-Jun-2019.) (Revised by Jim Kingdon, 4-Oct-2026.)

Hypotheses

Ref	Expression
gsum2d.b	⊢ 𝐵 = (Base‘𝐺)
gsum2d.z	⊢ 0 = (0g‘𝐺)
gsum2d.g	⊢ (𝜑 → 𝐺 ∈ CMnd)
gsum2dfi.a	⊢ (𝜑 → 𝐴 ∈ Fin)
gsum2d.r	⊢ (𝜑 → Rel 𝐴)
gsum2dfi.d	⊢ (𝜑 → 𝐷 ∈ Fin)
gsum2d.s	⊢ (𝜑 → dom 𝐴 ⊆ 𝐷)
gsum2dfi.dm	⊢ (𝜑 → dom 𝐴 ∈ Fin)
gsum2d.f	⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
gsum2dfi.fi	⊢ ((𝜑 ∧ 𝑗 ∈ 𝐷) → (𝐴 “ {𝑗}) ∈ Fin)

Assertion

Ref	Expression
gsum2dfilem2	⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐺 Σg (𝑗 ∈ dom 𝐴 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))))

Distinct variable groups:   𝑗,𝑘,𝐴   𝑗,𝐹,𝑘   𝑗,𝐺,𝑘   𝜑,𝑗,𝑘   𝐵,𝑗,𝑘   𝐷,𝑗,𝑘   0 ,𝑗,𝑘

Proof of Theorem gsum2dfilem2

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		gsum2d.r	. . . . . 6 ⊢ (𝜑 → Rel 𝐴)
2		resdm 5104	. . . . . 6 ⊢ (Rel 𝐴 → (𝐴 ↾ dom 𝐴) = 𝐴)
3	1, 2	syl 14	. . . . 5 ⊢ (𝜑 → (𝐴 ↾ dom 𝐴) = 𝐴)
4	3	reseq2d 5065	. . . 4 ⊢ (𝜑 → (𝐹 ↾ (𝐴 ↾ dom 𝐴)) = (𝐹 ↾ 𝐴))
5		gsum2d.f	. . . . . . 7 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
6	5	fdmd 5543	. . . . . 6 ⊢ (𝜑 → dom 𝐹 = 𝐴)
7	6	reseq2d 5065	. . . . 5 ⊢ (𝜑 → (𝐹 ↾ dom 𝐹) = (𝐹 ↾ 𝐴))
8		frel 5541	. . . . . 6 ⊢ (𝐹:𝐴⟶𝐵 → Rel 𝐹)
9		resdm 5104	. . . . . 6 ⊢ (Rel 𝐹 → (𝐹 ↾ dom 𝐹) = 𝐹)
10	5, 8, 9	3syl 17	. . . . 5 ⊢ (𝜑 → (𝐹 ↾ dom 𝐹) = 𝐹)
11	7, 10	eqtr3d 2273	. . . 4 ⊢ (𝜑 → (𝐹 ↾ 𝐴) = 𝐹)
12	4, 11	eqtrd 2271	. . 3 ⊢ (𝜑 → (𝐹 ↾ (𝐴 ↾ dom 𝐴)) = 𝐹)
13	12	oveq2d 6104	. 2 ⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ dom 𝐴))) = (𝐺 Σg 𝐹))
14		reseq2 5060	. . . . . 6 ⊢ (𝑥 = ∅ → (𝐴 ↾ 𝑥) = (𝐴 ↾ ∅))
15	14	reseq2d 5065	. . . . 5 ⊢ (𝑥 = ∅ → (𝐹 ↾ (𝐴 ↾ 𝑥)) = (𝐹 ↾ (𝐴 ↾ ∅)))
16	15	oveq2d 6104	. . . 4 ⊢ (𝑥 = ∅ → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑥))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ ∅))))
17		mpteq1 4216	. . . . 5 ⊢ (𝑥 = ∅ → (𝑗 ∈ 𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) = (𝑗 ∈ ∅ ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))
18	17	oveq2d 6104	. . . 4 ⊢ (𝑥 = ∅ → (𝐺 Σg (𝑗 ∈ 𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) = (𝐺 Σg (𝑗 ∈ ∅ ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))))
19	16, 18	eqeq12d 2253	. . 3 ⊢ (𝑥 = ∅ → ((𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑥))) = (𝐺 Σg (𝑗 ∈ 𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) ↔ (𝐺 Σg (𝐹 ↾ (𝐴 ↾ ∅))) = (𝐺 Σg (𝑗 ∈ ∅ ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))))
20		reseq2 5060	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝐴 ↾ 𝑥) = (𝐴 ↾ 𝑦))
21	20	reseq2d 5065	. . . . 5 ⊢ (𝑥 = 𝑦 → (𝐹 ↾ (𝐴 ↾ 𝑥)) = (𝐹 ↾ (𝐴 ↾ 𝑦)))
22	21	oveq2d 6104	. . . 4 ⊢ (𝑥 = 𝑦 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑥))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑦))))
23		mpteq1 4216	. . . . 5 ⊢ (𝑥 = 𝑦 → (𝑗 ∈ 𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) = (𝑗 ∈ 𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))
24	23	oveq2d 6104	. . . 4 ⊢ (𝑥 = 𝑦 → (𝐺 Σg (𝑗 ∈ 𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) = (𝐺 Σg (𝑗 ∈ 𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))))
25	22, 24	eqeq12d 2253	. . 3 ⊢ (𝑥 = 𝑦 → ((𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑥))) = (𝐺 Σg (𝑗 ∈ 𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) ↔ (𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑦))) = (𝐺 Σg (𝑗 ∈ 𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))))
26		reseq2 5060	. . . . . 6 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝐴 ↾ 𝑥) = (𝐴 ↾ (𝑦 ∪ {𝑧})))
27	26	reseq2d 5065	. . . . 5 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝐹 ↾ (𝐴 ↾ 𝑥)) = (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))))
28	27	oveq2d 6104	. . . 4 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑥))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧})))))
29		mpteq1 4216	. . . . 5 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝑗 ∈ 𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) = (𝑗 ∈ (𝑦 ∪ {𝑧}) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))
30	29	oveq2d 6104	. . . 4 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝐺 Σg (𝑗 ∈ 𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) = (𝐺 Σg (𝑗 ∈ (𝑦 ∪ {𝑧}) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))))
31	28, 30	eqeq12d 2253	. . 3 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑥))) = (𝐺 Σg (𝑗 ∈ 𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) ↔ (𝐺 Σg (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧})))) = (𝐺 Σg (𝑗 ∈ (𝑦 ∪ {𝑧}) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))))
32		reseq2 5060	. . . . . 6 ⊢ (𝑥 = dom 𝐴 → (𝐴 ↾ 𝑥) = (𝐴 ↾ dom 𝐴))
33	32	reseq2d 5065	. . . . 5 ⊢ (𝑥 = dom 𝐴 → (𝐹 ↾ (𝐴 ↾ 𝑥)) = (𝐹 ↾ (𝐴 ↾ dom 𝐴)))
34	33	oveq2d 6104	. . . 4 ⊢ (𝑥 = dom 𝐴 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑥))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ dom 𝐴))))
35		mpteq1 4216	. . . . 5 ⊢ (𝑥 = dom 𝐴 → (𝑗 ∈ 𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) = (𝑗 ∈ dom 𝐴 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))
36	35	oveq2d 6104	. . . 4 ⊢ (𝑥 = dom 𝐴 → (𝐺 Σg (𝑗 ∈ 𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) = (𝐺 Σg (𝑗 ∈ dom 𝐴 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))))
37	34, 36	eqeq12d 2253	. . 3 ⊢ (𝑥 = dom 𝐴 → ((𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑥))) = (𝐺 Σg (𝑗 ∈ 𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) ↔ (𝐺 Σg (𝐹 ↾ (𝐴 ↾ dom 𝐴))) = (𝐺 Σg (𝑗 ∈ dom 𝐴 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))))
38		res0 5069	. . . . . . . 8 ⊢ (𝐴 ↾ ∅) = ∅
39	38	reseq2i 5062	. . . . . . 7 ⊢ (𝐹 ↾ (𝐴 ↾ ∅)) = (𝐹 ↾ ∅)
40		res0 5069	. . . . . . 7 ⊢ (𝐹 ↾ ∅) = ∅
41	39, 40	eqtri 2259	. . . . . 6 ⊢ (𝐹 ↾ (𝐴 ↾ ∅)) = ∅
42	41	oveq2i 6099	. . . . 5 ⊢ (𝐺 Σg (𝐹 ↾ (𝐴 ↾ ∅))) = (𝐺 Σg ∅)
43		mpt0 5514	. . . . . 6 ⊢ (𝑗 ∈ ∅ ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) = ∅
44	43	oveq2i 6099	. . . . 5 ⊢ (𝐺 Σg (𝑗 ∈ ∅ ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) = (𝐺 Σg ∅)
45	42, 44	eqtr4i 2262	. . . 4 ⊢ (𝐺 Σg (𝐹 ↾ (𝐴 ↾ ∅))) = (𝐺 Σg (𝑗 ∈ ∅ ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))
46	45	a1i 9	. . 3 ⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ ∅))) = (𝐺 Σg (𝑗 ∈ ∅ ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))))
47		oveq1 6095	. . . 4 ⊢ ((𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑦))) = (𝐺 Σg (𝑗 ∈ 𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) → ((𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑦)))(+g‘𝐺)(𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧})))) = ((𝐺 Σg (𝑗 ∈ 𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))(+g‘𝐺)(𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧})))))
48		gsum2d.b	. . . . . . 7 ⊢ 𝐵 = (Base‘𝐺)
49		gsum2d.z	. . . . . . 7 ⊢ 0 = (0g‘𝐺)
50		eqid 2238	. . . . . . 7 ⊢ (+g‘𝐺) = (+g‘𝐺)
51		gsum2d.g	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ CMnd)
52	51	ad2antrr 492	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ dom 𝐴 ∧ 𝑧 ∈ (dom 𝐴 ∖ 𝑦))) → 𝐺 ∈ CMnd)
53		gsum2dfi.a	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ Fin)
54	53	ad2antrr 492	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ dom 𝐴 ∧ 𝑧 ∈ (dom 𝐴 ∖ 𝑦))) → 𝐴 ∈ Fin)
55	1	ad2antrr 492	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ dom 𝐴 ∧ 𝑧 ∈ (dom 𝐴 ∖ 𝑦))) → Rel 𝐴)
56		gsum2dfi.dm	. . . . . . . . 9 ⊢ (𝜑 → dom 𝐴 ∈ Fin)
57	56	ad2antrr 492	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ dom 𝐴 ∧ 𝑧 ∈ (dom 𝐴 ∖ 𝑦))) → dom 𝐴 ∈ Fin)
58		simprl 535	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ dom 𝐴 ∧ 𝑧 ∈ (dom 𝐴 ∖ 𝑦))) → 𝑦 ⊆ dom 𝐴)
59		simprr 537	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ dom 𝐴 ∧ 𝑧 ∈ (dom 𝐴 ∖ 𝑦))) → 𝑧 ∈ (dom 𝐴 ∖ 𝑦))
60	59	eldifad 3231	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ dom 𝐴 ∧ 𝑧 ∈ (dom 𝐴 ∖ 𝑦))) → 𝑧 ∈ dom 𝐴)
61	60	snssd 3860	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ dom 𝐴 ∧ 𝑧 ∈ (dom 𝐴 ∖ 𝑦))) → {𝑧} ⊆ dom 𝐴)
62	58, 61	unssd 3405	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ dom 𝐴 ∧ 𝑧 ∈ (dom 𝐴 ∖ 𝑦))) → (𝑦 ∪ {𝑧}) ⊆ dom 𝐴)
63		simplr 533	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ dom 𝐴 ∧ 𝑧 ∈ (dom 𝐴 ∖ 𝑦))) → 𝑦 ∈ Fin)
64	59	eldifbd 3232	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ dom 𝐴 ∧ 𝑧 ∈ (dom 𝐴 ∖ 𝑦))) → ¬ 𝑧 ∈ 𝑦)
65		unsnfi 7230	. . . . . . . . 9 ⊢ ((𝑦 ∈ Fin ∧ 𝑧 ∈ dom 𝐴 ∧ ¬ 𝑧 ∈ 𝑦) → (𝑦 ∪ {𝑧}) ∈ Fin)
66	63, 60, 64, 65	syl3anc 1278	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ dom 𝐴 ∧ 𝑧 ∈ (dom 𝐴 ∖ 𝑦))) → (𝑦 ∪ {𝑧}) ∈ Fin)
67	54, 55, 57, 62, 66	relresfin 7268	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ dom 𝐴 ∧ 𝑧 ∈ (dom 𝐴 ∖ 𝑦))) → (𝐴 ↾ (𝑦 ∪ {𝑧})) ∈ Fin)
68		resss 5089	. . . . . . . . 9 ⊢ (𝐴 ↾ (𝑦 ∪ {𝑧})) ⊆ 𝐴
69		fssres 5568	. . . . . . . . 9 ⊢ ((𝐹:𝐴⟶𝐵 ∧ (𝐴 ↾ (𝑦 ∪ {𝑧})) ⊆ 𝐴) → (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))):(𝐴 ↾ (𝑦 ∪ {𝑧}))⟶𝐵)
70	5, 68, 69	sylancl 417	. . . . . . . 8 ⊢ (𝜑 → (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))):(𝐴 ↾ (𝑦 ∪ {𝑧}))⟶𝐵)
71	70	ad2antrr 492	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ dom 𝐴 ∧ 𝑧 ∈ (dom 𝐴 ∖ 𝑦))) → (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))):(𝐴 ↾ (𝑦 ∪ {𝑧}))⟶𝐵)
72		disjsn 3771	. . . . . . . . . 10 ⊢ ((𝑦 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑦)
73	64, 72	sylibr 134	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ dom 𝐴 ∧ 𝑧 ∈ (dom 𝐴 ∖ 𝑦))) → (𝑦 ∩ {𝑧}) = ∅)
74	73	reseq2d 5065	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ dom 𝐴 ∧ 𝑧 ∈ (dom 𝐴 ∖ 𝑦))) → (𝐴 ↾ (𝑦 ∩ {𝑧})) = (𝐴 ↾ ∅))
75		resindi 5080	. . . . . . . 8 ⊢ (𝐴 ↾ (𝑦 ∩ {𝑧})) = ((𝐴 ↾ 𝑦) ∩ (𝐴 ↾ {𝑧}))
76	74, 75, 38	3eqtr3g 2294	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ dom 𝐴 ∧ 𝑧 ∈ (dom 𝐴 ∖ 𝑦))) → ((𝐴 ↾ 𝑦) ∩ (𝐴 ↾ {𝑧})) = ∅)
77		resundi 5078	. . . . . . . 8 ⊢ (𝐴 ↾ (𝑦 ∪ {𝑧})) = ((𝐴 ↾ 𝑦) ∪ (𝐴 ↾ {𝑧}))
78	77	a1i 9	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ dom 𝐴 ∧ 𝑧 ∈ (dom 𝐴 ∖ 𝑦))) → (𝐴 ↾ (𝑦 ∪ {𝑧})) = ((𝐴 ↾ 𝑦) ∪ (𝐴 ↾ {𝑧})))
79	48, 49, 50, 52, 67, 71, 76, 78	gsumsplitfi 14256	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ dom 𝐴 ∧ 𝑧 ∈ (dom 𝐴 ∖ 𝑦))) → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧})))) = ((𝐺 Σg ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ↾ (𝐴 ↾ 𝑦)))(+g‘𝐺)(𝐺 Σg ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ↾ (𝐴 ↾ {𝑧})))))
80		ssun1 3392	. . . . . . . . 9 ⊢ 𝑦 ⊆ (𝑦 ∪ {𝑧})
81		ssres2 5092	. . . . . . . . 9 ⊢ (𝑦 ⊆ (𝑦 ∪ {𝑧}) → (𝐴 ↾ 𝑦) ⊆ (𝐴 ↾ (𝑦 ∪ {𝑧})))
82		resabs1 5094	. . . . . . . . 9 ⊢ ((𝐴 ↾ 𝑦) ⊆ (𝐴 ↾ (𝑦 ∪ {𝑧})) → ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ↾ (𝐴 ↾ 𝑦)) = (𝐹 ↾ (𝐴 ↾ 𝑦)))
83	80, 81, 82	mp2b 8	. . . . . . . 8 ⊢ ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ↾ (𝐴 ↾ 𝑦)) = (𝐹 ↾ (𝐴 ↾ 𝑦))
84	83	oveq2i 6099	. . . . . . 7 ⊢ (𝐺 Σg ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ↾ (𝐴 ↾ 𝑦))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑦)))
85		ssun2 3393	. . . . . . . . 9 ⊢ {𝑧} ⊆ (𝑦 ∪ {𝑧})
86		ssres2 5092	. . . . . . . . 9 ⊢ ({𝑧} ⊆ (𝑦 ∪ {𝑧}) → (𝐴 ↾ {𝑧}) ⊆ (𝐴 ↾ (𝑦 ∪ {𝑧})))
87		resabs1 5094	. . . . . . . . 9 ⊢ ((𝐴 ↾ {𝑧}) ⊆ (𝐴 ↾ (𝑦 ∪ {𝑧})) → ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ↾ (𝐴 ↾ {𝑧})) = (𝐹 ↾ (𝐴 ↾ {𝑧})))
88	85, 86, 87	mp2b 8	. . . . . . . 8 ⊢ ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ↾ (𝐴 ↾ {𝑧})) = (𝐹 ↾ (𝐴 ↾ {𝑧}))
89	88	oveq2i 6099	. . . . . . 7 ⊢ (𝐺 Σg ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ↾ (𝐴 ↾ {𝑧}))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧})))
90	84, 89	oveq12i 6100	. . . . . 6 ⊢ ((𝐺 Σg ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ↾ (𝐴 ↾ 𝑦)))(+g‘𝐺)(𝐺 Σg ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ↾ (𝐴 ↾ {𝑧})))) = ((𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑦)))(+g‘𝐺)(𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧}))))
91	79, 90	eqtrdi 2287	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ dom 𝐴 ∧ 𝑧 ∈ (dom 𝐴 ∖ 𝑦))) → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧})))) = ((𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑦)))(+g‘𝐺)(𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧})))))
92	5	ad2antrr 492	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ dom 𝐴 ∧ 𝑧 ∈ (dom 𝐴 ∖ 𝑦))) → 𝐹:𝐴⟶𝐵)
93		gsum2d.s	. . . . . . . . . . . 12 ⊢ (𝜑 → dom 𝐴 ⊆ 𝐷)
94	93	ad2antrr 492	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ dom 𝐴 ∧ 𝑧 ∈ (dom 𝐴 ∖ 𝑦))) → dom 𝐴 ⊆ 𝐷)
95	58, 94	sstrd 3258	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ dom 𝐴 ∧ 𝑧 ∈ (dom 𝐴 ∖ 𝑦))) → 𝑦 ⊆ 𝐷)
96	95	sselda 3248	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ dom 𝐴 ∧ 𝑧 ∈ (dom 𝐴 ∖ 𝑦))) ∧ 𝑗 ∈ 𝑦) → 𝑗 ∈ 𝐷)
97		gsum2dfi.fi	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐷) → (𝐴 “ {𝑗}) ∈ Fin)
98	97	ad4ant14 518	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ dom 𝐴 ∧ 𝑧 ∈ (dom 𝐴 ∖ 𝑦))) ∧ 𝑗 ∈ 𝐷) → (𝐴 “ {𝑗}) ∈ Fin)
99	96, 98	syldan 282	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ dom 𝐴 ∧ 𝑧 ∈ (dom 𝐴 ∖ 𝑦))) ∧ 𝑗 ∈ 𝑦) → (𝐴 “ {𝑗}) ∈ Fin)
100	48, 49, 52, 92, 99	gsum2dfilem1 14271	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ dom 𝐴 ∧ 𝑧 ∈ (dom 𝐴 ∖ 𝑦))) ∧ 𝑗 ∈ 𝑦) → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) ∈ 𝐵)
101		sneq 3720	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑧 → {𝑗} = {𝑧})
102	101	imaeq2d 5129	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑧 → (𝐴 “ {𝑗}) = (𝐴 “ {𝑧}))
103		oveq1 6095	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑧 → (𝑗𝐹𝑘) = (𝑧𝐹𝑘))
104	102, 103	mpteq12dv 4214	. . . . . . . . . 10 ⊢ (𝑗 = 𝑧 → (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) = (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘)))
105	104	oveq2d 6104	. . . . . . . . 9 ⊢ (𝑗 = 𝑧 → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) = (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘))))
106	105	eleq1d 2307	. . . . . . . 8 ⊢ (𝑗 = 𝑧 → ((𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) ∈ 𝐵 ↔ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘))) ∈ 𝐵))
107	94	sselda 3248	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ dom 𝐴 ∧ 𝑧 ∈ (dom 𝐴 ∖ 𝑦))) ∧ 𝑗 ∈ dom 𝐴) → 𝑗 ∈ 𝐷)
108	107, 98	syldan 282	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ dom 𝐴 ∧ 𝑧 ∈ (dom 𝐴 ∖ 𝑦))) ∧ 𝑗 ∈ dom 𝐴) → (𝐴 “ {𝑗}) ∈ Fin)
109	48, 49, 52, 92, 108	gsum2dfilem1 14271	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ dom 𝐴 ∧ 𝑧 ∈ (dom 𝐴 ∖ 𝑦))) ∧ 𝑗 ∈ dom 𝐴) → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) ∈ 𝐵)
110	109	ralrimiva 2623	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ dom 𝐴 ∧ 𝑧 ∈ (dom 𝐴 ∖ 𝑦))) → ∀𝑗 ∈ dom 𝐴(𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) ∈ 𝐵)
111	106, 110, 60	rspcdva 2934	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ dom 𝐴 ∧ 𝑧 ∈ (dom 𝐴 ∖ 𝑦))) → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘))) ∈ 𝐵)
112	48, 50, 52, 63, 100, 60, 64, 111, 105	gsumunsn 14262	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ dom 𝐴 ∧ 𝑧 ∈ (dom 𝐴 ∖ 𝑦))) → (𝐺 Σg (𝑗 ∈ (𝑦 ∪ {𝑧}) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) = ((𝐺 Σg (𝑗 ∈ 𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))(+g‘𝐺)(𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘)))))
113	101	reseq2d 5065	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑧 → (𝐴 ↾ {𝑗}) = (𝐴 ↾ {𝑧}))
114	113	reseq2d 5065	. . . . . . . . . 10 ⊢ (𝑗 = 𝑧 → (𝐹 ↾ (𝐴 ↾ {𝑗})) = (𝐹 ↾ (𝐴 ↾ {𝑧})))
115	114	oveq2d 6104	. . . . . . . . 9 ⊢ (𝑗 = 𝑧 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑗}))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧}))))
116	105, 115	eqeq12d 2253	. . . . . . . 8 ⊢ (𝑗 = 𝑧 → ((𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑗}))) ↔ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧})))))
117	51	adantr 276	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ dom 𝐴) → 𝐺 ∈ CMnd)
118	93	sselda 3248	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ dom 𝐴) → 𝑗 ∈ 𝐷)
119	118, 97	syldan 282	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ dom 𝐴) → (𝐴 “ {𝑗}) ∈ Fin)
120		vex 2824	. . . . . . . . . . . . . . . 16 ⊢ 𝑗 ∈ V
121		vex 2824	. . . . . . . . . . . . . . . 16 ⊢ 𝑘 ∈ V
122	120, 121	elimasn 5157	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (𝐴 “ {𝑗}) ↔ ⟨𝑗, 𝑘⟩ ∈ 𝐴)
123		df-ov 6091	. . . . . . . . . . . . . . . 16 ⊢ (𝑗𝐹𝑘) = (𝐹‘⟨𝑗, 𝑘⟩)
124	5	ffvelcdmda 5846	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ⟨𝑗, 𝑘⟩ ∈ 𝐴) → (𝐹‘⟨𝑗, 𝑘⟩) ∈ 𝐵)
125	123, 124	eqeltrid 2325	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ⟨𝑗, 𝑘⟩ ∈ 𝐴) → (𝑗𝐹𝑘) ∈ 𝐵)
126	122, 125	sylan2b 287	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 “ {𝑗})) → (𝑗𝐹𝑘) ∈ 𝐵)
127	126	fmpttd 5866	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)):(𝐴 “ {𝑗})⟶𝐵)
128	127	adantr 276	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ dom 𝐴) → (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)):(𝐴 “ {𝑗})⟶𝐵)
129		2ndconst 6462	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ V → (2nd ↾ ({𝑗} × (𝐴 “ {𝑗}))):({𝑗} × (𝐴 “ {𝑗}))–1-1-onto→(𝐴 “ {𝑗}))
130	120, 129	mp1i 10	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ dom 𝐴) → (2nd ↾ ({𝑗} × (𝐴 “ {𝑗}))):({𝑗} × (𝐴 “ {𝑗}))–1-1-onto→(𝐴 “ {𝑗}))
131	48, 49, 117, 119, 128, 130	gsumf1ofi 14250	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ dom 𝐴) → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) = (𝐺 Σg ((𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) ∘ (2nd ↾ ({𝑗} × (𝐴 “ {𝑗}))))))
132		1st2nd2 6413	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) → 𝑥 = ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
133		xp1st 6403	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) → (1st ‘𝑥) ∈ {𝑗})
134		elsni 3727	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1st ‘𝑥) ∈ {𝑗} → (1st ‘𝑥) = 𝑗)
135	133, 134	syl 14	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) → (1st ‘𝑥) = 𝑗)
136	135	opeq1d 3910	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) → ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ = ⟨𝑗, (2nd ‘𝑥)⟩)
137	132, 136	eqtrd 2271	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) → 𝑥 = ⟨𝑗, (2nd ‘𝑥)⟩)
138	137	fveq2d 5702	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) → (𝐹‘𝑥) = (𝐹‘⟨𝑗, (2nd ‘𝑥)⟩))
139		df-ov 6091	. . . . . . . . . . . . . . . 16 ⊢ (𝑗𝐹(2nd ‘𝑥)) = (𝐹‘⟨𝑗, (2nd ‘𝑥)⟩)
140	138, 139	eqtr4di 2289	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) → (𝐹‘𝑥) = (𝑗𝐹(2nd ‘𝑥)))
141	140	mpteq2ia 4219	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) ↦ (𝐹‘𝑥)) = (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) ↦ (𝑗𝐹(2nd ‘𝑥)))
142	5	feqmptd 5759	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
143	142	reseq1d 5064	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹 ↾ (𝐴 ↾ {𝑗})) = ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ↾ (𝐴 ↾ {𝑗})))
144		resss 5089	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ↾ {𝑗}) ⊆ 𝐴
145		resmpt 5114	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ↾ {𝑗}) ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ↾ (𝐴 ↾ {𝑗})) = (𝑥 ∈ (𝐴 ↾ {𝑗}) ↦ (𝐹‘𝑥)))
146	144, 145	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ↾ (𝐴 ↾ {𝑗})) = (𝑥 ∈ (𝐴 ↾ {𝑗}) ↦ (𝐹‘𝑥))
147		ressn 5331	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ↾ {𝑗}) = ({𝑗} × (𝐴 “ {𝑗}))
148	147	mpteq1i 4218	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (𝐴 ↾ {𝑗}) ↦ (𝐹‘𝑥)) = (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) ↦ (𝐹‘𝑥))
149	146, 148	eqtri 2259	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ↾ (𝐴 ↾ {𝑗})) = (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) ↦ (𝐹‘𝑥))
150	143, 149	eqtrdi 2287	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐹 ↾ (𝐴 ↾ {𝑗})) = (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) ↦ (𝐹‘𝑥)))
151		xp2nd 6404	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) → (2nd ‘𝑥) ∈ (𝐴 “ {𝑗}))
152	151	adantl 277	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗}))) → (2nd ‘𝑥) ∈ (𝐴 “ {𝑗}))
153		fo2nd 6396	. . . . . . . . . . . . . . . . . . 19 ⊢ 2nd :V–onto→V
154		fof 5618	. . . . . . . . . . . . . . . . . . 19 ⊢ (2nd :V–onto→V → 2nd :V⟶V)
155	153, 154	mp1i 10	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 2nd :V⟶V)
156	155	feqmptd 5759	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 2nd = (𝑥 ∈ V ↦ (2nd ‘𝑥)))
157	156	reseq1d 5064	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2nd ↾ ({𝑗} × (𝐴 “ {𝑗}))) = ((𝑥 ∈ V ↦ (2nd ‘𝑥)) ↾ ({𝑗} × (𝐴 “ {𝑗}))))
158		ssv 3270	. . . . . . . . . . . . . . . . 17 ⊢ ({𝑗} × (𝐴 “ {𝑗})) ⊆ V
159		resmpt 5114	. . . . . . . . . . . . . . . . 17 ⊢ (({𝑗} × (𝐴 “ {𝑗})) ⊆ V → ((𝑥 ∈ V ↦ (2nd ‘𝑥)) ↾ ({𝑗} × (𝐴 “ {𝑗}))) = (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) ↦ (2nd ‘𝑥)))
160	158, 159	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ V ↦ (2nd ‘𝑥)) ↾ ({𝑗} × (𝐴 “ {𝑗}))) = (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) ↦ (2nd ‘𝑥))
161	157, 160	eqtrdi 2287	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2nd ↾ ({𝑗} × (𝐴 “ {𝑗}))) = (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) ↦ (2nd ‘𝑥)))
162		eqidd 2239	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) = (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))
163		oveq2 6096	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = (2nd ‘𝑥) → (𝑗𝐹𝑘) = (𝑗𝐹(2nd ‘𝑥)))
164	152, 161, 162, 163	fmptco 5877	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) ∘ (2nd ↾ ({𝑗} × (𝐴 “ {𝑗})))) = (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) ↦ (𝑗𝐹(2nd ‘𝑥))))
165	141, 150, 164	3eqtr4a 2297	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐹 ↾ (𝐴 ↾ {𝑗})) = ((𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) ∘ (2nd ↾ ({𝑗} × (𝐴 “ {𝑗})))))
166	165	oveq2d 6104	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑗}))) = (𝐺 Σg ((𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) ∘ (2nd ↾ ({𝑗} × (𝐴 “ {𝑗}))))))
167	166	adantr 276	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ dom 𝐴) → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑗}))) = (𝐺 Σg ((𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) ∘ (2nd ↾ ({𝑗} × (𝐴 “ {𝑗}))))))
168	131, 167	eqtr4d 2274	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ dom 𝐴) → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑗}))))
169	168	ralrimiva 2623	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑗 ∈ dom 𝐴(𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑗}))))
170	169	ad2antrr 492	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ dom 𝐴 ∧ 𝑧 ∈ (dom 𝐴 ∖ 𝑦))) → ∀𝑗 ∈ dom 𝐴(𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑗}))))
171	116, 170, 60	rspcdva 2934	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ dom 𝐴 ∧ 𝑧 ∈ (dom 𝐴 ∖ 𝑦))) → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧}))))
172	171	oveq2d 6104	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ dom 𝐴 ∧ 𝑧 ∈ (dom 𝐴 ∖ 𝑦))) → ((𝐺 Σg (𝑗 ∈ 𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))(+g‘𝐺)(𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘)))) = ((𝐺 Σg (𝑗 ∈ 𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))(+g‘𝐺)(𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧})))))
173	112, 172	eqtrd 2271	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ dom 𝐴 ∧ 𝑧 ∈ (dom 𝐴 ∖ 𝑦))) → (𝐺 Σg (𝑗 ∈ (𝑦 ∪ {𝑧}) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) = ((𝐺 Σg (𝑗 ∈ 𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))(+g‘𝐺)(𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧})))))
174	91, 173	eqeq12d 2253	. . . 4 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ dom 𝐴 ∧ 𝑧 ∈ (dom 𝐴 ∖ 𝑦))) → ((𝐺 Σg (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧})))) = (𝐺 Σg (𝑗 ∈ (𝑦 ∪ {𝑧}) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) ↔ ((𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑦)))(+g‘𝐺)(𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧})))) = ((𝐺 Σg (𝑗 ∈ 𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))(+g‘𝐺)(𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧}))))))
175	47, 174	imbitrrid 156	. . 3 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ dom 𝐴 ∧ 𝑧 ∈ (dom 𝐴 ∖ 𝑦))) → ((𝐺 Σg (𝐹 ↾ (𝐴 ↾ 𝑦))) = (𝐺 Σg (𝑗 ∈ 𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧})))) = (𝐺 Σg (𝑗 ∈ (𝑦 ∪ {𝑧}) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))))
176	19, 25, 31, 37, 46, 175, 56	findcard2sd 7200	. 2 ⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ dom 𝐴))) = (𝐺 Σg (𝑗 ∈ dom 𝐴 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))))
177	13, 176	eqtr3d 2273	1 ⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐺 Σg (𝑗 ∈ dom 𝐴 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 104   = wceq 1402   ∈ wcel 2209  ∀wral 2528  Vcvv 2821   ∖ cdif 3217   ∪ cun 3218   ∩ cin 3219   ⊆ wss 3220  ∅c0 3520  {csn 3709  ⟨cop 3712   ↦ cmpt 4193   × cxp 4774  dom cdm 4776   ↾ cres 4778   “ cima 4779   ∘ ccom 4780  Rel wrel 4781  ⟶wf 5376  –onto→wfo 5378  –1-1-onto→wf1o 5379  ‘cfv 5380  (class class class)co 6088  1^st c1st 6376  2^nd c2nd 6377  Fincfn 7026  Basecbs 13410  +_gcplusg 13490  0_gc0g 13669  CMndccmn 14177   Σ_g cgsu 14240

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-coll 4248  ax-sep 4251  ax-nul 4261  ax-pow 4313  ax-pr 4348  ax-un 4580  ax-setind 4686  ax-iinf 4737  ax-cnex 8276  ax-resscn 8277  ax-1cn 8278  ax-1re 8279  ax-icn 8280  ax-addcl 8281  ax-addrcl 8282  ax-mulcl 8283  ax-mulrcl 8284  ax-addcom 8285  ax-mulcom 8286  ax-addass 8287  ax-mulass 8288  ax-distr 8289  ax-i2m1 8290  ax-0lt1 8291  ax-1rid 8292  ax-0id 8293  ax-rnegex 8294  ax-precex 8295  ax-cnre 8296  ax-pre-ltirr 8297  ax-pre-ltwlin 8298  ax-pre-lttrn 8299  ax-pre-apti 8300  ax-pre-ltadd 8301  ax-pre-mulgt0 8302

This proof depends on definitions:  df-bi 117  df-stab 843  df-dc 847  df-3or 1010  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-nel 2516  df-ral 2533  df-rex 2534  df-reu 2535  df-rmo 2536  df-rab 2537  df-v 2823  df-sbc 3052  df-csb 3148  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-nul 3521  df-if 3639  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-int 3971  df-iun 4014  df-br 4132  df-opab 4194  df-mpt 4195  df-tr 4232  df-id 4440  df-iord 4513  df-on 4515  df-ilim 4516  df-suc 4518  df-iom 4740  df-xp 4782  df-rel 4783  df-cnv 4784  df-co 4785  df-dm 4786  df-rn 4787  df-res 4788  df-ima 4789  df-iota 5340  df-fun 5382  df-fn 5383  df-f 5384  df-f1 5385  df-fo 5386  df-f1o 5387  df-fv 5388  df-riota 6041  df-ov 6091  df-oprab 6092  df-mpo 6093  df-1st 6378  df-2nd 6379  df-recs 6580  df-irdg 6645  df-frec 6666  df-1o 6691  df-oadd 6695  df-er 6811  df-en 7027  df-dom 7028  df-fin 7029  df-pnf 8368  df-mnf 8369  df-xr 8370  df-ltxr 8371  df-le 8372  df-sub 8506  df-neg 8507  df-reap 8911  df-ap 8918  df-inn 9314  df-2 9372  df-n0 9575  df-z 9656  df-uz 9938  df-fz 10429  df-fzo 10567  df-seqfrec 10906  df-ihash 11237  df-ndx 13413  df-slot 13414  df-base 13416  df-plusg 13503  df-0g 13671  df-gzsum 13672  df-mgm 13735  df-sgrp 13776  df-mnd 13789  df-minusg 13868  df-mulg 13982  df-cmn 14179  df-gsumfi 14241

This theorem is used by:  gsum2dfi  14273