Theorem gsumzaddlem 18321

Description: The sum of two group sums. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 5-Jun-2019.)

Hypotheses

Ref	Expression
gsumzadd.b	⊢ 𝐵 = (Base‘𝐺)
gsumzadd.0	⊢ 0 = (0g‘𝐺)
gsumzadd.p	⊢ + = (+g‘𝐺)
gsumzadd.z	⊢ 𝑍 = (Cntz‘𝐺)
gsumzadd.g	⊢ (𝜑 → 𝐺 ∈ Mnd)
gsumzadd.a	⊢ (𝜑 → 𝐴 ∈ 𝑉)
gsumzadd.fn	⊢ (𝜑 → 𝐹 finSupp 0 )
gsumzadd.hn	⊢ (𝜑 → 𝐻 finSupp 0 )
gsumzaddlem.w	⊢ 𝑊 = ((𝐹 ∪ 𝐻) supp 0 )
gsumzaddlem.f	⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
gsumzaddlem.h	⊢ (𝜑 → 𝐻:𝐴⟶𝐵)
gsumzaddlem.1	⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
gsumzaddlem.2	⊢ (𝜑 → ran 𝐻 ⊆ (𝑍‘ran 𝐻))
gsumzaddlem.3	⊢ (𝜑 → ran (𝐹 ∘𝑓 + 𝐻) ⊆ (𝑍‘ran (𝐹 ∘𝑓 + 𝐻)))
gsumzaddlem.4	⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → (𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))}))

Assertion

Ref	Expression
gsumzaddlem	⊢ (𝜑 → (𝐺 Σg (𝐹 ∘𝑓 + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)))

Distinct variable groups:   𝑥,𝑘, +   0 ,𝑘,𝑥   𝑘,𝐹,𝑥   𝑘,𝐺,𝑥   𝐴,𝑘,𝑥   𝐵,𝑘,𝑥   𝑘,𝐻,𝑥   𝜑,𝑘,𝑥   𝑥,𝑉   𝑘,𝑊,𝑥   𝑘,𝑍,𝑥

Allowed substitution hint:   𝑉(𝑘)

Proof of Theorem gsumzaddlem

