gsumzaddlem

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

	Ref	Expression
Hypotheses	gsumzadd.b	$⊢ B = {Base}_{G}$
	gsumzadd.0	$⊢ \underset{˙}{0} = 0_{G}$
	gsumzadd.p	$⊢ \underset{˙}{+} = +_{G}$
	gsumzadd.z	$⊢ Z = Cntz (G)$
	gsumzadd.g	$⊢ φ \to G \in Mnd$
	gsumzadd.a	$⊢ φ \to A \in V$
	gsumzadd.fn	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (F)$
	gsumzadd.hn	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (H)$
	gsumzaddlem.w	$⊢ W = (F \cup H) supp \underset{˙}{0}$
	gsumzaddlem.f	$⊢ φ \to F : A ⟶ B$
	gsumzaddlem.h	$⊢ φ \to H : A ⟶ B$
	gsumzaddlem.1	$⊢ φ \to ran F \subseteq Z (ran F)$
	gsumzaddlem.2	$⊢ φ \to ran H \subseteq Z (ran H)$
	gsumzaddlem.3	$⊢ φ \to ran (F {\underset{˙}{+}}_{f} H) \subseteq Z (ran (F {\underset{˙}{+}}_{f} H))$
	gsumzaddlem.4	$⊢ (φ \land (x \subseteq A \land k \in (A ∖ x))) \to F (k) \in Z (\{\sum_{G} ({H ↾}_{x})\})$
Assertion	gsumzaddlem	$⊢ φ \to \sum_{G} (F {\underset{˙}{+}}_{f} H) = (\sum_{G}, F) \underset{˙}{+} (\sum_{G}, H)$

Proof

