Theorem gsumzaddlem 19034

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 (𝐹 ∘f + 𝐻) ⊆ (𝑍‘ran (𝐹 ∘f + 𝐻)))
gsumzaddlem.4	⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → (𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))}))

Assertion

Ref	Expression
gsumzaddlem	⊢ (𝜑 → (𝐺 Σg (𝐹 ∘f + 𝐻)) = ((𝐺 Σ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 17918	. . . . . . 7 ⊢ (𝐺 ∈ Mnd → 0 ∈ 𝐵)
5	1, 4	syl 17	. . . . . 6 ⊢ (𝜑 → 0 ∈ 𝐵)
6		gsumzadd.p	. . . . . . 7 ⊢ + = (+g‘𝐺)
7	2, 6, 3	mndlid 17923	. . . . . 6 ⊢ ((𝐺 ∈ Mnd ∧ 0 ∈ 𝐵) → ( 0 + 0 ) = 0 )
8	1, 5, 7	syl2anc 587	. . . . 5 ⊢ (𝜑 → ( 0 + 0 ) = 0 )
9	8	adantr 484	. . . 4 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ( 0 + 0 ) = 0 )
10		gsumzaddlem.f	. . . . . . . 8 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
11		gsumzadd.a	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
12	3	fvexi 6659	. . . . . . . . 9 ⊢ 0 ∈ V
13	12	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 0 ∈ V)
14		gsumzaddlem.h	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐻:𝐴⟶𝐵)
15		fex 6966	. . . . . . . . . . 11 ⊢ ((𝐻:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉) → 𝐻 ∈ V)
16	14, 11, 15	syl2anc 587	. . . . . . . . . 10 ⊢ (𝜑 → 𝐻 ∈ V)
17	16	suppun 7833	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 supp 0 ) ⊆ ((𝐹 ∪ 𝐻) supp 0 ))
18		gsumzaddlem.w	. . . . . . . . 9 ⊢ 𝑊 = ((𝐹 ∪ 𝐻) supp 0 )
19	17, 18	sseqtrrdi 3966	. . . . . . . 8 ⊢ (𝜑 → (𝐹 supp 0 ) ⊆ 𝑊)
20	10, 11, 13, 19	gsumcllem 19021	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐹 = (𝑥 ∈ 𝐴 ↦ 0 ))
21	20	oveq2d 7151	. . . . . 6 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg 𝐹) = (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 )))
22	3	gsumz 17992	. . . . . . . 8 ⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 )) = 0 )
23	1, 11, 22	syl2anc 587	. . . . . . 7 ⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 )) = 0 )
24	23	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 )) = 0 )
25	21, 24	eqtrd 2833	. . . . 5 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg 𝐹) = 0 )
26		fex 6966	. . . . . . . . . . . 12 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉) → 𝐹 ∈ V)
27	10, 11, 26	syl2anc 587	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ V)
28	27	suppun 7833	. . . . . . . . . 10 ⊢ (𝜑 → (𝐻 supp 0 ) ⊆ ((𝐻 ∪ 𝐹) supp 0 ))
29		uncom 4080	. . . . . . . . . . 11 ⊢ (𝐹 ∪ 𝐻) = (𝐻 ∪ 𝐹)
30	29	oveq1i 7145	. . . . . . . . . 10 ⊢ ((𝐹 ∪ 𝐻) supp 0 ) = ((𝐻 ∪ 𝐹) supp 0 )
31	28, 30	sseqtrrdi 3966	. . . . . . . . 9 ⊢ (𝜑 → (𝐻 supp 0 ) ⊆ ((𝐹 ∪ 𝐻) supp 0 ))
32	31, 18	sseqtrrdi 3966	. . . . . . . 8 ⊢ (𝜑 → (𝐻 supp 0 ) ⊆ 𝑊)
33	14, 11, 13, 32	gsumcllem 19021	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐻 = (𝑥 ∈ 𝐴 ↦ 0 ))
34	33	oveq2d 7151	. . . . . 6 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg 𝐻) = (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 )))
35	34, 24	eqtrd 2833	. . . . 5 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg 𝐻) = 0 )
36	25, 35	oveq12d 7153	. . . 4 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)) = ( 0 + 0 ))
37	11	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐴 ∈ 𝑉)
38	5	ad2antrr 725	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ 𝐴) → 0 ∈ 𝐵)
39	37, 38, 38, 20, 33	offval2 7406	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐹 ∘f + 𝐻) = (𝑥 ∈ 𝐴 ↦ ( 0 + 0 )))
40	9	mpteq2dv 5126	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝑥 ∈ 𝐴 ↦ ( 0 + 0 )) = (𝑥 ∈ 𝐴 ↦ 0 ))
41	39, 40	eqtrd 2833	. . . . . 6 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐹 ∘f + 𝐻) = (𝑥 ∈ 𝐴 ↦ 0 ))
42	41	oveq2d 7151	. . . . 5 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg (𝐹 ∘f + 𝐻)) = (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 0 )))
43	42, 24	eqtrd 2833	. . . 4 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg (𝐹 ∘f + 𝐻)) = 0 )
44	9, 36, 43	3eqtr4rd 2844	. . 3 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐺 Σg (𝐹 ∘f + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)))
45	44	ex 416	. 2 ⊢ (𝜑 → (𝑊 = ∅ → (𝐺 Σg (𝐹 ∘f + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))))
46	1	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → 𝐺 ∈ Mnd)
47	2, 6	mndcl 17911	. . . . . . . . . 10 ⊢ ((𝐺 ∈ Mnd ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) → (𝑧 + 𝑤) ∈ 𝐵)
48	47	3expb 1117	. . . . . . . . 9 ⊢ ((𝐺 ∈ Mnd ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (𝑧 + 𝑤) ∈ 𝐵)
49	46, 48	sylan 583	. . . . . . . 8 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (𝑧 + 𝑤) ∈ 𝐵)
50	49	caovclg 7320	. . . . . . 7 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) ∈ 𝐵)
51		simprl 770	. . . . . . . 8 ⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (♯‘𝑊) ∈ ℕ)
52		nnuz 12269	. . . . . . . 8 ⊢ ℕ = (ℤ≥‘1)
53	51, 52	eleqtrdi 2900	. . . . . . 7 ⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (♯‘𝑊) ∈ (ℤ≥‘1))
54	10	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → 𝐹:𝐴⟶𝐵)
55		f1of1 6589	. . . . . . . . . . . 12 ⊢ (𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 → 𝑓:(1...(♯‘𝑊))–1-1→𝑊)
56	55	ad2antll 728	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → 𝑓:(1...(♯‘𝑊))–1-1→𝑊)
57		suppssdm 7826	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∪ 𝐻) supp 0 ) ⊆ dom (𝐹 ∪ 𝐻)
58	57	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐹 ∪ 𝐻) supp 0 ) ⊆ dom (𝐹 ∪ 𝐻))
59	18	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑊 = ((𝐹 ∪ 𝐻) supp 0 ))
60		dmun 5743	. . . . . . . . . . . . . 14 ⊢ dom (𝐹 ∪ 𝐻) = (dom 𝐹 ∪ dom 𝐻)
61	10	fdmd 6497	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → dom 𝐹 = 𝐴)
62	14	fdmd 6497	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → dom 𝐻 = 𝐴)
63	61, 62	uneq12d 4091	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (dom 𝐹 ∪ dom 𝐻) = (𝐴 ∪ 𝐴))
64		unidm 4079	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∪ 𝐴) = 𝐴
65	63, 64	eqtrdi 2849	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (dom 𝐹 ∪ dom 𝐻) = 𝐴)
66	60, 65	syl5req 2846	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 = dom (𝐹 ∪ 𝐻))
67	58, 59, 66	3sstr4d 3962	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑊 ⊆ 𝐴)
68	67	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → 𝑊 ⊆ 𝐴)
69		f1ss 6555	. . . . . . . . . . 11 ⊢ ((𝑓:(1...(♯‘𝑊))–1-1→𝑊 ∧ 𝑊 ⊆ 𝐴) → 𝑓:(1...(♯‘𝑊))–1-1→𝐴)
70	56, 68, 69	syl2anc 587	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → 𝑓:(1...(♯‘𝑊))–1-1→𝐴)
71		f1f 6549	. . . . . . . . . 10 ⊢ (𝑓:(1...(♯‘𝑊))–1-1→𝐴 → 𝑓:(1...(♯‘𝑊))⟶𝐴)
72	70, 71	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → 𝑓:(1...(♯‘𝑊))⟶𝐴)
73		fco 6505	. . . . . . . . 9 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑓:(1...(♯‘𝑊))⟶𝐴) → (𝐹 ∘ 𝑓):(1...(♯‘𝑊))⟶𝐵)
74	54, 72, 73	syl2anc 587	. . . . . . . 8 ⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (𝐹 ∘ 𝑓):(1...(♯‘𝑊))⟶𝐵)
75	74	ffvelrnda 6828	. . . . . . 7 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑘 ∈ (1...(♯‘𝑊))) → ((𝐹 ∘ 𝑓)‘𝑘) ∈ 𝐵)
76	14	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → 𝐻:𝐴⟶𝐵)
77		fco 6505	. . . . . . . . 9 ⊢ ((𝐻:𝐴⟶𝐵 ∧ 𝑓:(1...(♯‘𝑊))⟶𝐴) → (𝐻 ∘ 𝑓):(1...(♯‘𝑊))⟶𝐵)
78	76, 72, 77	syl2anc 587	. . . . . . . 8 ⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (𝐻 ∘ 𝑓):(1...(♯‘𝑊))⟶𝐵)
79	78	ffvelrnda 6828	. . . . . . 7 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑘 ∈ (1...(♯‘𝑊))) → ((𝐻 ∘ 𝑓)‘𝑘) ∈ 𝐵)
80	54	ffnd 6488	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → 𝐹 Fn 𝐴)
81	76	ffnd 6488	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → 𝐻 Fn 𝐴)
82	11	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → 𝐴 ∈ 𝑉)
83		ovexd 7170	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (1...(♯‘𝑊)) ∈ V)
84		inidm 4145	. . . . . . . . . . 11 ⊢ (𝐴 ∩ 𝐴) = 𝐴
85	80, 81, 72, 82, 82, 83, 84	ofco 7409	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → ((𝐹 ∘f + 𝐻) ∘ 𝑓) = ((𝐹 ∘ 𝑓) ∘f + (𝐻 ∘ 𝑓)))
86	85	fveq1d 6647	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (((𝐹 ∘f + 𝐻) ∘ 𝑓)‘𝑘) = (((𝐹 ∘ 𝑓) ∘f + (𝐻 ∘ 𝑓))‘𝑘))
87	86	adantr 484	. . . . . . . 8 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑘 ∈ (1...(♯‘𝑊))) → (((𝐹 ∘f + 𝐻) ∘ 𝑓)‘𝑘) = (((𝐹 ∘ 𝑓) ∘f + (𝐻 ∘ 𝑓))‘𝑘))
88		fnfco 6517	. . . . . . . . . 10 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑓:(1...(♯‘𝑊))⟶𝐴) → (𝐹 ∘ 𝑓) Fn (1...(♯‘𝑊)))
89	80, 72, 88	syl2anc 587	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (𝐹 ∘ 𝑓) Fn (1...(♯‘𝑊)))
90		fnfco 6517	. . . . . . . . . 10 ⊢ ((𝐻 Fn 𝐴 ∧ 𝑓:(1...(♯‘𝑊))⟶𝐴) → (𝐻 ∘ 𝑓) Fn (1...(♯‘𝑊)))
91	81, 72, 90	syl2anc 587	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (𝐻 ∘ 𝑓) Fn (1...(♯‘𝑊)))
92		inidm 4145	. . . . . . . . 9 ⊢ ((1...(♯‘𝑊)) ∩ (1...(♯‘𝑊))) = (1...(♯‘𝑊))
93		eqidd 2799	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑘 ∈ (1...(♯‘𝑊))) → ((𝐹 ∘ 𝑓)‘𝑘) = ((𝐹 ∘ 𝑓)‘𝑘))
94		eqidd 2799	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑘 ∈ (1...(♯‘𝑊))) → ((𝐻 ∘ 𝑓)‘𝑘) = ((𝐻 ∘ 𝑓)‘𝑘))
95	89, 91, 83, 83, 92, 93, 94	ofval 7398	. . . . . . . 8 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑘 ∈ (1...(♯‘𝑊))) → (((𝐹 ∘ 𝑓) ∘f + (𝐻 ∘ 𝑓))‘𝑘) = (((𝐹 ∘ 𝑓)‘𝑘) + ((𝐻 ∘ 𝑓)‘𝑘)))
96	87, 95	eqtrd 2833	. . . . . . 7 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑘 ∈ (1...(♯‘𝑊))) → (((𝐹 ∘f + 𝐻) ∘ 𝑓)‘𝑘) = (((𝐹 ∘ 𝑓)‘𝑘) + ((𝐻 ∘ 𝑓)‘𝑘)))
97	1	ad2antrr 725	. . . . . . . 8 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → 𝐺 ∈ Mnd)
98		elfzouz 13037	. . . . . . . . . 10 ⊢ (𝑛 ∈ (1..^(♯‘𝑊)) → 𝑛 ∈ (ℤ≥‘1))
99	98	adantl 485	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → 𝑛 ∈ (ℤ≥‘1))
100		elfzouz2 13047	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (1..^(♯‘𝑊)) → (♯‘𝑊) ∈ (ℤ≥‘𝑛))
101	100	adantl 485	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (♯‘𝑊) ∈ (ℤ≥‘𝑛))
102		fzss2 12942	. . . . . . . . . . . 12 ⊢ ((♯‘𝑊) ∈ (ℤ≥‘𝑛) → (1...𝑛) ⊆ (1...(♯‘𝑊)))
103	101, 102	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (1...𝑛) ⊆ (1...(♯‘𝑊)))
104	103	sselda 3915	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ (1...(♯‘𝑊)))
105	75	adantlr 714	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) ∧ 𝑘 ∈ (1...(♯‘𝑊))) → ((𝐹 ∘ 𝑓)‘𝑘) ∈ 𝐵)
106	104, 105	syldan 594	. . . . . . . . 9 ⊢ ((((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐹 ∘ 𝑓)‘𝑘) ∈ 𝐵)
107	2, 6	mndcl 17911	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ Mnd ∧ 𝑘 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵) → (𝑘 + 𝑥) ∈ 𝐵)
108	107	3expb 1117	. . . . . . . . . 10 ⊢ ((𝐺 ∈ Mnd ∧ (𝑘 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) → (𝑘 + 𝑥) ∈ 𝐵)
109	97, 108	sylan 583	. . . . . . . . 9 ⊢ ((((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) ∧ (𝑘 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) → (𝑘 + 𝑥) ∈ 𝐵)
110	99, 106, 109	seqcl 13386	. . . . . . . 8 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (seq1( + , (𝐹 ∘ 𝑓))‘𝑛) ∈ 𝐵)
111	79	adantlr 714	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) ∧ 𝑘 ∈ (1...(♯‘𝑊))) → ((𝐻 ∘ 𝑓)‘𝑘) ∈ 𝐵)
112	104, 111	syldan 594	. . . . . . . . 9 ⊢ ((((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐻 ∘ 𝑓)‘𝑘) ∈ 𝐵)
113	99, 112, 109	seqcl 13386	. . . . . . . 8 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (seq1( + , (𝐻 ∘ 𝑓))‘𝑛) ∈ 𝐵)
114		fzofzp1 13129	. . . . . . . . 9 ⊢ (𝑛 ∈ (1..^(♯‘𝑊)) → (𝑛 + 1) ∈ (1...(♯‘𝑊)))
115		ffvelrn 6826	. . . . . . . . 9 ⊢ (((𝐹 ∘ 𝑓):(1...(♯‘𝑊))⟶𝐵 ∧ (𝑛 + 1) ∈ (1...(♯‘𝑊))) → ((𝐹 ∘ 𝑓)‘(𝑛 + 1)) ∈ 𝐵)
116	74, 114, 115	syl2an 598	. . . . . . . 8 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ((𝐹 ∘ 𝑓)‘(𝑛 + 1)) ∈ 𝐵)
117		ffvelrn 6826	. . . . . . . . 9 ⊢ (((𝐻 ∘ 𝑓):(1...(♯‘𝑊))⟶𝐵 ∧ (𝑛 + 1) ∈ (1...(♯‘𝑊))) → ((𝐻 ∘ 𝑓)‘(𝑛 + 1)) ∈ 𝐵)
118	78, 114, 117	syl2an 598	. . . . . . . 8 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ((𝐻 ∘ 𝑓)‘(𝑛 + 1)) ∈ 𝐵)
119		fvco3 6737	. . . . . . . . . . . 12 ⊢ ((𝑓:(1...(♯‘𝑊))⟶𝐴 ∧ (𝑛 + 1) ∈ (1...(♯‘𝑊))) → ((𝐹 ∘ 𝑓)‘(𝑛 + 1)) = (𝐹‘(𝑓‘(𝑛 + 1))))
120	72, 114, 119	syl2an 598	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ((𝐹 ∘ 𝑓)‘(𝑛 + 1)) = (𝐹‘(𝑓‘(𝑛 + 1))))
121		fveq2 6645	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑓‘(𝑛 + 1)) → (𝐹‘𝑘) = (𝐹‘(𝑓‘(𝑛 + 1))))
122	121	eleq1d 2874	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑓‘(𝑛 + 1)) → ((𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}) ↔ (𝐹‘(𝑓‘(𝑛 + 1))) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})))
123		gsumzaddlem.4	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → (𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))}))
124	123	expr 460	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐴) → (𝑘 ∈ (𝐴 ∖ 𝑥) → (𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))})))
125	124	ralrimiv 3148	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐴) → ∀𝑘 ∈ (𝐴 ∖ 𝑥)(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))}))
126	125	ex 416	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑥 ⊆ 𝐴 → ∀𝑘 ∈ (𝐴 ∖ 𝑥)(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))})))
127	126	alrimiv 1928	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑥(𝑥 ⊆ 𝐴 → ∀𝑘 ∈ (𝐴 ∖ 𝑥)(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))})))
128	127	ad2antrr 725	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ∀𝑥(𝑥 ⊆ 𝐴 → ∀𝑘 ∈ (𝐴 ∖ 𝑥)(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))})))
129		imassrn 5907	. . . . . . . . . . . . . 14 ⊢ (𝑓 “ (1...𝑛)) ⊆ ran 𝑓
130	72	adantr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → 𝑓:(1...(♯‘𝑊))⟶𝐴)
131	130	frnd 6494	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ran 𝑓 ⊆ 𝐴)
132	129, 131	sstrid 3926	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝑓 “ (1...𝑛)) ⊆ 𝐴)
133		vex 3444	. . . . . . . . . . . . . . 15 ⊢ 𝑓 ∈ V
134	133	imaex 7603	. . . . . . . . . . . . . 14 ⊢ (𝑓 “ (1...𝑛)) ∈ V
135		sseq1 3940	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝑓 “ (1...𝑛)) → (𝑥 ⊆ 𝐴 ↔ (𝑓 “ (1...𝑛)) ⊆ 𝐴))
136		difeq2 4044	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝑓 “ (1...𝑛)) → (𝐴 ∖ 𝑥) = (𝐴 ∖ (𝑓 “ (1...𝑛))))
137		reseq2 5813	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (𝑓 “ (1...𝑛)) → (𝐻 ↾ 𝑥) = (𝐻 ↾ (𝑓 “ (1...𝑛))))
138	137	oveq2d 7151	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (𝑓 “ (1...𝑛)) → (𝐺 Σg (𝐻 ↾ 𝑥)) = (𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛)))))
139	138	sneqd 4537	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = (𝑓 “ (1...𝑛)) → {(𝐺 Σg (𝐻 ↾ 𝑥))} = {(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})
140	139	fveq2d 6649	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (𝑓 “ (1...𝑛)) → (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))}) = (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}))
141	140	eleq2d 2875	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝑓 “ (1...𝑛)) → ((𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))}) ↔ (𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})))
142	136, 141	raleqbidv 3354	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝑓 “ (1...𝑛)) → (∀𝑘 ∈ (𝐴 ∖ 𝑥)(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))}) ↔ ∀𝑘 ∈ (𝐴 ∖ (𝑓 “ (1...𝑛)))(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})))
143	135, 142	imbi12d 348	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑓 “ (1...𝑛)) → ((𝑥 ⊆ 𝐴 → ∀𝑘 ∈ (𝐴 ∖ 𝑥)(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))})) ↔ ((𝑓 “ (1...𝑛)) ⊆ 𝐴 → ∀𝑘 ∈ (𝐴 ∖ (𝑓 “ (1...𝑛)))(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}))))
144	134, 143	spcv 3554	. . . . . . . . . . . . 13 ⊢ (∀𝑥(𝑥 ⊆ 𝐴 → ∀𝑘 ∈ (𝐴 ∖ 𝑥)(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))})) → ((𝑓 “ (1...𝑛)) ⊆ 𝐴 → ∀𝑘 ∈ (𝐴 ∖ (𝑓 “ (1...𝑛)))(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})))
145	128, 132, 144	sylc 65	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ∀𝑘 ∈ (𝐴 ∖ (𝑓 “ (1...𝑛)))(𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}))
146		ffvelrn 6826	. . . . . . . . . . . . . 14 ⊢ ((𝑓:(1...(♯‘𝑊))⟶𝐴 ∧ (𝑛 + 1) ∈ (1...(♯‘𝑊))) → (𝑓‘(𝑛 + 1)) ∈ 𝐴)
147	72, 114, 146	syl2an 598	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝑓‘(𝑛 + 1)) ∈ 𝐴)
148		fzp1nel 12986	. . . . . . . . . . . . . 14 ⊢ ¬ (𝑛 + 1) ∈ (1...𝑛)
149	70	adantr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → 𝑓:(1...(♯‘𝑊))–1-1→𝐴)
150	114	adantl 485	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝑛 + 1) ∈ (1...(♯‘𝑊)))
151		f1elima 6999	. . . . . . . . . . . . . . 15 ⊢ ((𝑓:(1...(♯‘𝑊))–1-1→𝐴 ∧ (𝑛 + 1) ∈ (1...(♯‘𝑊)) ∧ (1...𝑛) ⊆ (1...(♯‘𝑊))) → ((𝑓‘(𝑛 + 1)) ∈ (𝑓 “ (1...𝑛)) ↔ (𝑛 + 1) ∈ (1...𝑛)))
152	149, 150, 103, 151	syl3anc 1368	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ((𝑓‘(𝑛 + 1)) ∈ (𝑓 “ (1...𝑛)) ↔ (𝑛 + 1) ∈ (1...𝑛)))
153	148, 152	mtbiri 330	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ¬ (𝑓‘(𝑛 + 1)) ∈ (𝑓 “ (1...𝑛)))
154	147, 153	eldifd 3892	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝑓‘(𝑛 + 1)) ∈ (𝐴 ∖ (𝑓 “ (1...𝑛))))
155	122, 145, 154	rspcdva 3573	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝐹‘(𝑓‘(𝑛 + 1))) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}))
156	120, 155	eqeltrd 2890	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ((𝐹 ∘ 𝑓)‘(𝑛 + 1)) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}))
157		gsumzadd.z	. . . . . . . . . . . . 13 ⊢ 𝑍 = (Cntz‘𝐺)
158	134	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝑓 “ (1...𝑛)) ∈ V)
159	14	ad2antrr 725	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → 𝐻:𝐴⟶𝐵)
160	159, 132	fssresd 6519	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝐻 ↾ (𝑓 “ (1...𝑛))):(𝑓 “ (1...𝑛))⟶𝐵)
161		gsumzaddlem.2	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ran 𝐻 ⊆ (𝑍‘ran 𝐻))
162	161	ad2antrr 725	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ran 𝐻 ⊆ (𝑍‘ran 𝐻))
163		resss 5843	. . . . . . . . . . . . . . 15 ⊢ (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ 𝐻
164	163	rnssi 5774	. . . . . . . . . . . . . 14 ⊢ ran (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ ran 𝐻
165	157	cntzidss 18460	. . . . . . . . . . . . . 14 ⊢ ((ran 𝐻 ⊆ (𝑍‘ran 𝐻) ∧ ran (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ ran 𝐻) → ran (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ (𝑍‘ran (𝐻 ↾ (𝑓 “ (1...𝑛)))))
166	162, 164, 165	sylancl 589	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ran (𝐻 ↾ (𝑓 “ (1...𝑛))) ⊆ (𝑍‘ran (𝐻 ↾ (𝑓 “ (1...𝑛)))))
167	99, 52	eleqtrrdi 2901	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → 𝑛 ∈ ℕ)
168		f1ores 6604	. . . . . . . . . . . . . . 15 ⊢ ((𝑓:(1...(♯‘𝑊))–1-1→𝐴 ∧ (1...𝑛) ⊆ (1...(♯‘𝑊))) → (𝑓 ↾ (1...𝑛)):(1...𝑛)–1-1-onto→(𝑓 “ (1...𝑛)))
169	149, 103, 168	syl2anc 587	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝑓 ↾ (1...𝑛)):(1...𝑛)–1-1-onto→(𝑓 “ (1...𝑛)))
170		f1of1 6589	. . . . . . . . . . . . . 14 ⊢ ((𝑓 ↾ (1...𝑛)):(1...𝑛)–1-1-onto→(𝑓 “ (1...𝑛)) → (𝑓 ↾ (1...𝑛)):(1...𝑛)–1-1→(𝑓 “ (1...𝑛)))
171	169, 170	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝑓 ↾ (1...𝑛)):(1...𝑛)–1-1→(𝑓 “ (1...𝑛)))
172		suppssdm 7826	. . . . . . . . . . . . . . 15 ⊢ ((𝐻 ↾ (𝑓 “ (1...𝑛))) supp 0 ) ⊆ dom (𝐻 ↾ (𝑓 “ (1...𝑛)))
173		dmres 5840	. . . . . . . . . . . . . . . 16 ⊢ dom (𝐻 ↾ (𝑓 “ (1...𝑛))) = ((𝑓 “ (1...𝑛)) ∩ dom 𝐻)
174	173	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → dom (𝐻 ↾ (𝑓 “ (1...𝑛))) = ((𝑓 “ (1...𝑛)) ∩ dom 𝐻))
175	172, 174	sseqtrid 3967	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ((𝐻 ↾ (𝑓 “ (1...𝑛))) supp 0 ) ⊆ ((𝑓 “ (1...𝑛)) ∩ dom 𝐻))
176		inss1 4155	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 “ (1...𝑛)) ∩ dom 𝐻) ⊆ (𝑓 “ (1...𝑛))
177		df-ima 5532	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 “ (1...𝑛)) = ran (𝑓 ↾ (1...𝑛))
178	177	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝑓 “ (1...𝑛)) = ran (𝑓 ↾ (1...𝑛)))
179	176, 178	sseqtrid 3967	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ((𝑓 “ (1...𝑛)) ∩ dom 𝐻) ⊆ ran (𝑓 ↾ (1...𝑛)))
180	175, 179	sstrd 3925	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ((𝐻 ↾ (𝑓 “ (1...𝑛))) supp 0 ) ⊆ ran (𝑓 ↾ (1...𝑛)))
181		eqid 2798	. . . . . . . . . . . . 13 ⊢ (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) supp 0 ) = (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) supp 0 )
182	2, 3, 6, 157, 97, 158, 160, 166, 167, 171, 180, 181	gsumval3 19020	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛)))) = (seq1( + , ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))))‘𝑛))
183	177	eqimss2i 3974	. . . . . . . . . . . . . . . . . 18 ⊢ ran (𝑓 ↾ (1...𝑛)) ⊆ (𝑓 “ (1...𝑛))
184		cores 6069	. . . . . . . . . . . . . . . . . 18 ⊢ (ran (𝑓 ↾ (1...𝑛)) ⊆ (𝑓 “ (1...𝑛)) → ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) = (𝐻 ∘ (𝑓 ↾ (1...𝑛))))
185	183, 184	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) = (𝐻 ∘ (𝑓 ↾ (1...𝑛)))
186		resco 6070	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐻 ∘ 𝑓) ↾ (1...𝑛)) = (𝐻 ∘ (𝑓 ↾ (1...𝑛)))
187	185, 186	eqtr4i 2824	. . . . . . . . . . . . . . . 16 ⊢ ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))) = ((𝐻 ∘ 𝑓) ↾ (1...𝑛))
188	187	fveq1i 6646	. . . . . . . . . . . . . . 15 ⊢ (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛)))‘𝑘) = (((𝐻 ∘ 𝑓) ↾ (1...𝑛))‘𝑘)
189		fvres 6664	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (1...𝑛) → (((𝐻 ∘ 𝑓) ↾ (1...𝑛))‘𝑘) = ((𝐻 ∘ 𝑓)‘𝑘))
190	188, 189	syl5eq 2845	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (1...𝑛) → (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛)))‘𝑘) = ((𝐻 ∘ 𝑓)‘𝑘))
191	190	adantl 485	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛)))‘𝑘) = ((𝐻 ∘ 𝑓)‘𝑘))
192	99, 191	seqfveq 13390	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (seq1( + , ((𝐻 ↾ (𝑓 “ (1...𝑛))) ∘ (𝑓 ↾ (1...𝑛))))‘𝑛) = (seq1( + , (𝐻 ∘ 𝑓))‘𝑛))
193	182, 192	eqtr2d 2834	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (seq1( + , (𝐻 ∘ 𝑓))‘𝑛) = (𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛)))))
194		fvex 6658	. . . . . . . . . . . 12 ⊢ (seq1( + , (𝐻 ∘ 𝑓))‘𝑛) ∈ V
195	194	elsn 4540	. . . . . . . . . . 11 ⊢ ((seq1( + , (𝐻 ∘ 𝑓))‘𝑛) ∈ {(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))} ↔ (seq1( + , (𝐻 ∘ 𝑓))‘𝑛) = (𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛)))))
196	193, 195	sylibr 237	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (seq1( + , (𝐻 ∘ 𝑓))‘𝑛) ∈ {(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))})
197	6, 157	cntzi 18451	. . . . . . . . . 10 ⊢ ((((𝐹 ∘ 𝑓)‘(𝑛 + 1)) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}) ∧ (seq1( + , (𝐻 ∘ 𝑓))‘𝑛) ∈ {(𝐺 Σg (𝐻 ↾ (𝑓 “ (1...𝑛))))}) → (((𝐹 ∘ 𝑓)‘(𝑛 + 1)) + (seq1( + , (𝐻 ∘ 𝑓))‘𝑛)) = ((seq1( + , (𝐻 ∘ 𝑓))‘𝑛) + ((𝐹 ∘ 𝑓)‘(𝑛 + 1))))
198	156, 196, 197	syl2anc 587	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (((𝐹 ∘ 𝑓)‘(𝑛 + 1)) + (seq1( + , (𝐻 ∘ 𝑓))‘𝑛)) = ((seq1( + , (𝐻 ∘ 𝑓))‘𝑛) + ((𝐹 ∘ 𝑓)‘(𝑛 + 1))))
199	198	eqcomd 2804	. . . . . . . 8 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → ((seq1( + , (𝐻 ∘ 𝑓))‘𝑛) + ((𝐹 ∘ 𝑓)‘(𝑛 + 1))) = (((𝐹 ∘ 𝑓)‘(𝑛 + 1)) + (seq1( + , (𝐻 ∘ 𝑓))‘𝑛)))
200	2, 6, 97, 110, 113, 116, 118, 199	mnd4g 17917	. . . . . . 7 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑛 ∈ (1..^(♯‘𝑊))) → (((seq1( + , (𝐹 ∘ 𝑓))‘𝑛) + (seq1( + , (𝐻 ∘ 𝑓))‘𝑛)) + (((𝐹 ∘ 𝑓)‘(𝑛 + 1)) + ((𝐻 ∘ 𝑓)‘(𝑛 + 1)))) = (((seq1( + , (𝐹 ∘ 𝑓))‘𝑛) + ((𝐹 ∘ 𝑓)‘(𝑛 + 1))) + ((seq1( + , (𝐻 ∘ 𝑓))‘𝑛) + ((𝐻 ∘ 𝑓)‘(𝑛 + 1)))))
201	50, 50, 53, 75, 79, 96, 200	seqcaopr3 13401	. . . . . 6 ⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (seq1( + , ((𝐹 ∘f + 𝐻) ∘ 𝑓))‘(♯‘𝑊)) = ((seq1( + , (𝐹 ∘ 𝑓))‘(♯‘𝑊)) + (seq1( + , (𝐻 ∘ 𝑓))‘(♯‘𝑊))))
202	49, 54, 76, 82, 82, 84	off 7404	. . . . . . 7 ⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (𝐹 ∘f + 𝐻):𝐴⟶𝐵)
203		gsumzaddlem.3	. . . . . . . 8 ⊢ (𝜑 → ran (𝐹 ∘f + 𝐻) ⊆ (𝑍‘ran (𝐹 ∘f + 𝐻)))
204	203	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → ran (𝐹 ∘f + 𝐻) ⊆ (𝑍‘ran (𝐹 ∘f + 𝐻)))
205	46, 108	sylan 583	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ (𝑘 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) → (𝑘 + 𝑥) ∈ 𝐵)
206	205, 54, 76, 82, 82, 84	off 7404	. . . . . . . 8 ⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (𝐹 ∘f + 𝐻):𝐴⟶𝐵)
207		eldifi 4054	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐴 ∖ ran 𝑓) → 𝑥 ∈ 𝐴)
208		eqidd 2799	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = (𝐹‘𝑥))
209		eqidd 2799	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) = (𝐻‘𝑥))
210	80, 81, 82, 82, 84, 208, 209	ofval 7398	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑥 ∈ 𝐴) → ((𝐹 ∘f + 𝐻)‘𝑥) = ((𝐹‘𝑥) + (𝐻‘𝑥)))
211	207, 210	sylan2 595	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → ((𝐹 ∘f + 𝐻)‘𝑥) = ((𝐹‘𝑥) + (𝐻‘𝑥)))
212	17	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (𝐹 supp 0 ) ⊆ ((𝐹 ∪ 𝐻) supp 0 ))
213		f1ofo 6597	. . . . . . . . . . . . . . . 16 ⊢ (𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 → 𝑓:(1...(♯‘𝑊))–onto→𝑊)
214		forn 6568	. . . . . . . . . . . . . . . 16 ⊢ (𝑓:(1...(♯‘𝑊))–onto→𝑊 → ran 𝑓 = 𝑊)
215	213, 214	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 → ran 𝑓 = 𝑊)
216	215, 18	eqtrdi 2849	. . . . . . . . . . . . . 14 ⊢ (𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 → ran 𝑓 = ((𝐹 ∪ 𝐻) supp 0 ))
217	216	sseq2d 3947	. . . . . . . . . . . . 13 ⊢ (𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 → ((𝐹 supp 0 ) ⊆ ran 𝑓 ↔ (𝐹 supp 0 ) ⊆ ((𝐹 ∪ 𝐻) supp 0 )))
218	217	ad2antll 728	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → ((𝐹 supp 0 ) ⊆ ran 𝑓 ↔ (𝐹 supp 0 ) ⊆ ((𝐹 ∪ 𝐻) supp 0 )))
219	212, 218	mpbird 260	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (𝐹 supp 0 ) ⊆ ran 𝑓)
220	12	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → 0 ∈ V)
221	54, 219, 82, 220	suppssr 7844	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → (𝐹‘𝑥) = 0 )
222	28	adantr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (𝐻 supp 0 ) ⊆ ((𝐻 ∪ 𝐹) supp 0 ))
223	222, 30	sseqtrrdi 3966	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (𝐻 supp 0 ) ⊆ ((𝐹 ∪ 𝐻) supp 0 ))
224	216	sseq2d 3947	. . . . . . . . . . . . 13 ⊢ (𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 → ((𝐻 supp 0 ) ⊆ ran 𝑓 ↔ (𝐻 supp 0 ) ⊆ ((𝐹 ∪ 𝐻) supp 0 )))
225	224	ad2antll 728	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → ((𝐻 supp 0 ) ⊆ ran 𝑓 ↔ (𝐻 supp 0 ) ⊆ ((𝐹 ∪ 𝐻) supp 0 )))
226	223, 225	mpbird 260	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (𝐻 supp 0 ) ⊆ ran 𝑓)
227	76, 226, 82, 220	suppssr 7844	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → (𝐻‘𝑥) = 0 )
228	221, 227	oveq12d 7153	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → ((𝐹‘𝑥) + (𝐻‘𝑥)) = ( 0 + 0 ))
229	8	ad2antrr 725	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → ( 0 + 0 ) = 0 )
230	211, 228, 229	3eqtrd 2837	. . . . . . . 8 ⊢ (((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) ∧ 𝑥 ∈ (𝐴 ∖ ran 𝑓)) → ((𝐹 ∘f + 𝐻)‘𝑥) = 0 )
231	206, 230	suppss 7843	. . . . . . 7 ⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → ((𝐹 ∘f + 𝐻) supp 0 ) ⊆ ran 𝑓)
232		ovex 7168	. . . . . . . . 9 ⊢ (𝐹 ∘f + 𝐻) ∈ V
233	232, 133	coex 7617	. . . . . . . 8 ⊢ ((𝐹 ∘f + 𝐻) ∘ 𝑓) ∈ V
234		suppimacnv 7824	. . . . . . . . 9 ⊢ ((((𝐹 ∘f + 𝐻) ∘ 𝑓) ∈ V ∧ 0 ∈ V) → (((𝐹 ∘f + 𝐻) ∘ 𝑓) supp 0 ) = (◡((𝐹 ∘f + 𝐻) ∘ 𝑓) “ (V ∖ { 0 })))
235	234	eqcomd 2804	. . . . . . . 8 ⊢ ((((𝐹 ∘f + 𝐻) ∘ 𝑓) ∈ V ∧ 0 ∈ V) → (◡((𝐹 ∘f + 𝐻) ∘ 𝑓) “ (V ∖ { 0 })) = (((𝐹 ∘f + 𝐻) ∘ 𝑓) supp 0 ))
236	233, 12, 235	mp2an 691	. . . . . . 7 ⊢ (◡((𝐹 ∘f + 𝐻) ∘ 𝑓) “ (V ∖ { 0 })) = (((𝐹 ∘f + 𝐻) ∘ 𝑓) supp 0 )
237	2, 3, 6, 157, 46, 82, 202, 204, 51, 70, 231, 236	gsumval3 19020	. . . . . 6 ⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (𝐺 Σg (𝐹 ∘f + 𝐻)) = (seq1( + , ((𝐹 ∘f + 𝐻) ∘ 𝑓))‘(♯‘𝑊)))
238		gsumzaddlem.1	. . . . . . . . 9 ⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
239	238	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
240		eqid 2798	. . . . . . . 8 ⊢ ((𝐹 ∘ 𝑓) supp 0 ) = ((𝐹 ∘ 𝑓) supp 0 )
241	2, 3, 6, 157, 46, 82, 54, 239, 51, 70, 219, 240	gsumval3 19020	. . . . . . 7 ⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘𝑊)))
242	161	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → ran 𝐻 ⊆ (𝑍‘ran 𝐻))
243		eqid 2798	. . . . . . . 8 ⊢ ((𝐻 ∘ 𝑓) supp 0 ) = ((𝐻 ∘ 𝑓) supp 0 )
244	2, 3, 6, 157, 46, 82, 76, 242, 51, 70, 226, 243	gsumval3 19020	. . . . . . 7 ⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (𝐺 Σg 𝐻) = (seq1( + , (𝐻 ∘ 𝑓))‘(♯‘𝑊)))
245	241, 244	oveq12d 7153	. . . . . 6 ⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)) = ((seq1( + , (𝐹 ∘ 𝑓))‘(♯‘𝑊)) + (seq1( + , (𝐻 ∘ 𝑓))‘(♯‘𝑊))))
246	201, 237, 245	3eqtr4d 2843	. . . . 5 ⊢ ((𝜑 ∧ ((♯‘𝑊) ∈ ℕ ∧ 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)) → (𝐺 Σg (𝐹 ∘f + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)))
247	246	expr 460	. . . 4 ⊢ ((𝜑 ∧ (♯‘𝑊) ∈ ℕ) → (𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 → (𝐺 Σg (𝐹 ∘f + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))))
248	247	exlimdv 1934	. . 3 ⊢ ((𝜑 ∧ (♯‘𝑊) ∈ ℕ) → (∃𝑓 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 → (𝐺 Σg (𝐹 ∘f + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))))
249	248	expimpd 457	. 2 ⊢ (𝜑 → (((♯‘𝑊) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊) → (𝐺 Σg (𝐹 ∘f + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))))
250		gsumzadd.fn	. . . . 5 ⊢ (𝜑 → 𝐹 finSupp 0 )
251		gsumzadd.hn	. . . . 5 ⊢ (𝜑 → 𝐻 finSupp 0 )
252	250, 251	fsuppun 8836	. . . 4 ⊢ (𝜑 → ((𝐹 ∪ 𝐻) supp 0 ) ∈ Fin)
253	18, 252	eqeltrid 2894	. . 3 ⊢ (𝜑 → 𝑊 ∈ Fin)
254		fz1f1o 15059	. . 3 ⊢ (𝑊 ∈ Fin → (𝑊 = ∅ ∨ ((♯‘𝑊) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)))
255	253, 254	syl 17	. 2 ⊢ (𝜑 → (𝑊 = ∅ ∨ ((♯‘𝑊) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊)))
256	45, 249, 255	mpjaod 857	1 ⊢ (𝜑 → (𝐺 Σg (𝐹 ∘f + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844  ∀wal 1536   = wceq 1538  ∃wex 1781   ∈ wcel 2111  ∀wral 3106  Vcvv 3441   ∖ cdif 3878   ∪ cun 3879   ∩ cin 3880   ⊆ wss 3881  ∅c0 4243  {csn 4525   class class class wbr 5030   ↦ cmpt 5110  ^◡ccnv 5518  dom cdm 5519  ran crn 5520   ↾ cres 5521   “ cima 5522   ∘ ccom 5523   Fn wfn 6319  ⟶wf 6320  –1-1→wf1 6321  –onto→wfo 6322  –1-1-onto→wf1o 6323  ‘cfv 6324  (class class class)co 7135   ∘_f cof 7387   supp csupp 7813  Fincfn 8492   finSupp cfsupp 8817  1c1 10527   + caddc 10529  ℕcn 11625  ℤ_≥cuz 12231  ...cfz 12885  ..^cfzo 13028  seqcseq 13364  ♯chash 13686  Basecbs 16475  +_gcplusg 16557  0_gc0g 16705   Σ_g cgsu 16706  Mndcmnd 17903  Cntzccntz 18437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-int 4839  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-se 5479  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-isom 6333  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-of 7389  df-om 7561  df-1st 7671  df-2nd 7672  df-supp 7814  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-1o 8085  df-oadd 8089  df-er 8272  df-en 8493  df-dom 8494  df-sdom 8495  df-fin 8496  df-fsupp 8818  df-oi 8958  df-card 9352  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-nn 11626  df-n0 11886  df-z 11970  df-uz 12232  df-fz 12886  df-fzo 13029  df-seq 13365  df-hash 13687  df-0g 16707  df-gsum 16708  df-mgm 17844  df-sgrp 17893  df-mnd 17904  df-cntz 18439

This theorem is referenced by:  gsumzadd  19035  dprdfadd  19135