Dummy variables 𝑓 𝑛 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		gsumzadd.g	. . . . . 6 ⊢ (𝜑 → 𝐺 ∈ Mnd)
2		gsumzadd.b	. . . . . . . 8 ⊢ 𝐵 = (Base‘𝐺)
3		gsumzadd.0	. . . . . . . 8 ⊢ 0 = (0g‘𝐺)
4	2, 3	mndidcl 17308	. . . . . . 7 ⊢ (𝐺 ∈ Mnd → 0 ∈ 𝐵)
5	1, 4	syl 17	. . . . . 6 ⊢ (𝜑 → 0 ∈ 𝐵)
6		gsumzadd.p	. . . . . . 7 ⊢ + = (+g‘𝐺)
7	2, 6, 3	mndlid 17311	. . . . . 6 ⊢ ((𝐺 ∈ Mnd ∧ 0 ∈ 𝐵) → ( 0 + 0 ) = 0 )
8	1, 5, 7	syl2anc 693	. . . . 5 ⊢ (𝜑 → ( 0 + 0 ) = 0 )
9	8	adantr 481	. . . 4 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ( 0 + 0 ) = 0 )
10		gsumzaddlem.f	. . . . . . . 8 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
11		gsumzadd.a	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
12		fvex 6201	. . . . . . . . . 10 ⊢ (0g‘𝐺) ∈ V
13	3, 12	eqeltri 2697	. . . . . . . . 9 ⊢ 0 ∈ V
14	13	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 0 ∈ V)
15		gsumzaddlem.h	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐻:𝐴⟶𝐵)
16		fex 6490	. . . . . . . . . . 11 ⊢ ((𝐻:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉) → 𝐻 ∈ V)
17	15, 11, 16	syl2anc 693	. . . . . . . . . 10 ⊢ (𝜑 → 𝐻 ∈ V)
18	17	suppun 7315	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 supp 0 ) ⊆ ((𝐹 ∪ 𝐻) supp 0 ))
19		gsumzaddlem.w	. . . . . . . . 9 ⊢ 𝑊 = ((𝐹 ∪ 𝐻) supp 0 )
20	18, 19	syl6sseqr 3652	. . . . . . . 8 ⊢ (𝜑 → (𝐹 supp 0 ) ⊆ 𝑊)
21	10, 11, 14, 20	gsumcllem 18309	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐹 = (𝑥 ∈ 𝐴 ↦ 0 ))
22	21	oveq2d 6666	. . . . . 6 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg 𝐹) = (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 )))
23	3	gsumz 17374	. . . . . . . 8 ⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 )) = 0 )
24	1, 11, 23	syl2anc 693	. . . . . . 7 ⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 )) = 0 )
25	24	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 )) = 0 )
26	22, 25	eqtrd 2656	. . . . 5 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg 𝐹) = 0 )
27		fex 6490	. . . . . . . . . . . 12 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉) → 𝐹 ∈ V)
28	10, 11, 27	syl2anc 693	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ V)
29	28	suppun 7315	. . . . . . . . . 10 ⊢ (𝜑 → (𝐻 supp 0 ) ⊆ ((𝐻 ∪ 𝐹) supp 0 ))
30		uncom 3757	. . . . . . . . . . 11 ⊢ (𝐹 ∪ 𝐻) = (𝐻 ∪ 𝐹)
31	30	oveq1i 6660	. . . . . . . . . 10 ⊢ ((𝐹 ∪ 𝐻) supp 0 ) = ((𝐻 ∪ 𝐹) supp 0 )
32	29, 31	syl6sseqr 3652	. . . . . . . . 9 ⊢ (𝜑 → (𝐻 supp 0 ) ⊆ ((𝐹 ∪ 𝐻) supp 0 ))
33	32, 19	syl6sseqr 3652	. . . . . . . 8 ⊢ (𝜑 → (𝐻 supp 0 ) ⊆ 𝑊)
34	15, 11, 14, 33	gsumcllem 18309	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐻 = (𝑥 ∈ 𝐴 ↦ 0 ))
35	34	oveq2d 6666	. . . . . 6 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg 𝐻) = (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 )))
36	35, 25	eqtrd 2656	. . . . 5 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg 𝐻) = 0 )
37	26, 36	oveq12d 6668	. . . 4 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)) = ( 0 + 0 ))
38	11	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐴 ∈ 𝑉)
39	5	ad2antrr 762	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ 𝐴) → 0 ∈ 𝐵)
40	38, 39, 39, 21, 34	offval2 6914	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐹 ∘𝑓 + 𝐻) = (𝑥 ∈ 𝐴 ↦ ( 0 + 0 )))
41	9	mpteq2dv 4745	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝑥 ∈ 𝐴 ↦ ( 0 + 0 )) = (𝑥 ∈ 𝐴 ↦ 0 ))
42	40, 41	eqtrd 2656	. . . . . 6 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐹 ∘𝑓 + 𝐻) = (𝑥 ∈ 𝐴 ↦ 0 ))
43	42	oveq2d 6666	. . . . 5 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg (𝐹 ∘𝑓 + 𝐻)) = (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 )))
44	43, 25	eqtrd 2656	. . . 4 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg (𝐹 ∘𝑓 + 𝐻)) = 0 )
45	9, 37, 44	3eqtr4rd 2667	. . 3 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg (𝐹 ∘𝑓 + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)))
46	45	ex 450	. 2 ⊢ (𝜑 → (𝑊 = ∅ → (𝐺 Σg (𝐹 ∘𝑓 + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))))
47	1	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → 𝐺 ∈ Mnd)
48	2, 6	mndcl 17301	. . . . . . . . . 10 ⊢ ((𝐺 ∈ Mnd ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) → (𝑧 + 𝑤) ∈ 𝐵)
49	48	3expb 1266	. . . . . . . . 9 ⊢ ((𝐺 ∈ Mnd ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (𝑧 + 𝑤) ∈ 𝐵)
50	47, 49	sylan 488	. . . . . . . 8 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (𝑧 + 𝑤) ∈ 𝐵)
51	50	caovclg 6826	. . . . . . 7 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) ∈ 𝐵)
52		simprl 794	. . . . . . . 8 ⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → (#‘𝑊) ∈ ℕ)
53		nnuz 11723	. . . . . . . 8 ⊢ ℕ = (ℤ≥‘1)
54	52, 53	syl6eleq 2711	. . . . . . 7 ⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → (#‘𝑊) ∈ (ℤ≥‘1))
55	10	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → 𝐹:𝐴⟶𝐵)
56		f1of1 6136	. . . . . . . . . . . 12 ⊢ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 → 𝑓:(1...(#‘𝑊))–1-1→𝑊)
57	56	ad2antll 765	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → 𝑓:(1...(#‘𝑊))–1-1→𝑊)
58		suppssdm 7308	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∪ 𝐻) supp 0 ) ⊆ dom (𝐹 ∪ 𝐻)
59	58	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐹 ∪ 𝐻) supp 0 ) ⊆ dom (𝐹 ∪ 𝐻))
60	19	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑊 = ((𝐹 ∪ 𝐻) supp 0 ))
61		dmun 5331	. . . . . . . . . . . . . 14 ⊢ dom (𝐹 ∪ 𝐻) = (dom 𝐹 ∪ dom 𝐻)
62		fdm 6051	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴)
63	10, 62	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → dom 𝐹 = 𝐴)
64		fdm 6051	. . . . . . . . . . . . . . . . 17 ⊢ (𝐻:𝐴⟶𝐵 → dom 𝐻 = 𝐴)
65	15, 64	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → dom 𝐻 = 𝐴)
66	63, 65	uneq12d 3768	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (dom 𝐹 ∪ dom 𝐻) = (𝐴 ∪ 𝐴))
67		unidm 3756	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∪ 𝐴) = 𝐴
68	66, 67	syl6eq 2672	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (dom 𝐹 ∪ dom 𝐻) = 𝐴)
69	61, 68	syl5req 2669	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 = dom (𝐹 ∪ 𝐻))
70	59, 60, 69	3sstr4d 3648	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑊 ⊆ 𝐴)
71	70	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → 𝑊 ⊆ 𝐴)
72		f1ss 6106	. . . . . . . . . . 11 ⊢ ((𝑓:(1...(#‘𝑊))–1-1→𝑊 ∧ 𝑊 ⊆ 𝐴) → 𝑓:(1...(#‘𝑊))–1-1→𝐴)
73	57, 71, 72	syl2anc 693	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → 𝑓:(1...(#‘𝑊))–1-1→𝐴)
74		f1f 6101	. . . . . . . . . 10 ⊢ (𝑓:(1...(#‘𝑊))–1-1→𝐴 → 𝑓:(1...(#‘𝑊))⟶𝐴)
75	73, 74	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → 𝑓:(1...(#‘𝑊))⟶𝐴)
76		fco 6058	. . . . . . . . 9 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑓:(1...(#‘𝑊))⟶𝐴) → (𝐹 ∘ 𝑓):(1...(#‘𝑊))⟶𝐵)
77	55, 75, 76	syl2anc 693	. . . . . . . 8 ⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → (𝐹 ∘ 𝑓):(1...(#‘𝑊))⟶𝐵)
78	77	ffvelrnda 6359	. . . . . . 7 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → ((𝐹 ∘ 𝑓)‘𝑘) ∈ 𝐵)
79	15	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → 𝐻:𝐴⟶𝐵)
80		fco 6058	. . . . . . . . 9 ⊢ ((𝐻:𝐴⟶𝐵 ∧ 𝑓:(1...(#‘𝑊))⟶𝐴) → (𝐻 ∘ 𝑓):(1...(#‘𝑊))⟶𝐵)
81	79, 75, 80	syl2anc 693	. . . . . . . 8 ⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → (𝐻 ∘ 𝑓):(1...(#‘𝑊))⟶𝐵)
82	81	ffvelrnda 6359	. . . . . . 7 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → ((𝐻 ∘ 𝑓)‘𝑘) ∈ 𝐵)
83	55	ffnd 6046	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → 𝐹 Fn 𝐴)
84	79	ffnd 6046	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → 𝐻 Fn 𝐴)
85	11	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → 𝐴 ∈ 𝑉)
86		ovexd 6680	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → (1...(#‘𝑊)) ∈ V)
87		inidm 3822	. . . . . . . . . . 11 ⊢ (𝐴 ∩ 𝐴) = 𝐴
88	83, 84, 75, 85, 85, 86, 87	ofco 6917	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → ((𝐹 ∘𝑓 + 𝐻) ∘ 𝑓) = ((𝐹 ∘ 𝑓) ∘𝑓 + (𝐻 ∘ 𝑓)))
89	88	fveq1d 6193	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → (((𝐹 ∘𝑓 + 𝐻) ∘ 𝑓)‘𝑘) = (((𝐹 ∘ 𝑓) ∘𝑓 + (𝐻 ∘ 𝑓))‘𝑘))
90	89	adantr 481	. . . . . . . 8 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → (((𝐹 ∘𝑓 + 𝐻) ∘ 𝑓)‘𝑘) = (((𝐹 ∘ 𝑓) ∘𝑓 + (𝐻 ∘ 𝑓))‘𝑘))
91		fnfco 6069	. . . . . . . . . 10 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑓:(1...(#‘𝑊))⟶𝐴) → (𝐹 ∘ 𝑓) Fn (1...(#‘𝑊)))
92	83, 75, 91	syl2anc 693	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → (𝐹 ∘ 𝑓) Fn (1...(#‘𝑊)))
93		fnfco 6069	. . . . . . . . . 10 ⊢ ((𝐻 Fn 𝐴 ∧ 𝑓:(1...(#‘𝑊))⟶𝐴) → (𝐻 ∘ 𝑓) Fn (1...(#‘𝑊)))
94	84, 75, 93	syl2anc 693	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → (𝐻 ∘ 𝑓) Fn (1...(#‘𝑊)))
95		inidm 3822	. . . . . . . . 9 ⊢ ((1...(#‘𝑊)) ∩ (1...(#‘𝑊))) = (1...(#‘𝑊))
96		eqidd 2623	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → ((𝐹 ∘ 𝑓)‘𝑘) = ((𝐹 ∘ 𝑓)‘𝑘))
97		eqidd 2623	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → ((𝐻 ∘ 𝑓)‘𝑘) = ((𝐻 ∘ 𝑓)‘𝑘))
98	92, 94, 86, 86, 95, 96, 97	ofval 6906	. . . . . . . 8 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → (((𝐹 ∘ 𝑓) ∘𝑓 + (𝐻 ∘ 𝑓))‘𝑘) = (((𝐹 ∘ 𝑓)‘𝑘) + ((𝐻 ∘ 𝑓)‘𝑘)))
99	90, 98	eqtrd 2656	. . . . . . 7 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑘 ∈ (1...(#‘𝑊))) → (((𝐹 ∘𝑓 + 𝐻) ∘ 𝑓)‘𝑘) = (((𝐹 ∘ 𝑓)‘𝑘) + ((𝐻 ∘ 𝑓)‘𝑘)))
100	1	ad2antrr 762	. . . . . . . 8 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → 𝐺 ∈ Mnd)
101		elfzouz 12474	. . . . . . . . . 10 ⊢ (𝑛 ∈ (1..^(#‘𝑊)) → 𝑛 ∈ (ℤ≥‘1))
102	101	adantl 482	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → 𝑛 ∈ (ℤ≥‘1))
103		elfzouz2 12484	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (1..^(#‘𝑊)) → (#‘𝑊) ∈ (ℤ≥‘𝑛))
104	103	adantl 482	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (#‘𝑊) ∈ (ℤ≥‘𝑛))
105		fzss2 12381	. . . . . . . . . . . 12 ⊢ ((#‘𝑊) ∈ (ℤ≥‘𝑛) → (1...𝑛) ⊆ (1...(#‘𝑊)))
106	104, 105	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (1...𝑛) ⊆ (1...(#‘𝑊)))
107	106	sselda 3603	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ (1...(#‘𝑊)))
108	78	adantlr 751	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) ∧ 𝑘 ∈ (1...(#‘𝑊))) → ((𝐹 ∘ 𝑓)‘𝑘) ∈ 𝐵)
109	107, 108	syldan 487	. . . . . . . . 9 ⊢ ((((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐹 ∘ 𝑓)‘𝑘) ∈ 𝐵)
110	2, 6	mndcl 17301	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ Mnd ∧ 𝑘 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵) → (𝑘 + 𝑥) ∈ 𝐵)
111	110	3expb 1266	. . . . . . . . . 10 ⊢ ((𝐺 ∈ Mnd ∧ (𝑘 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) → (𝑘 + 𝑥) ∈ 𝐵)
112	100, 111	sylan 488	. . . . . . . . 9 ⊢ ((((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) ∧ (𝑘 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) → (𝑘 + 𝑥) ∈ 𝐵)
113	102, 109, 112	seqcl 12821	. . . . . . . 8 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (seq1( + , (𝐹 ∘ 𝑓))‘𝑛) ∈ 𝐵)
114	82	adantlr 751	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) ∧ 𝑘 ∈ (1...(#‘𝑊))) → ((𝐻 ∘ 𝑓)‘𝑘) ∈ 𝐵)
115	107, 114	syldan 487	. . . . . . . . 9 ⊢ ((((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐻 ∘ 𝑓)‘𝑘) ∈ 𝐵)
116	102, 115, 112	seqcl 12821	. . . . . . . 8 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (seq1( + , (𝐻 ∘ 𝑓))‘𝑛) ∈ 𝐵)
117		fzofzp1 12565	. . . . . . . . 9 ⊢ (𝑛 ∈ (1..^(#‘𝑊)) → (𝑛 + 1) ∈ (1...(#‘𝑊)))
118		ffvelrn 6357	. . . . . . . . 9 ⊢ (((𝐹 ∘ 𝑓):(1...(#‘𝑊))⟶𝐵 ∧ (𝑛 + 1) ∈ (1...(#‘𝑊))) → ((𝐹 ∘ 𝑓)‘(𝑛 + 1)) ∈ 𝐵)
119	77, 117, 118	syl2an 494	. . . . . . . 8 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ((𝐹 ∘ 𝑓)‘(𝑛 + 1)) ∈ 𝐵)
120		ffvelrn 6357	. . . . . . . . 9 ⊢ (((𝐻 ∘ 𝑓):(1...(#‘𝑊))⟶𝐵 ∧ (𝑛 + 1) ∈ (1...(#‘𝑊))) → ((𝐻 ∘ 𝑓)‘(𝑛 + 1)) ∈ 𝐵)
121	81, 117, 120	syl2an 494	. . . . . . . 8 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ((𝐻 ∘ 𝑓)‘(𝑛 + 1)) ∈ 𝐵)
122		fvco3 6275	. . . . . . . . . . . 12 ⊢ ((𝑓:(1...(#‘𝑊))⟶𝐴 ∧ (𝑛 + 1) ∈ (1...(#‘𝑊))) → ((𝐹 ∘ 𝑓)‘(𝑛 + 1)) = (𝐹‘(𝑓‘(𝑛 + 1))))
123	75, 117, 122	syl2an 494	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ((𝐹 ∘ 𝑓)‘(𝑛 + 1)) = (𝐹‘(𝑓‘(𝑛 + 1))))
124		fveq2 6191	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑓‘(𝑛 + 1)) → (𝐹‘𝑘) = (𝐹‘(𝑓‘(𝑛 + 1))))
125	124	eleq1d 2686	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑓‘(𝑛 + 1)) → ((𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}) ↔ (𝐹‘(𝑓‘(𝑛 + 1))) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})))
126		gsumzaddlem.4	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → (𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))}))
127	126	expr 643	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐴) → (𝑘 ∈ (𝐴 ∖ 𝑥) → (𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))})))
128	127	ralrimiv 2965	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐴) → ∀𝑘 ∈ (𝐴 ∖ 𝑥)(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))}))
129	128	ex 450	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑥 ⊆ 𝐴 → ∀𝑘 ∈ (𝐴 ∖ 𝑥)(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))})))
130	129	alrimiv 1855	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑥(𝑥 ⊆ 𝐴 → ∀𝑘 ∈ (𝐴 ∖ 𝑥)(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))})))
131	130	ad2antrr 762	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ∀𝑥(𝑥 ⊆ 𝐴 → ∀𝑘 ∈ (𝐴 ∖ 𝑥)(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))})))
132		imassrn 5477	. . . . . . . . . . . . . 14 ⊢ (𝑓 “ (1...𝑛)) ⊆ ran 𝑓
133	75	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → 𝑓:(1...(#‘𝑊))⟶𝐴)
134		frn 6053	. . . . . . . . . . . . . . 15 ⊢ (𝑓:(1...(#‘𝑊))⟶𝐴 → ran 𝑓 ⊆ 𝐴)
135	133, 134	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ran 𝑓 ⊆ 𝐴)
136	132, 135	syl5ss 3614	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (𝑓 “ (1...𝑛)) ⊆ 𝐴)
137		vex 3203	. . . . . . . . . . . . . . 15 ⊢ 𝑓 ∈ V
138	137	imaex 7104	. . . . . . . . . . . . . 14 ⊢ (𝑓 “ (1...𝑛)) ∈ V
139		sseq1 3626	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝑓 “ (1...𝑛)) → (𝑥 ⊆ 𝐴 ↔ (𝑓 “ (1...𝑛)) ⊆ 𝐴))
140		difeq2 3722	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝑓 “ (1...𝑛)) → (𝐴 ∖ 𝑥) = (𝐴 ∖ (𝑓 “ (1...𝑛))))
141		reseq2 5391	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (𝑓 “ (1...𝑛)) → (𝐻 ↾ 𝑥) = (𝐻 ↾ (𝑓 “ (1...𝑛))))
142	141	oveq2d 6666	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (𝑓 “ (1...𝑛)) → (𝐺 Σg (𝐻 ↾ 𝑥)) = (𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛)))))
143	142	sneqd 4189	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = (𝑓 “ (1...𝑛)) → {(𝐺 Σg (𝐻 ↾ 𝑥))} = {(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})
144	143	fveq2d 6195	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (𝑓 “ (1...𝑛)) → (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))}) = (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}))
145	144	eleq2d 2687	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝑓 “ (1...𝑛)) → ((𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))}) ↔ (𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})))
146	140, 145	raleqbidv 3152	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝑓 “ (1...𝑛)) → (∀𝑘 ∈ (𝐴 ∖ 𝑥)(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))}) ↔ ∀𝑘 ∈ (𝐴 ∖ (𝑓 “ (1...𝑛)))(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})))
147	139, 146	imbi12d 334	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑓 “ (1...𝑛)) → ((𝑥 ⊆ 𝐴 → ∀𝑘 ∈ (𝐴 ∖ 𝑥)(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))})) ↔ ((𝑓 “ (1...𝑛)) ⊆ 𝐴 → ∀𝑘 ∈ (𝐴 ∖ (𝑓 “ (1...𝑛)))(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}))))
148	138, 147	spcv 3299	. . . . . . . . . . . . 13 ⊢ (∀𝑥(𝑥 ⊆ 𝐴 → ∀𝑘 ∈ (𝐴 ∖ 𝑥)(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))})) → ((𝑓 “ (1...𝑛)) ⊆ 𝐴 → ∀𝑘 ∈ (𝐴 ∖ (𝑓 “ (1...𝑛)))(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})))
149	131, 136, 148	sylc 65	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ∀𝑘 ∈ (𝐴 ∖ (𝑓 “ (1...𝑛)))(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}))
150		ffvelrn 6357	. . . . . . . . . . . . . 14 ⊢ ((𝑓:(1...(#‘𝑊))⟶𝐴 ∧ (𝑛 + 1) ∈ (1...(#‘𝑊))) → (𝑓‘(𝑛 + 1)) ∈ 𝐴)
151	75, 117, 150	syl2an 494	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (𝑓‘(𝑛 + 1)) ∈ 𝐴)
152		fzp1nel 12424	. . . . . . . . . . . . . 14 ⊢ ¬ (𝑛 + 1) ∈ (1...𝑛)
153	73	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → 𝑓:(1...(#‘𝑊))–1-1→𝐴)
154	117	adantl 482	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (𝑛 + 1) ∈ (1...(#‘𝑊)))
155		f1elima 6520	. . . . . . . . . . . . . . 15 ⊢ ((𝑓:(1...(#‘𝑊))–1-1→𝐴 ∧ (𝑛 + 1) ∈ (1...(#‘𝑊)) ∧ (1...𝑛) ⊆ (1...(#‘𝑊))) → ((𝑓‘(𝑛 + 1)) ∈ (𝑓 “ (1...𝑛)) ↔ (𝑛 + 1) ∈ (1...𝑛)))
156	153, 154, 106, 155	syl3anc 1326	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ((𝑓‘(𝑛 + 1)) ∈ (𝑓 “ (1...𝑛)) ↔ (𝑛 + 1) ∈ (1...𝑛)))
157	152, 156	mtbiri 317	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ¬ (𝑓‘(𝑛 + 1)) ∈ (𝑓 “ (1...𝑛)))
158	151, 157	eldifd 3585	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (𝑓‘(𝑛 + 1)) ∈ (𝐴 ∖ (𝑓 “ (1...𝑛))))
159	125, 149, 158	rspcdva 3316	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (𝐹‘(𝑓‘(𝑛 + 1))) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}))
160	123, 159	eqeltrd 2701	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ((𝐹 ∘ 𝑓)‘(𝑛 + 1)) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}))
161		gsumzadd.z	. . . . . . . . . . . . 13 ⊢ 𝑍 = (Cntz‘𝐺)
162	138	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (𝑓 “ (1...𝑛)) ∈ V)
163	15	ad2antrr 762	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → 𝐻:𝐴⟶𝐵)
164	163, 136	fssresd 6071	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (𝐻 ↾ (𝑓 “ (1...𝑛))):(𝑓 “ (1...𝑛))⟶𝐵)
165		gsumzaddlem.2	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ran 𝐻 ⊆ (𝑍‘ran 𝐻))
166	165	ad2antrr 762	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ran 𝐻 ⊆ (𝑍‘ran 𝐻))
167		resss 5422	. . . . . . . . . . . . . . 15 ⊢ (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ 𝐻
168		rnss 5354	. . . . . . . . . . . . . . 15 ⊢ ((𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ 𝐻 → ran (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ ran 𝐻)
169	167, 168	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ran (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ ran 𝐻
170	161	cntzidss 17770	. . . . . . . . . . . . . 14 ⊢ ((ran 𝐻 ⊆ (𝑍‘ran 𝐻) ∧ ran (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ ran 𝐻) → ran (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ (𝑍‘ran (𝐻 ↾ (𝑓 “ (1...𝑛)))))
171	166, 169, 170	sylancl 694	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ran (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ (𝑍‘ran (𝐻 ↾ (𝑓 “ (1...𝑛)))))
172	102, 53	syl6eleqr 2712	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → 𝑛 ∈ ℕ)
173		f1ores 6151	. . . . . . . . . . . . . . 15 ⊢ ((𝑓:(1...(#‘𝑊))–1-1→𝐴 ∧ (1...𝑛) ⊆ (1...(#‘𝑊))) → (𝑓 ↾ (1...𝑛)):(1...𝑛)–1-1-onto→(𝑓 “ (1...𝑛)))
174	153, 106, 173	syl2anc 693	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (𝑓 ↾ (1...𝑛)):(1...𝑛)–1-1-onto→(𝑓 “ (1...𝑛)))
175		f1of1 6136	. . . . . . . . . . . . . 14 ⊢ ((𝑓 ↾ (1...𝑛)):(1...𝑛)–1-1-onto→(𝑓 “ (1...𝑛)) → (𝑓 ↾ (1...𝑛)):(1...𝑛)–1-1→(𝑓 “ (1...𝑛)))
176	174, 175	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (𝑓 ↾ (1...𝑛)):(1...𝑛)–1-1→(𝑓 “ (1...𝑛)))
177		suppssdm 7308	. . . . . . . . . . . . . . 15 ⊢ ((𝐻 ↾ (𝑓 “ (1...𝑛))) supp 0 ) ⊆ dom (𝐻 ↾ (𝑓 “ (1...𝑛)))
178		dmres 5419	. . . . . . . . . . . . . . . 16 ⊢ dom (𝐻 ↾ (𝑓 “ (1...𝑛))) = ((𝑓 “ (1...𝑛)) ∩ dom 𝐻)
179	178	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → dom (𝐻 ↾ (𝑓 “ (1...𝑛))) = ((𝑓 “ (1...𝑛)) ∩ dom 𝐻))
180	177, 179	syl5sseq 3653	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ((𝐻 ↾ (𝑓 “ (1...𝑛))) supp 0 ) ⊆ ((𝑓 “ (1...𝑛)) ∩ dom 𝐻))
181		inss1 3833	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 “ (1...𝑛)) ∩ dom 𝐻) ⊆ (𝑓 “ (1...𝑛))
182		df-ima 5127	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 “ (1...𝑛)) = ran (𝑓 ↾ (1...𝑛))
183	182	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (𝑓 “ (1...𝑛)) = ran (𝑓 ↾ (1...𝑛)))
184	181, 183	syl5sseq 3653	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ((𝑓 “ (1...𝑛)) ∩ dom 𝐻) ⊆ ran (𝑓 ↾ (1...𝑛)))
185	180, 184	sstrd 3613	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ((𝐻 ↾ (𝑓 “ (1...𝑛))) supp 0 ) ⊆ ran (𝑓 ↾ (1...𝑛)))
186		eqid 2622	. . . . . . . . . . . . 13 ⊢ (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) supp 0 ) = (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) supp 0 )
187	2, 3, 6, 161, 100, 162, 164, 171, 172, 176, 185, 186	gsumval3 18308	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛)))) = (seq1( + , ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))))‘𝑛))
188	182	eqimss2i 3660	. . . . . . . . . . . . . . . . . 18 ⊢ ran (𝑓 ↾ (1...𝑛)) ⊆ (𝑓 “ (1...𝑛))
189		cores 5638	. . . . . . . . . . . . . . . . . 18 ⊢ (ran (𝑓 ↾ (1...𝑛)) ⊆ (𝑓 “ (1...𝑛)) → ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) = (𝐻 ∘ (𝑓 ↾ (1...𝑛))))
190	188, 189	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) = (𝐻 ∘ (𝑓 ↾ (1...𝑛)))
191		resco 5639	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐻 ∘ 𝑓) ↾ (1...𝑛)) = (𝐻 ∘ (𝑓 ↾ (1...𝑛)))
192	190, 191	eqtr4i 2647	. . . . . . . . . . . . . . . 16 ⊢ ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) = ((𝐻 ∘ 𝑓) ↾ (1...𝑛))
193	192	fveq1i 6192	. . . . . . . . . . . . . . 15 ⊢ (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛)))‘𝑘) = (((𝐻 ∘ 𝑓) ↾ (1...𝑛))‘𝑘)
194		fvres 6207	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (1...𝑛) → (((𝐻 ∘ 𝑓) ↾ (1...𝑛))‘𝑘) = ((𝐻 ∘ 𝑓)‘𝑘))
195	193, 194	syl5eq 2668	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (1...𝑛) → (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛)))‘𝑘) = ((𝐻 ∘ 𝑓)‘𝑘))
196	195	adantl 482	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛)))‘𝑘) = ((𝐻 ∘ 𝑓)‘𝑘))
197	102, 196	seqfveq 12825	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (seq1( + , ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))))‘𝑛) = (seq1( + , (𝐻 ∘ 𝑓))‘𝑛))
198	187, 197	eqtr2d 2657	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (seq1( + , (𝐻 ∘ 𝑓))‘𝑛) = (𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛)))))
199		fvex 6201	. . . . . . . . . . . 12 ⊢ (seq1( + , (𝐻 ∘ 𝑓))‘𝑛) ∈ V
200	199	elsn 4192	. . . . . . . . . . 11 ⊢ ((seq1( + , (𝐻 ∘ 𝑓))‘𝑛) ∈ {(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))} ↔ (seq1( + , (𝐻 ∘ 𝑓))‘𝑛) = (𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛)))))
201	198, 200	sylibr 224	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (seq1( + , (𝐻 ∘ 𝑓))‘𝑛) ∈ {(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})
202	6, 161	cntzi 17762	. . . . . . . . . 10 ⊢ ((((𝐹 ∘ 𝑓)‘(𝑛 + 1)) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}) ∧ (seq1( + , (𝐻 ∘ 𝑓))‘𝑛) ∈ {(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}) → (((𝐹 ∘ 𝑓)‘(𝑛 + 1)) + (seq1( + , (𝐻 ∘ 𝑓))‘𝑛)) = ((seq1( + , (𝐻 ∘ 𝑓))‘𝑛) + ((𝐹 ∘ 𝑓)‘(𝑛 + 1))))
203	160, 201, 202	syl2anc 693	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (((𝐹 ∘ 𝑓)‘(𝑛 + 1)) + (seq1( + , (𝐻 ∘ 𝑓))‘𝑛)) = ((seq1( + , (𝐻 ∘ 𝑓))‘𝑛) + ((𝐹 ∘ 𝑓)‘(𝑛 + 1))))
204	203	eqcomd 2628	. . . . . . . 8 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → ((seq1( + , (𝐻 ∘ 𝑓))‘𝑛) + ((𝐹 ∘ 𝑓)‘(𝑛 + 1))) = (((𝐹 ∘ 𝑓)‘(𝑛 + 1)) + (seq1( + , (𝐻 ∘ 𝑓))‘𝑛)))
205	2, 6, 100, 113, 116, 119, 121, 204	mnd4g 17307	. . . . . . 7 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(#‘𝑊))) → (((seq1( + , (𝐹 ∘ 𝑓))‘𝑛) + (seq1( + , (𝐻 ∘ 𝑓))‘𝑛)) + (((𝐹 ∘ 𝑓)‘(𝑛 + 1)) + ((𝐻 ∘ 𝑓)‘(𝑛 + 1)))) = (((seq1( + , (𝐹 ∘ 𝑓))‘𝑛) + ((𝐹 ∘ 𝑓)‘(𝑛 + 1))) + ((seq1( + , (𝐻 ∘ 𝑓))‘𝑛) + ((𝐻 ∘ 𝑓)‘(𝑛 + 1)))))
206	51, 51, 54, 78, 82, 99, 205	seqcaopr3 12836	. . . . . 6 ⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → (seq1( + , ((𝐹 ∘𝑓 + 𝐻) ∘ 𝑓))‘(#‘𝑊)) = ((seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊)) + (seq1( + , (𝐻 ∘ 𝑓))‘(#‘𝑊))))
207	50, 55, 79, 85, 85, 87	off 6912	. . . . . . 7 ⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → (𝐹 ∘𝑓 + 𝐻):𝐴⟶𝐵)
208		gsumzaddlem.3	. . . . . . . 8 ⊢ (𝜑 → ran (𝐹 ∘𝑓 + 𝐻) ⊆ (𝑍‘ran (𝐹 ∘𝑓 + 𝐻)))
209	208	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → ran (𝐹 ∘𝑓 + 𝐻) ⊆ (𝑍‘ran (𝐹 ∘𝑓 + 𝐻)))
210	47, 111	sylan 488	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ (𝑘 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) → (𝑘 + 𝑥) ∈ 𝐵)
211	210, 55, 79, 85, 85, 87	off 6912	. . . . . . . 8 ⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → (𝐹 ∘𝑓 + 𝐻):𝐴⟶𝐵)
212		eldifi 3732	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐴 ∖ ran 𝑓) → 𝑥 ∈ 𝐴)
213		eqidd 2623	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = (𝐹‘𝑥))
214		eqidd 2623	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) = (𝐻‘𝑥))
215	83, 84, 85, 85, 87, 213, 214	ofval 6906	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑥 ∈ 𝐴) → ((𝐹 ∘𝑓 + 𝐻)‘𝑥) = ((𝐹‘𝑥) + (𝐻‘𝑥)))
216	212, 215	sylan2 491	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → ((𝐹 ∘𝑓 + 𝐻)‘𝑥) = ((𝐹‘𝑥) + (𝐻‘𝑥)))
217	18	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → (𝐹 supp 0 ) ⊆ ((𝐹 ∪ 𝐻) supp 0 ))
218		f1ofo 6144	. . . . . . . . . . . . . . . 16 ⊢ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 → 𝑓:(1...(#‘𝑊))–onto→𝑊)
219		forn 6118	. . . . . . . . . . . . . . . 16 ⊢ (𝑓:(1...(#‘𝑊))–onto→𝑊 → ran 𝑓 = 𝑊)
220	218, 219	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 → ran 𝑓 = 𝑊)
221	220, 19	syl6eq 2672	. . . . . . . . . . . . . 14 ⊢ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 → ran 𝑓 = ((𝐹 ∪ 𝐻) supp 0 ))
222	221	sseq2d 3633	. . . . . . . . . . . . 13 ⊢ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 → ((𝐹 supp 0 ) ⊆ ran 𝑓 ↔ (𝐹 supp 0 ) ⊆ ((𝐹 ∪ 𝐻) supp 0 )))
223	222	ad2antll 765	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → ((𝐹 supp 0 ) ⊆ ran 𝑓 ↔ (𝐹 supp 0 ) ⊆ ((𝐹 ∪ 𝐻) supp 0 )))
224	217, 223	mpbird 247	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → (𝐹 supp 0 ) ⊆ ran 𝑓)
225	13	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → 0 ∈ V)
226	55, 224, 85, 225	suppssr 7326	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → (𝐹‘𝑥) = 0 )
227	29	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → (𝐻 supp 0 ) ⊆ ((𝐻 ∪ 𝐹) supp 0 ))
228	227, 31	syl6sseqr 3652	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → (𝐻 supp 0 ) ⊆ ((𝐹 ∪ 𝐻) supp 0 ))
229	221	sseq2d 3633	. . . . . . . . . . . . 13 ⊢ (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 → ((𝐻 supp 0 ) ⊆ ran 𝑓 ↔ (𝐻 supp 0 ) ⊆ ((𝐹 ∪ 𝐻) supp 0 )))
230	229	ad2antll 765	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → ((𝐻 supp 0 ) ⊆ ran 𝑓 ↔ (𝐻 supp 0 ) ⊆ ((𝐹 ∪ 𝐻) supp 0 )))
231	228, 230	mpbird 247	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → (𝐻 supp 0 ) ⊆ ran 𝑓)
232	79, 231, 85, 225	suppssr 7326	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → (𝐻‘𝑥) = 0 )
233	226, 232	oveq12d 6668	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → ((𝐹‘𝑥) + (𝐻‘𝑥)) = ( 0 + 0 ))
234	8	ad2antrr 762	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → ( 0 + 0 ) = 0 )
235	216, 233, 234	3eqtrd 2660	. . . . . . . 8 ⊢ (((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → ((𝐹 ∘𝑓 + 𝐻)‘𝑥) = 0 )
236	211, 235	suppss 7325	. . . . . . 7 ⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → ((𝐹 ∘𝑓 + 𝐻) supp 0 ) ⊆ ran 𝑓)
237		ovex 6678	. . . . . . . . 9 ⊢ (𝐹 ∘𝑓 + 𝐻) ∈ V
238	237, 137	coex 7118	. . . . . . . 8 ⊢ ((𝐹 ∘𝑓 + 𝐻) ∘ 𝑓) ∈ V
239		suppimacnv 7306	. . . . . . . . 9 ⊢ ((((𝐹 ∘𝑓 + 𝐻) ∘ 𝑓) ∈ V ∧ 0 ∈ V) → (((𝐹 ∘𝑓 + 𝐻) ∘ 𝑓) supp 0 ) = (◡((𝐹 ∘𝑓 + 𝐻) ∘ 𝑓) “ (V ∖ { 0 })))
240	239	eqcomd 2628	. . . . . . . 8 ⊢ ((((𝐹 ∘𝑓 + 𝐻) ∘ 𝑓) ∈ V ∧ 0 ∈ V) → (◡((𝐹 ∘𝑓 + 𝐻) ∘ 𝑓) “ (V ∖ { 0 })) = (((𝐹 ∘𝑓 + 𝐻) ∘ 𝑓) supp 0 ))
241	238, 13, 240	mp2an 708	. . . . . . 7 ⊢ (◡((𝐹 ∘𝑓 + 𝐻) ∘ 𝑓) “ (V ∖ { 0 })) = (((𝐹 ∘𝑓 + 𝐻) ∘ 𝑓) supp 0 )
242	2, 3, 6, 161, 47, 85, 207, 209, 52, 73, 236, 241	gsumval3 18308	. . . . . 6 ⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → (𝐺 Σg (𝐹 ∘𝑓 + 𝐻)) = (seq1( + , ((𝐹 ∘𝑓 + 𝐻) ∘ 𝑓))‘(#‘𝑊)))
243		gsumzaddlem.1	. . . . . . . . 9 ⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
244	243	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
245		eqid 2622	. . . . . . . 8 ⊢ ((𝐹 ∘ 𝑓) supp 0 ) = ((𝐹 ∘ 𝑓) supp 0 )
246	2, 3, 6, 161, 47, 85, 55, 244, 52, 73, 224, 245	gsumval3 18308	. . . . . . 7 ⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊)))
247	165	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → ran 𝐻 ⊆ (𝑍‘ran 𝐻))
248		eqid 2622	. . . . . . . 8 ⊢ ((𝐻 ∘ 𝑓) supp 0 ) = ((𝐻 ∘ 𝑓) supp 0 )
249	2, 3, 6, 161, 47, 85, 79, 247, 52, 73, 231, 248	gsumval3 18308	. . . . . . 7 ⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → (𝐺 Σg 𝐻) = (seq1( + , (𝐻 ∘ 𝑓))‘(#‘𝑊)))
250	246, 249	oveq12d 6668	. . . . . 6 ⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)) = ((seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊)) + (seq1( + , (𝐻 ∘ 𝑓))‘(#‘𝑊))))
251	206, 242, 250	3eqtr4d 2666	. . . . 5 ⊢ ((𝜑 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)) → (𝐺 Σg (𝐹 ∘𝑓 + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)))
252	251	expr 643	. . . 4 ⊢ ((𝜑 ∧ (#‘𝑊) ∈ ℕ) → (𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 → (𝐺 Σg (𝐹 ∘𝑓 + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))))
253	252	exlimdv 1861	. . 3 ⊢ ((𝜑 ∧ (#‘𝑊) ∈ ℕ) → (∃𝑓 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 → (𝐺 Σg (𝐹 ∘𝑓 + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))))
254	253	expimpd 629	. 2 ⊢ (𝜑 → (((#‘𝑊) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊) → (𝐺 Σg (𝐹 ∘𝑓 + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))))
255		gsumzadd.fn	. . . . 5 ⊢ (𝜑 → 𝐹 finSupp 0 )
256		gsumzadd.hn	. . . . 5 ⊢ (𝜑 → 𝐻 finSupp 0 )
257	255, 256	fsuppun 8294	. . . 4 ⊢ (𝜑 → ((𝐹 ∪ 𝐻) supp 0 ) ∈ Fin)
258	19, 257	syl5eqel 2705	. . 3 ⊢ (𝜑 → 𝑊 ∈ Fin)
259		fz1f1o 14441	. . 3 ⊢ (𝑊 ∈ Fin → (𝑊 = ∅ ∨ ((#‘𝑊) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)))
260	258, 259	syl 17	. 2 ⊢ (𝜑 → (𝑊 = ∅ ∨ ((#‘𝑊) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(#‘𝑊))–1-1-onto→𝑊)))
261	46, 254, 260	mpjaod 396	1 ⊢ (𝜑 → (𝐺 Σg (𝐹 ∘𝑓 + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)))

Syntax hints:   → wi 4   ↔ wb 196   ∨ wo 383   ∧ wa 384  ∀wal 1481   = wceq 1483  ∃wex 1704   ∈ wcel 1990  ∀wral 2912  Vcvv 3200   ∖ cdif 3571   ∪ cun 3572   ∩ cin 3573   ⊆ wss 3574  ∅c0 3915  {csn 4177   class class class wbr 4653   ↦ cmpt 4729  ^◡ccnv 5113  dom cdm 5114  ran crn 5115   ↾ cres 5116   “ cima 5117   ∘ ccom 5118   Fn wfn 5883  ⟶wf 5884  –1-1→wf1 5885  –onto→wfo 5886  –1-1-onto→wf1o 5887  ‘cfv 5888  (class class class)co 6650   ∘_𝑓 cof 6895   supp csupp 7295  Fincfn 7955   finSupp cfsupp 8275  1c1 9937   + caddc 9939  ℕcn 11020  ℤ_≥cuz 11687  ...cfz 12326  ..^cfzo 12465  seqcseq 12801  #chash 13117  Basecbs 15857  +_gcplusg 15941  0_gc0g 16100   Σ_g cgsu 16101  Mndcmnd 17294  Cntzccntz 17748

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-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  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-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  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-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  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-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  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-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-of 6897  df-om 7066  df-1st 7168  df-2nd 7169  df-supp 7296  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-fsupp 8276  df-oi 8415  df-card 8765  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-nn 11021  df-n0 11293  df-z 11378  df-uz 11688  df-fz 12327  df-fzo 12466  df-seq 12802  df-hash 13118  df-0g 16102  df-gsum 16103  df-mgm 17242  df-sgrp 17284  df-mnd 17295  df-cntz 17750

This theorem is referenced by:  gsumzadd  18322  dprdfadd  18419