Step	Hyp	Ref	Expression
1		gsumzadd.b	$⊢ B = {Base}_{G}$
2		gsumzadd.0	$⊢ \underset{˙}{0} = 0_{G}$
3		gsumzadd.p	$⊢ \underset{˙}{+} = +_{G}$
4		gsumzadd.z	$⊢ Z = Cntz (G)$
5		gsumzadd.g	$⊢ φ \to G \in Mnd$
6		gsumzadd.a	$⊢ φ \to A \in V$
7		gsumzadd.fn	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (F)$
8		gsumzadd.hn	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (H)$
9		gsumzaddlem.w	$⊢ W = (F \cup H) supp \underset{˙}{0}$
10		gsumzaddlem.f	$⊢ φ \to F : A ⟶ B$
11		gsumzaddlem.h	$⊢ φ \to H : A ⟶ B$
12		gsumzaddlem.1	$⊢ φ \to ran F \subseteq Z (ran F)$
13		gsumzaddlem.2	$⊢ φ \to ran H \subseteq Z (ran H)$
14		gsumzaddlem.3	$⊢ φ \to ran (F {\underset{˙}{+}}_{f} H) \subseteq Z (ran (F {\underset{˙}{+}}_{f} H))$
15		gsumzaddlem.4	$⊢ (φ \land (x \subseteq A \land k \in (A ∖ x))) \to F (k) \in Z (\{\sum_{G} ({H ↾}_{x})\})$
16	1 2	mndidcl	$⊢ G \in Mnd \to \underset{˙}{0} \in B$
17	5 16	syl	$⊢ φ \to \underset{˙}{0} \in B$
18	1 3 2	mndlid	$⊢ (G \in Mnd \land \underset{˙}{0} \in B) \to \underset{˙}{0} \underset{˙}{+} \underset{˙}{0} = \underset{˙}{0}$
19	5 17 18	syl2anc	$⊢ φ \to \underset{˙}{0} \underset{˙}{+} \underset{˙}{0} = \underset{˙}{0}$
20	19	adantr	$⊢ (φ \land W = \emptyset) \to \underset{˙}{0} \underset{˙}{+} \underset{˙}{0} = \underset{˙}{0}$
21	2	fvexi	$⊢ \underset{˙}{0} \in V$
22	21	a1i	$⊢ φ \to \underset{˙}{0} \in V$
23		fex	$⊢ (H : A ⟶ B \land A \in V) \to H \in V$
24	11 6 23	syl2anc	$⊢ φ \to H \in V$
25	24	suppun	$⊢ φ \to F supp \underset{˙}{0} \subseteq (F \cup H) supp \underset{˙}{0}$
26	25 9	sseqtrrdi	$⊢ φ \to F supp \underset{˙}{0} \subseteq W$
27	10 6 22 26	gsumcllem	$⊢ (φ \land W = \emptyset) \to F = (x \in A ⟼ \underset{˙}{0})$
28	27	oveq2d	$⊢ (φ \land W = \emptyset) \to \sum_{G} F = \underset{x \in A}{\sum_{G}} \underset{˙}{0}$
29	2	gsumz	$⊢ (G \in Mnd \land A \in V) \to \underset{x \in A}{\sum_{G}} \underset{˙}{0} = \underset{˙}{0}$
30	5 6 29	syl2anc	$⊢ φ \to \underset{x \in A}{\sum_{G}} \underset{˙}{0} = \underset{˙}{0}$
31	30	adantr	$⊢ (φ \land W = \emptyset) \to \underset{x \in A}{\sum_{G}} \underset{˙}{0} = \underset{˙}{0}$
32	28 31	eqtrd	$⊢ (φ \land W = \emptyset) \to \sum_{G} F = \underset{˙}{0}$
33		fex	$⊢ (F : A ⟶ B \land A \in V) \to F \in V$
34	10 6 33	syl2anc	$⊢ φ \to F \in V$
35	34	suppun	$⊢ φ \to H supp \underset{˙}{0} \subseteq (H \cup F) supp \underset{˙}{0}$
36		uncom	$⊢ F \cup H = H \cup F$
37	36	oveq1i	$⊢ (F \cup H) supp \underset{˙}{0} = (H \cup F) supp \underset{˙}{0}$
38	35 37	sseqtrrdi	$⊢ φ \to H supp \underset{˙}{0} \subseteq (F \cup H) supp \underset{˙}{0}$
39	38 9	sseqtrrdi	$⊢ φ \to H supp \underset{˙}{0} \subseteq W$
40	11 6 22 39	gsumcllem	$⊢ (φ \land W = \emptyset) \to H = (x \in A ⟼ \underset{˙}{0})$
41	40	oveq2d	$⊢ (φ \land W = \emptyset) \to \sum_{G} H = \underset{x \in A}{\sum_{G}} \underset{˙}{0}$
42	41 31	eqtrd	$⊢ (φ \land W = \emptyset) \to \sum_{G} H = \underset{˙}{0}$
43	32 42	oveq12d	$⊢ (φ \land W = \emptyset) \to (\sum_{G}, F) \underset{˙}{+} (\sum_{G}, H) = \underset{˙}{0} \underset{˙}{+} \underset{˙}{0}$
44	6	adantr	$⊢ (φ \land W = \emptyset) \to A \in V$
45	17	ad2antrr	$⊢ ((φ \land W = \emptyset) \land x \in A) \to \underset{˙}{0} \in B$
46	44 45 45 27 40	offval2	$⊢ (φ \land W = \emptyset) \to F {\underset{˙}{+}}_{f} H = (x \in A ⟼ \underset{˙}{0} \underset{˙}{+} \underset{˙}{0})$
47	20	mpteq2dv	$⊢ (φ \land W = \emptyset) \to (x \in A ⟼ \underset{˙}{0} \underset{˙}{+} \underset{˙}{0}) = (x \in A ⟼ \underset{˙}{0})$
48	46 47	eqtrd	$⊢ (φ \land W = \emptyset) \to F {\underset{˙}{+}}_{f} H = (x \in A ⟼ \underset{˙}{0})$
49	48	oveq2d	$⊢ (φ \land W = \emptyset) \to \sum_{G} (F {\underset{˙}{+}}_{f} H) = \underset{x \in A}{\sum_{G}} \underset{˙}{0}$
50	49 31	eqtrd	$⊢ (φ \land W = \emptyset) \to \sum_{G} (F {\underset{˙}{+}}_{f} H) = \underset{˙}{0}$
51	20 43 50	3eqtr4rd	$⊢ (φ \land W = \emptyset) \to \sum_{G} (F {\underset{˙}{+}}_{f} H) = (\sum_{G}, F) \underset{˙}{+} (\sum_{G}, H)$
52	51	ex	$⊢ φ \to (W = \emptyset \to \sum_{G} (F {\underset{˙}{+}}_{f} H) = (\sum_{G}, F) \underset{˙}{+} (\sum_{G}, H))$
53	5	adantr	$⊢ (φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to G \in Mnd$
54	1 3	mndcl	$⊢ (G \in Mnd \land z \in B \land w \in B) \to z \underset{˙}{+} w \in B$
55	54	3expb	$⊢ (G \in Mnd \land (z \in B \land w \in B)) \to z \underset{˙}{+} w \in B$
56	53 55	sylan	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land (z \in B \land w \in B)) \to z \underset{˙}{+} w \in B$
57	56	caovclg	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land (x \in B \land y \in B)) \to x \underset{˙}{+} y \in B$
58		simprl	$⊢ (φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to \|W\| \in ℕ$
59		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
60	58 59	eleqtrdi	$⊢ (φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to \|W\| \in ℤ_{\geq 1}$
61	10	adantr	$⊢ (φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to F : A ⟶ B$
62		f1of1	$⊢ f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \to f : (1 \dots \|W\|) \underset{1-1}{⟶} W$
63	62	ad2antll	$⊢ (φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to f : (1 \dots \|W\|) \underset{1-1}{⟶} W$
64		suppssdm	$⊢ (F \cup H) supp \underset{˙}{0} \subseteq dom (F \cup H)$
65	64	a1i	$⊢ φ \to (F \cup H) supp \underset{˙}{0} \subseteq dom (F \cup H)$
66	9	a1i	$⊢ φ \to W = (F \cup H) supp \underset{˙}{0}$
67		dmun	$⊢ dom (F \cup H) = dom F \cup dom H$
68	10	fdmd	$⊢ φ \to dom F = A$
69	11	fdmd	$⊢ φ \to dom H = A$
70	68 69	uneq12d	$⊢ φ \to dom F \cup dom H = A \cup A$
71		unidm	$⊢ A \cup A = A$
72	70 71	eqtrdi	$⊢ φ \to dom F \cup dom H = A$
73	67 72	syl5req	$⊢ φ \to A = dom (F \cup H)$
74	65 66 73	3sstr4d	$⊢ φ \to W \subseteq A$
75	74	adantr	$⊢ (φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to W \subseteq A$
76		f1ss	$⊢ (f : (1 \dots \|W\|) \underset{1-1}{⟶} W \land W \subseteq A) \to f : (1 \dots \|W\|) \underset{1-1}{⟶} A$
77	63 75 76	syl2anc	$⊢ (φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to f : (1 \dots \|W\|) \underset{1-1}{⟶} A$
78		f1f	$⊢ f : (1 \dots \|W\|) \underset{1-1}{⟶} A \to f : (1 \dots \|W\|) ⟶ A$
79	77 78	syl	$⊢ (φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to f : (1 \dots \|W\|) ⟶ A$
80		fco	$⊢ (F : A ⟶ B \land f : (1 \dots \|W\|) ⟶ A) \to (F \circ f) : (1 \dots \|W\|) ⟶ B$
81	61 79 80	syl2anc	$⊢ (φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to (F \circ f) : (1 \dots \|W\|) ⟶ B$
82	81	ffvelrnda	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land k \in (1 \dots \|W\|)) \to (F \circ f) (k) \in B$
83	11	adantr	$⊢ (φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to H : A ⟶ B$
84		fco	$⊢ (H : A ⟶ B \land f : (1 \dots \|W\|) ⟶ A) \to (H \circ f) : (1 \dots \|W\|) ⟶ B$
85	83 79 84	syl2anc	$⊢ (φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to (H \circ f) : (1 \dots \|W\|) ⟶ B$
86	85	ffvelrnda	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land k \in (1 \dots \|W\|)) \to (H \circ f) (k) \in B$
87	61	ffnd	$⊢ (φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to F Fn A$
88	83	ffnd	$⊢ (φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to H Fn A$
89	6	adantr	$⊢ (φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to A \in V$
90		ovexd	$⊢ (φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to (1 \dots \|W\|) \in V$
91		inidm	$⊢ A \cap A = A$
92	87 88 79 89 89 90 91	ofco	$⊢ (φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to (F {\underset{˙}{+}}_{f} H) \circ f = (F \circ f) {\underset{˙}{+}}_{f} (H \circ f)$
93	92	fveq1d	$⊢ (φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to ((F {\underset{˙}{+}}_{f} H) \circ f) (k) = ((F \circ f) {\underset{˙}{+}}_{f} (H \circ f)) (k)$
94	93	adantr	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land k \in (1 \dots \|W\|)) \to ((F {\underset{˙}{+}}_{f} H) \circ f) (k) = ((F \circ f) {\underset{˙}{+}}_{f} (H \circ f)) (k)$
95		fnfco	$⊢ (F Fn A \land f : (1 \dots \|W\|) ⟶ A) \to (F \circ f) Fn (1 \dots \|W\|)$
96	87 79 95	syl2anc	$⊢ (φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to (F \circ f) Fn (1 \dots \|W\|)$
97		fnfco	$⊢ (H Fn A \land f : (1 \dots \|W\|) ⟶ A) \to (H \circ f) Fn (1 \dots \|W\|)$
98	88 79 97	syl2anc	$⊢ (φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to (H \circ f) Fn (1 \dots \|W\|)$
99		inidm	$⊢ (1 \dots \|W\|) \cap (1 \dots \|W\|) = (1 \dots \|W\|)$
100		eqidd	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land k \in (1 \dots \|W\|)) \to (F \circ f) (k) = (F \circ f) (k)$
101		eqidd	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land k \in (1 \dots \|W\|)) \to (H \circ f) (k) = (H \circ f) (k)$
102	96 98 90 90 99 100 101	ofval	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land k \in (1 \dots \|W\|)) \to ((F \circ f) {\underset{˙}{+}}_{f} (H \circ f)) (k) = (F \circ f) (k) \underset{˙}{+} (H \circ f) (k)$
103	94 102	eqtrd	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land k \in (1 \dots \|W\|)) \to ((F {\underset{˙}{+}}_{f} H) \circ f) (k) = (F \circ f) (k) \underset{˙}{+} (H \circ f) (k)$
104	5	ad2antrr	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land n \in (1 ..^\|W\|)) \to G \in Mnd$
105		elfzouz	$⊢ n \in (1 ..^\|W\|) \to n \in ℤ_{\geq 1}$
106	105	adantl	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land n \in (1 ..^\|W\|)) \to n \in ℤ_{\geq 1}$
107		elfzouz2	$⊢ n \in (1 ..^\|W\|) \to \|W\| \in ℤ_{\geq n}$
108	107	adantl	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land n \in (1 ..^\|W\|)) \to \|W\| \in ℤ_{\geq n}$
109		fzss2	$⊢ \|W\| \in ℤ_{\geq n} \to (1 \dots n) \subseteq (1 \dots \|W\|)$
110	108 109	syl	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land n \in (1 ..^\|W\|)) \to (1 \dots n) \subseteq (1 \dots \|W\|)$
111	110	sselda	$⊢ (((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land n \in (1 ..^\|W\|)) \land k \in (1 \dots n)) \to k \in (1 \dots \|W\|)$
112	82	adantlr	$⊢ (((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land n \in (1 ..^\|W\|)) \land k \in (1 \dots \|W\|)) \to (F \circ f) (k) \in B$
113	111 112	syldan	$⊢ (((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land n \in (1 ..^\|W\|)) \land k \in (1 \dots n)) \to (F \circ f) (k) \in B$
114	1 3	mndcl	$⊢ (G \in Mnd \land k \in B \land x \in B) \to k \underset{˙}{+} x \in B$
115	114	3expb	$⊢ (G \in Mnd \land (k \in B \land x \in B)) \to k \underset{˙}{+} x \in B$
116	104 115	sylan	$⊢ (((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land n \in (1 ..^\|W\|)) \land (k \in B \land x \in B)) \to k \underset{˙}{+} x \in B$
117	106 113 116	seqcl	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land n \in (1 ..^\|W\|)) \to seq 1 (\underset{˙}{+}, (F \circ f)) (n) \in B$
118	86	adantlr	$⊢ (((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land n \in (1 ..^\|W\|)) \land k \in (1 \dots \|W\|)) \to (H \circ f) (k) \in B$
119	111 118	syldan	$⊢ (((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land n \in (1 ..^\|W\|)) \land k \in (1 \dots n)) \to (H \circ f) (k) \in B$
120	106 119 116	seqcl	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land n \in (1 ..^\|W\|)) \to seq 1 (\underset{˙}{+}, (H \circ f)) (n) \in B$
121		fzofzp1	$⊢ n \in (1 ..^\|W\|) \to n + 1 \in (1 \dots \|W\|)$
122		ffvelrn	$⊢ ((F \circ f) : (1 \dots \|W\|) ⟶ B \land n + 1 \in (1 \dots \|W\|)) \to (F \circ f) (n + 1) \in B$
123	81 121 122	syl2an	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land n \in (1 ..^\|W\|)) \to (F \circ f) (n + 1) \in B$
124		ffvelrn	$⊢ ((H \circ f) : (1 \dots \|W\|) ⟶ B \land n + 1 \in (1 \dots \|W\|)) \to (H \circ f) (n + 1) \in B$
125	85 121 124	syl2an	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land n \in (1 ..^\|W\|)) \to (H \circ f) (n + 1) \in B$
126		fvco3	$⊢ (f : (1 \dots \|W\|) ⟶ A \land n + 1 \in (1 \dots \|W\|)) \to (F \circ f) (n + 1) = F (f (n + 1))$
127	79 121 126	syl2an	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land n \in (1 ..^\|W\|)) \to (F \circ f) (n + 1) = F (f (n + 1))$
128		fveq2	$⊢ k = f (n + 1) \to F (k) = F (f (n + 1))$
129	128	eleq1d	$⊢ k = f (n + 1) \to (F (k) \in Z (\{\sum_{G} ({H ↾}_{f [(1 \dots n)]})\}) \leftrightarrow F (f (n + 1)) \in Z (\{\sum_{G} ({H ↾}_{f [(1 \dots n)]})\}))$
130	15	expr	$⊢ (φ \land x \subseteq A) \to (k \in (A ∖ x) \to F (k) \in Z (\{\sum_{G} ({H ↾}_{x})\}))$
131	130	ralrimiv	$⊢ (φ \land x \subseteq A) \to \forall k \in (A ∖ x) F (k) \in Z (\{\sum_{G} ({H ↾}_{x})\})$
132	131	ex	$⊢ φ \to (x \subseteq A \to \forall k \in (A ∖ x) F (k) \in Z (\{\sum_{G} ({H ↾}_{x})\}))$
133	132	alrimiv	$⊢ φ \to \forall x (x \subseteq A \to \forall k \in (A ∖ x) F (k) \in Z (\{\sum_{G} ({H ↾}_{x})\}))$
134	133	ad2antrr	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land n \in (1 ..^\|W\|)) \to \forall x (x \subseteq A \to \forall k \in (A ∖ x) F (k) \in Z (\{\sum_{G} ({H ↾}_{x})\}))$
135		imassrn	$⊢ f [(1 \dots n)] \subseteq ran f$
136	79	adantr	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land n \in (1 ..^\|W\|)) \to f : (1 \dots \|W\|) ⟶ A$
137	136	frnd	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land n \in (1 ..^\|W\|)) \to ran f \subseteq A$
138	135 137	sstrid	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land n \in (1 ..^\|W\|)) \to f [(1 \dots n)] \subseteq A$
139		vex	$⊢ f \in V$
140	139	imaex	$⊢ f [(1 \dots n)] \in V$
141		sseq1	$⊢ x = f [(1 \dots n)] \to (x \subseteq A \leftrightarrow f [(1 \dots n)] \subseteq A)$
142		difeq2	$⊢ x = f [(1 \dots n)] \to A ∖ x = A ∖ f [(1 \dots n)]$
143		reseq2	$⊢ x = f [(1 \dots n)] \to {H ↾}_{x} = {H ↾}_{f [(1 \dots n)]}$
144	143	oveq2d	$⊢ x = f [(1 \dots n)] \to \sum_{G} ({H ↾}_{x}) = \sum_{G} ({H ↾}_{f [(1 \dots n)]})$
145	144	sneqd	$⊢ x = f [(1 \dots n)] \to \{\sum_{G} ({H ↾}_{x})\} = \{\sum_{G} ({H ↾}_{f [(1 \dots n)]})\}$
146	145	fveq2d	$⊢ x = f [(1 \dots n)] \to Z (\{\sum_{G} ({H ↾}_{x})\}) = Z (\{\sum_{G} ({H ↾}_{f [(1 \dots n)]})\})$
147	146	eleq2d	$⊢ x = f [(1 \dots n)] \to (F (k) \in Z (\{\sum_{G} ({H ↾}_{x})\}) \leftrightarrow F (k) \in Z (\{\sum_{G} ({H ↾}_{f [(1 \dots n)]})\}))$
148	142 147	raleqbidv	$⊢ x = f [(1 \dots n)] \to (\forall k \in (A ∖ x) F (k) \in Z (\{\sum_{G} ({H ↾}_{x})\}) \leftrightarrow \forall k \in (A ∖ f [(1 \dots n)]) F (k) \in Z (\{\sum_{G} ({H ↾}_{f [(1 \dots n)]})\}))$
149	141 148	imbi12d	$⊢ x = f [(1 \dots n)] \to ((x \subseteq A \to \forall k \in (A ∖ x) F (k) \in Z (\{\sum_{G} ({H ↾}_{x})\})) \leftrightarrow (f [(1 \dots n)] \subseteq A \to \forall k \in (A ∖ f [(1 \dots n)]) F (k) \in Z (\{\sum_{G} ({H ↾}_{f [(1 \dots n)]})\})))$
150	140 149	spcv	$⊢ \forall x (x \subseteq A \to \forall k \in (A ∖ x) F (k) \in Z (\{\sum_{G} ({H ↾}_{x})\})) \to (f [(1 \dots n)] \subseteq A \to \forall k \in (A ∖ f [(1 \dots n)]) F (k) \in Z (\{\sum_{G} ({H ↾}_{f [(1 \dots n)]})\}))$
151	134 138 150	sylc	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land n \in (1 ..^\|W\|)) \to \forall k \in (A ∖ f [(1 \dots n)]) F (k) \in Z (\{\sum_{G} ({H ↾}_{f [(1 \dots n)]})\})$
152		ffvelrn	$⊢ (f : (1 \dots \|W\|) ⟶ A \land n + 1 \in (1 \dots \|W\|)) \to f (n + 1) \in A$
153	79 121 152	syl2an	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land n \in (1 ..^\|W\|)) \to f (n + 1) \in A$
154		fzp1nel	$⊢ \neg n + 1 \in (1 \dots n)$
155	77	adantr	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land n \in (1 ..^\|W\|)) \to f : (1 \dots \|W\|) \underset{1-1}{⟶} A$
156	121	adantl	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land n \in (1 ..^\|W\|)) \to n + 1 \in (1 \dots \|W\|)$
157		f1elima	$⊢ (f : (1 \dots \|W\|) \underset{1-1}{⟶} A \land n + 1 \in (1 \dots \|W\|) \land (1 \dots n) \subseteq (1 \dots \|W\|)) \to (f (n + 1) \in f [(1 \dots n)] \leftrightarrow n + 1 \in (1 \dots n))$
158	155 156 110 157	syl3anc	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land n \in (1 ..^\|W\|)) \to (f (n + 1) \in f [(1 \dots n)] \leftrightarrow n + 1 \in (1 \dots n))$
159	154 158	mtbiri	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land n \in (1 ..^\|W\|)) \to \neg f (n + 1) \in f [(1 \dots n)]$
160	153 159	eldifd	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land n \in (1 ..^\|W\|)) \to f (n + 1) \in (A ∖ f [(1 \dots n)])$
161	129 151 160	rspcdva	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land n \in (1 ..^\|W\|)) \to F (f (n + 1)) \in Z (\{\sum_{G} ({H ↾}_{f [(1 \dots n)]})\})$
162	127 161	eqeltrd	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land n \in (1 ..^\|W\|)) \to (F \circ f) (n + 1) \in Z (\{\sum_{G} ({H ↾}_{f [(1 \dots n)]})\})$
163	140	a1i	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land n \in (1 ..^\|W\|)) \to f [(1 \dots n)] \in V$
164	11	ad2antrr	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land n \in (1 ..^\|W\|)) \to H : A ⟶ B$
165	164 138	fssresd	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land n \in (1 ..^\|W\|)) \to ({H ↾}_{f [(1 \dots n)]}) : f [(1 \dots n)] ⟶ B$
166	13	ad2antrr	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land n \in (1 ..^\|W\|)) \to ran H \subseteq Z (ran H)$
167		resss	$⊢ {H ↾}_{f [(1 \dots n)]} \subseteq H$
168	167	rnssi	$⊢ ran ({H ↾}_{f [(1 \dots n)]}) \subseteq ran H$
169	4	cntzidss	$⊢ (ran H \subseteq Z (ran H) \land ran ({H ↾}_{f [(1 \dots n)]}) \subseteq ran H) \to ran ({H ↾}_{f [(1 \dots n)]}) \subseteq Z (ran ({H ↾}_{f [(1 \dots n)]}))$
170	166 168 169	sylancl	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land n \in (1 ..^\|W\|)) \to ran ({H ↾}_{f [(1 \dots n)]}) \subseteq Z (ran ({H ↾}_{f [(1 \dots n)]}))$
171	106 59	eleqtrrdi	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land n \in (1 ..^\|W\|)) \to n \in ℕ$
172		f1ores	$⊢ (f : (1 \dots \|W\|) \underset{1-1}{⟶} A \land (1 \dots n) \subseteq (1 \dots \|W\|)) \to ({f ↾}_{(1 \dots n)}) : (1 \dots n) \underset{1-1 onto}{⟶} f [(1 \dots n)]$
173	155 110 172	syl2anc	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land n \in (1 ..^\|W\|)) \to ({f ↾}_{(1 \dots n)}) : (1 \dots n) \underset{1-1 onto}{⟶} f [(1 \dots n)]$
174		f1of1	$⊢ ({f ↾}_{(1 \dots n)}) : (1 \dots n) \underset{1-1 onto}{⟶} f [(1 \dots n)] \to ({f ↾}_{(1 \dots n)}) : (1 \dots n) \underset{1-1}{⟶} f [(1 \dots n)]$
175	173 174	syl	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land n \in (1 ..^\|W\|)) \to ({f ↾}_{(1 \dots n)}) : (1 \dots n) \underset{1-1}{⟶} f [(1 \dots n)]$
176		suppssdm	$⊢ ({H ↾}_{f [(1 \dots n)]}) supp \underset{˙}{0} \subseteq dom ({H ↾}_{f [(1 \dots n)]})$
177		dmres	$⊢ dom ({H ↾}_{f [(1 \dots n)]}) = f [(1 \dots n)] \cap dom H$
178	177	a1i	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land n \in (1 ..^\|W\|)) \to dom ({H ↾}_{f [(1 \dots n)]}) = f [(1 \dots n)] \cap dom H$
179	176 178	sseqtrid	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land n \in (1 ..^\|W\|)) \to ({H ↾}_{f [(1 \dots n)]}) supp \underset{˙}{0} \subseteq f [(1 \dots n)] \cap dom H$
180		inss1	$⊢ f [(1 \dots n)] \cap dom H \subseteq f [(1 \dots n)]$
181		df-ima	$⊢ f [(1 \dots n)] = ran ({f ↾}_{(1 \dots n)})$
182	181	a1i	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land n \in (1 ..^\|W\|)) \to f [(1 \dots n)] = ran ({f ↾}_{(1 \dots n)})$
183	180 182	sseqtrid	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land n \in (1 ..^\|W\|)) \to f [(1 \dots n)] \cap dom H \subseteq ran ({f ↾}_{(1 \dots n)})$
184	179 183	sstrd	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land n \in (1 ..^\|W\|)) \to ({H ↾}_{f [(1 \dots n)]}) supp \underset{˙}{0} \subseteq ran ({f ↾}_{(1 \dots n)})$
185		eqid	$⊢ (({H ↾}_{f [(1 \dots n)]}) \circ ({f ↾}_{(1 \dots n)})) supp \underset{˙}{0} = (({H ↾}_{f [(1 \dots n)]}) \circ ({f ↾}_{(1 \dots n)})) supp \underset{˙}{0}$
186	1 2 3 4 104 163 165 170 171 175 184 185	gsumval3	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land n \in (1 ..^\|W\|)) \to \sum_{G} ({H ↾}_{f [(1 \dots n)]}) = seq 1 (\underset{˙}{+}, (({H ↾}_{f [(1 \dots n)]}) \circ ({f ↾}_{(1 \dots n)}))) (n)$
187	181	eqimss2i	$⊢ ran ({f ↾}_{(1 \dots n)}) \subseteq f [(1 \dots n)]$
188		cores	$⊢ ran ({f ↾}_{(1 \dots n)}) \subseteq f [(1 \dots n)] \to ({H ↾}_{f [(1 \dots n)]}) \circ ({f ↾}_{(1 \dots n)}) = H \circ ({f ↾}_{(1 \dots n)})$
189	187 188	ax-mp	$⊢ ({H ↾}_{f [(1 \dots n)]}) \circ ({f ↾}_{(1 \dots n)}) = H \circ ({f ↾}_{(1 \dots n)})$
190		resco	$⊢ {(H \circ f) ↾}_{(1 \dots n)} = H \circ ({f ↾}_{(1 \dots n)})$
191	189 190	eqtr4i	$⊢ ({H ↾}_{f [(1 \dots n)]}) \circ ({f ↾}_{(1 \dots n)}) = {(H \circ f) ↾}_{(1 \dots n)}$
192	191	fveq1i	$⊢ (({H ↾}_{f [(1 \dots n)]}) \circ ({f ↾}_{(1 \dots n)})) (k) = ({(H \circ f) ↾}_{(1 \dots n)}) (k)$
193		fvres	$⊢ k \in (1 \dots n) \to ({(H \circ f) ↾}_{(1 \dots n)}) (k) = (H \circ f) (k)$
194	192 193	syl5eq	$⊢ k \in (1 \dots n) \to (({H ↾}_{f [(1 \dots n)]}) \circ ({f ↾}_{(1 \dots n)})) (k) = (H \circ f) (k)$
195	194	adantl	$⊢ (((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land n \in (1 ..^\|W\|)) \land k \in (1 \dots n)) \to (({H ↾}_{f [(1 \dots n)]}) \circ ({f ↾}_{(1 \dots n)})) (k) = (H \circ f) (k)$
196	106 195	seqfveq	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land n \in (1 ..^\|W\|)) \to seq 1 (\underset{˙}{+}, (({H ↾}_{f [(1 \dots n)]}) \circ ({f ↾}_{(1 \dots n)}))) (n) = seq 1 (\underset{˙}{+}, (H \circ f)) (n)$
197	186 196	eqtr2d	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land n \in (1 ..^\|W\|)) \to seq 1 (\underset{˙}{+}, (H \circ f)) (n) = \sum_{G} ({H ↾}_{f [(1 \dots n)]})$
198		fvex	$⊢ seq 1 (\underset{˙}{+}, (H \circ f)) (n) \in V$
199	198	elsn	$⊢ seq 1 (\underset{˙}{+}, (H \circ f)) (n) \in \{\sum_{G} ({H ↾}_{f [(1 \dots n)]})\} \leftrightarrow seq 1 (\underset{˙}{+}, (H \circ f)) (n) = \sum_{G} ({H ↾}_{f [(1 \dots n)]})$
200	197 199	sylibr	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land n \in (1 ..^\|W\|)) \to seq 1 (\underset{˙}{+}, (H \circ f)) (n) \in \{\sum_{G} ({H ↾}_{f [(1 \dots n)]})\}$
201	3 4	cntzi	$⊢ ((F \circ f) (n + 1) \in Z (\{\sum_{G} ({H ↾}_{f [(1 \dots n)]})\}) \land seq 1 (\underset{˙}{+}, (H \circ f)) (n) \in \{\sum_{G} ({H ↾}_{f [(1 \dots n)]})\}) \to (F \circ f) (n + 1) \underset{˙}{+} seq 1 (\underset{˙}{+}, (H \circ f)) (n) = seq 1 (\underset{˙}{+}, (H \circ f)) (n) \underset{˙}{+} (F \circ f) (n + 1)$
202	162 200 201	syl2anc	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land n \in (1 ..^\|W\|)) \to (F \circ f) (n + 1) \underset{˙}{+} seq 1 (\underset{˙}{+}, (H \circ f)) (n) = seq 1 (\underset{˙}{+}, (H \circ f)) (n) \underset{˙}{+} (F \circ f) (n + 1)$
203	202	eqcomd	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land n \in (1 ..^\|W\|)) \to seq 1 (\underset{˙}{+}, (H \circ f)) (n) \underset{˙}{+} (F \circ f) (n + 1) = (F \circ f) (n + 1) \underset{˙}{+} seq 1 (\underset{˙}{+}, (H \circ f)) (n)$
204	1 3 104 117 120 123 125 203	mnd4g	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land n \in (1 ..^\|W\|)) \to (seq 1 (\underset{˙}{+}, (F \circ f)) (n) \underset{˙}{+} seq 1 (\underset{˙}{+}, (H \circ f)) (n)) \underset{˙}{+} ((F \circ f) (n + 1) \underset{˙}{+} (H \circ f) (n + 1)) = (seq 1 (\underset{˙}{+}, (F \circ f)) (n) \underset{˙}{+} (F \circ f) (n + 1)) \underset{˙}{+} (seq 1 (\underset{˙}{+}, (H \circ f)) (n) \underset{˙}{+} (H \circ f) (n + 1))$
205	57 57 60 82 86 103 204	seqcaopr3	$⊢ (φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to seq 1 (\underset{˙}{+}, ((F {\underset{˙}{+}}_{f} H) \circ f)) (\|W\|) = seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|) \underset{˙}{+} seq 1 (\underset{˙}{+}, (H \circ f)) (\|W\|)$
206	56 61 83 89 89 91	off	$⊢ (φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to (F {\underset{˙}{+}}_{f} H) : A ⟶ B$
207	14	adantr	$⊢ (φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to ran (F {\underset{˙}{+}}_{f} H) \subseteq Z (ran (F {\underset{˙}{+}}_{f} H))$
208	53 115	sylan	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land (k \in B \land x \in B)) \to k \underset{˙}{+} x \in B$
209	208 61 83 89 89 91	off	$⊢ (φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to (F {\underset{˙}{+}}_{f} H) : A ⟶ B$
210		eldifi	$⊢ x \in (A ∖ ran f) \to x \in A$
211		eqidd	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land x \in A) \to F (x) = F (x)$
212		eqidd	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land x \in A) \to H (x) = H (x)$
213	87 88 89 89 91 211 212	ofval	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land x \in A) \to (F {\underset{˙}{+}}_{f} H) (x) = F (x) \underset{˙}{+} H (x)$
214	210 213	sylan2	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land x \in (A ∖ ran f)) \to (F {\underset{˙}{+}}_{f} H) (x) = F (x) \underset{˙}{+} H (x)$
215	25	adantr	$⊢ (φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to F supp \underset{˙}{0} \subseteq (F \cup H) supp \underset{˙}{0}$
216		f1ofo	$⊢ f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \to f : (1 \dots \|W\|) \underset{onto}{⟶} W$
217		forn	$⊢ f : (1 \dots \|W\|) \underset{onto}{⟶} W \to ran f = W$
218	216 217	syl	$⊢ f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \to ran f = W$
219	218 9	eqtrdi	$⊢ f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \to ran f = (F \cup H) supp \underset{˙}{0}$
220	219	sseq2d	$⊢ f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \to (F supp \underset{˙}{0} \subseteq ran f \leftrightarrow F supp \underset{˙}{0} \subseteq (F \cup H) supp \underset{˙}{0})$
221	220	ad2antll	$⊢ (φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to (F supp \underset{˙}{0} \subseteq ran f \leftrightarrow F supp \underset{˙}{0} \subseteq (F \cup H) supp \underset{˙}{0})$
222	215 221	mpbird	$⊢ (φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to F supp \underset{˙}{0} \subseteq ran f$
223	21	a1i	$⊢ (φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to \underset{˙}{0} \in V$
224	61 222 89 223	suppssr	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land x \in (A ∖ ran f)) \to F (x) = \underset{˙}{0}$
225	35	adantr	$⊢ (φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to H supp \underset{˙}{0} \subseteq (H \cup F) supp \underset{˙}{0}$
226	225 37	sseqtrrdi	$⊢ (φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to H supp \underset{˙}{0} \subseteq (F \cup H) supp \underset{˙}{0}$
227	219	sseq2d	$⊢ f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \to (H supp \underset{˙}{0} \subseteq ran f \leftrightarrow H supp \underset{˙}{0} \subseteq (F \cup H) supp \underset{˙}{0})$
228	227	ad2antll	$⊢ (φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to (H supp \underset{˙}{0} \subseteq ran f \leftrightarrow H supp \underset{˙}{0} \subseteq (F \cup H) supp \underset{˙}{0})$
229	226 228	mpbird	$⊢ (φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to H supp \underset{˙}{0} \subseteq ran f$
230	83 229 89 223	suppssr	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land x \in (A ∖ ran f)) \to H (x) = \underset{˙}{0}$
231	224 230	oveq12d	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land x \in (A ∖ ran f)) \to F (x) \underset{˙}{+} H (x) = \underset{˙}{0} \underset{˙}{+} \underset{˙}{0}$
232	19	ad2antrr	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land x \in (A ∖ ran f)) \to \underset{˙}{0} \underset{˙}{+} \underset{˙}{0} = \underset{˙}{0}$
233	214 231 232	3eqtrd	$⊢ ((φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \land x \in (A ∖ ran f)) \to (F {\underset{˙}{+}}_{f} H) (x) = \underset{˙}{0}$
234	209 233	suppss	$⊢ (φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to (F {\underset{˙}{+}}_{f} H) supp \underset{˙}{0} \subseteq ran f$
235		ovex	$⊢ F {\underset{˙}{+}}_{f} H \in V$
236	235 139	coex	$⊢ (F {\underset{˙}{+}}_{f} H) \circ f \in V$
237		suppimacnv	$⊢ ((F {\underset{˙}{+}}_{f} H) \circ f \in V \land \underset{˙}{0} \in V) \to ((F {\underset{˙}{+}}_{f} H) \circ f) supp \underset{˙}{0} = {((F {\underset{˙}{+}}_{f} H) \circ f)}^{-1} [V ∖ \{\underset{˙}{0}\}]$
238	237	eqcomd	$⊢ ((F {\underset{˙}{+}}_{f} H) \circ f \in V \land \underset{˙}{0} \in V) \to {((F {\underset{˙}{+}}_{f} H) \circ f)}^{-1} [V ∖ \{\underset{˙}{0}\}] = ((F {\underset{˙}{+}}_{f} H) \circ f) supp \underset{˙}{0}$
239	236 21 238	mp2an	$⊢ {((F {\underset{˙}{+}}_{f} H) \circ f)}^{-1} [V ∖ \{\underset{˙}{0}\}] = ((F {\underset{˙}{+}}_{f} H) \circ f) supp \underset{˙}{0}$
240	1 2 3 4 53 89 206 207 58 77 234 239	gsumval3	$⊢ (φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to \sum_{G} (F {\underset{˙}{+}}_{f} H) = seq 1 (\underset{˙}{+}, ((F {\underset{˙}{+}}_{f} H) \circ f)) (\|W\|)$
241	12	adantr	$⊢ (φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to ran F \subseteq Z (ran F)$
242		eqid	$⊢ (F \circ f) supp \underset{˙}{0} = (F \circ f) supp \underset{˙}{0}$
243	1 2 3 4 53 89 61 241 58 77 222 242	gsumval3	$⊢ (φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to \sum_{G} F = seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|)$
244	13	adantr	$⊢ (φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to ran H \subseteq Z (ran H)$
245		eqid	$⊢ (H \circ f) supp \underset{˙}{0} = (H \circ f) supp \underset{˙}{0}$
246	1 2 3 4 53 89 83 244 58 77 229 245	gsumval3	$⊢ (φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to \sum_{G} H = seq 1 (\underset{˙}{+}, (H \circ f)) (\|W\|)$
247	243 246	oveq12d	$⊢ (φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to (\sum_{G}, F) \underset{˙}{+} (\sum_{G}, H) = seq 1 (\underset{˙}{+}, (F \circ f)) (\|W\|) \underset{˙}{+} seq 1 (\underset{˙}{+}, (H \circ f)) (\|W\|)$
248	205 240 247	3eqtr4d	$⊢ (φ \land (\|W\| \in ℕ \land f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W)) \to \sum_{G} (F {\underset{˙}{+}}_{f} H) = (\sum_{G}, F) \underset{˙}{+} (\sum_{G}, H)$
249	248	expr	$⊢ (φ \land \|W\| \in ℕ) \to (f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \to \sum_{G} (F {\underset{˙}{+}}_{f} H) = (\sum_{G}, F) \underset{˙}{+} (\sum_{G}, H))$
250	249	exlimdv	$⊢ (φ \land \|W\| \in ℕ) \to (\exists f f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W \to \sum_{G} (F {\underset{˙}{+}}_{f} H) = (\sum_{G}, F) \underset{˙}{+} (\sum_{G}, H))$
251	250	expimpd	$⊢ φ \to ((\|W\| \in ℕ \land \exists f f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W) \to \sum_{G} (F {\underset{˙}{+}}_{f} H) = (\sum_{G}, F) \underset{˙}{+} (\sum_{G}, H))$
252	7 8	fsuppun	$⊢ φ \to (F \cup H) supp \underset{˙}{0} \in Fin$
253	9 252	eqeltrid	$⊢ φ \to W \in Fin$
254		fz1f1o	$⊢ W \in Fin \to (W = \emptyset \lor (\|W\| \in ℕ \land \exists f f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W))$
255	253 254	syl	$⊢ φ \to (W = \emptyset \lor (\|W\| \in ℕ \land \exists f f : (1 \dots \|W\|) \underset{1-1 onto}{⟶} W))$
256	52 251 255	mpjaod	$⊢ φ \to \sum_{G} (F {\underset{˙}{+}}_{f} H) = (\sum_{G}, F) \underset{˙}{+} (\sum_{G}, H)$

Metamath Proof Explorer

Theorem gsumzaddlem

Proof