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

Metamath Proof Explorer

Theorem gsumzaddlem

Proof