gsum2dlem2

Description: Lemma for gsum2d . (Contributed by Mario Carneiro, 28-Dec-2014) (Revised by AV, 8-Jun-2019)

	Ref	Expression
Hypotheses	gsum2d.b	$⊢ B = {Base}_{G}$
	gsum2d.z	$⊢ \underset{˙}{0} = 0_{G}$
	gsum2d.g	$⊢ φ \to G \in CMnd$
	gsum2d.a	$⊢ φ \to A \in V$
	gsum2d.r	$⊢ φ \to Rel A$
	gsum2d.d	$⊢ φ \to D \in W$
	gsum2d.s	$⊢ φ \to dom A \subseteq D$
	gsum2d.f	$⊢ φ \to F : A ⟶ B$
	gsum2d.w	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (F)$
Assertion	gsum2dlem2	$⊢ φ \to \sum_{G} ({F ↾}_{({A ↾}_{dom {supp}_{\underset{˙}{0}} (F)})}) = \underset{j \in dom {supp}_{\underset{˙}{0}} (F)}{\sum_{G}} (\underset{k \in A [\{j\}]}{\sum_{G}}, (j F k))$

Proof

Step	Hyp	Ref	Expression
1		gsum2d.b	$⊢ B = {Base}_{G}$
2		gsum2d.z	$⊢ \underset{˙}{0} = 0_{G}$
3		gsum2d.g	$⊢ φ \to G \in CMnd$
4		gsum2d.a	$⊢ φ \to A \in V$
5		gsum2d.r	$⊢ φ \to Rel A$
6		gsum2d.d	$⊢ φ \to D \in W$
7		gsum2d.s	$⊢ φ \to dom A \subseteq D$
8		gsum2d.f	$⊢ φ \to F : A ⟶ B$
9		gsum2d.w	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (F)$
10	9	fsuppimpd	$⊢ φ \to F supp \underset{˙}{0} \in Fin$
11		dmfi	$⊢ F supp \underset{˙}{0} \in Fin \to dom {supp}_{\underset{˙}{0}} (F) \in Fin$
12	10 11	syl	$⊢ φ \to dom {supp}_{\underset{˙}{0}} (F) \in Fin$
13		reseq2	$⊢ x = \emptyset \to {A ↾}_{x} = {A ↾}_{\emptyset}$
14		res0	$⊢ {A ↾}_{\emptyset} = \emptyset$
15	13 14	eqtrdi	$⊢ x = \emptyset \to {A ↾}_{x} = \emptyset$
16	15	reseq2d	$⊢ x = \emptyset \to {F ↾}_{({A ↾}_{x})} = {F ↾}_{\emptyset}$
17		res0	$⊢ {F ↾}_{\emptyset} = \emptyset$
18	16 17	eqtrdi	$⊢ x = \emptyset \to {F ↾}_{({A ↾}_{x})} = \emptyset$
19	18	oveq2d	$⊢ x = \emptyset \to \sum_{G} ({F ↾}_{({A ↾}_{x})}) = \sum_{G} \emptyset$
20		mpteq1	$⊢ x = \emptyset \to (j \in x ⟼ \underset{k \in A [\{j\}]}{\sum_{G}} (j F k)) = (j \in \emptyset ⟼ \underset{k \in A [\{j\}]}{\sum_{G}} (j F k))$
21		mpt0	$⊢ (j \in \emptyset ⟼ \underset{k \in A [\{j\}]}{\sum_{G}} (j F k)) = \emptyset$
22	20 21	eqtrdi	$⊢ x = \emptyset \to (j \in x ⟼ \underset{k \in A [\{j\}]}{\sum_{G}} (j F k)) = \emptyset$
23	22	oveq2d	$⊢ x = \emptyset \to \underset{j \in x}{\sum_{G}} (\underset{k \in A [\{j\}]}{\sum_{G}}, (j F k)) = \sum_{G} \emptyset$
24	19 23	eqeq12d	$⊢ x = \emptyset \to (\sum_{G} ({F ↾}_{({A ↾}_{x})}) = \underset{j \in x}{\sum_{G}} (\underset{k \in A [\{j\}]}{\sum_{G}}, (j F k)) \leftrightarrow \sum_{G} \emptyset = \sum_{G} \emptyset)$
25	24	imbi2d	$⊢ x = \emptyset \to ((φ \to \sum_{G} ({F ↾}_{({A ↾}_{x})}) = \underset{j \in x}{\sum_{G}} (\underset{k \in A [\{j\}]}{\sum_{G}}, (j F k))) \leftrightarrow (φ \to \sum_{G} \emptyset = \sum_{G} \emptyset))$
26		reseq2	$⊢ x = y \to {A ↾}_{x} = {A ↾}_{y}$
27	26	reseq2d	$⊢ x = y \to {F ↾}_{({A ↾}_{x})} = {F ↾}_{({A ↾}_{y})}$
28	27	oveq2d	$⊢ x = y \to \sum_{G} ({F ↾}_{({A ↾}_{x})}) = \sum_{G} ({F ↾}_{({A ↾}_{y})})$
29		mpteq1	$⊢ x = y \to (j \in x ⟼ \underset{k \in A [\{j\}]}{\sum_{G}} (j F k)) = (j \in y ⟼ \underset{k \in A [\{j\}]}{\sum_{G}} (j F k))$
30	29	oveq2d	$⊢ x = y \to \underset{j \in x}{\sum_{G}} (\underset{k \in A [\{j\}]}{\sum_{G}}, (j F k)) = \underset{j \in y}{\sum_{G}} (\underset{k \in A [\{j\}]}{\sum_{G}}, (j F k))$
31	28 30	eqeq12d	$⊢ x = y \to (\sum_{G} ({F ↾}_{({A ↾}_{x})}) = \underset{j \in x}{\sum_{G}} (\underset{k \in A [\{j\}]}{\sum_{G}}, (j F k)) \leftrightarrow \sum_{G} ({F ↾}_{({A ↾}_{y})}) = \underset{j \in y}{\sum_{G}} (\underset{k \in A [\{j\}]}{\sum_{G}}, (j F k)))$
32	31	imbi2d	$⊢ x = y \to ((φ \to \sum_{G} ({F ↾}_{({A ↾}_{x})}) = \underset{j \in x}{\sum_{G}} (\underset{k \in A [\{j\}]}{\sum_{G}}, (j F k))) \leftrightarrow (φ \to \sum_{G} ({F ↾}_{({A ↾}_{y})}) = \underset{j \in y}{\sum_{G}} (\underset{k \in A [\{j\}]}{\sum_{G}}, (j F k))))$
33		reseq2	$⊢ x = y \cup \{z\} \to {A ↾}_{x} = {A ↾}_{(y \cup \{z\})}$
34	33	reseq2d	$⊢ x = y \cup \{z\} \to {F ↾}_{({A ↾}_{x})} = {F ↾}_{({A ↾}_{(y \cup \{z\})})}$
35	34	oveq2d	$⊢ x = y \cup \{z\} \to \sum_{G} ({F ↾}_{({A ↾}_{x})}) = \sum_{G} ({F ↾}_{({A ↾}_{(y \cup \{z\})})})$
36		mpteq1	$⊢ x = y \cup \{z\} \to (j \in x ⟼ \underset{k \in A [\{j\}]}{\sum_{G}} (j F k)) = (j \in (y \cup \{z\}) ⟼ \underset{k \in A [\{j\}]}{\sum_{G}} (j F k))$
37	36	oveq2d	$⊢ x = y \cup \{z\} \to \underset{j \in x}{\sum_{G}} (\underset{k \in A [\{j\}]}{\sum_{G}}, (j F k)) = \underset{j \in y \cup \{z\}}{\sum_{G}} (\underset{k \in A [\{j\}]}{\sum_{G}}, (j F k))$
38	35 37	eqeq12d	$⊢ x = y \cup \{z\} \to (\sum_{G} ({F ↾}_{({A ↾}_{x})}) = \underset{j \in x}{\sum_{G}} (\underset{k \in A [\{j\}]}{\sum_{G}}, (j F k)) \leftrightarrow \sum_{G} ({F ↾}_{({A ↾}_{(y \cup \{z\})})}) = \underset{j \in y \cup \{z\}}{\sum_{G}} (\underset{k \in A [\{j\}]}{\sum_{G}}, (j F k)))$
39	38	imbi2d	$⊢ x = y \cup \{z\} \to ((φ \to \sum_{G} ({F ↾}_{({A ↾}_{x})}) = \underset{j \in x}{\sum_{G}} (\underset{k \in A [\{j\}]}{\sum_{G}}, (j F k))) \leftrightarrow (φ \to \sum_{G} ({F ↾}_{({A ↾}_{(y \cup \{z\})})}) = \underset{j \in y \cup \{z\}}{\sum_{G}} (\underset{k \in A [\{j\}]}{\sum_{G}}, (j F k))))$
40		reseq2	$⊢ x = dom {supp}_{\underset{˙}{0}} (F) \to {A ↾}_{x} = {A ↾}_{dom {supp}_{\underset{˙}{0}} (F)}$
41	40	reseq2d	$⊢ x = dom {supp}_{\underset{˙}{0}} (F) \to {F ↾}_{({A ↾}_{x})} = {F ↾}_{({A ↾}_{dom {supp}_{\underset{˙}{0}} (F)})}$
42	41	oveq2d	$⊢ x = dom {supp}_{\underset{˙}{0}} (F) \to \sum_{G} ({F ↾}_{({A ↾}_{x})}) = \sum_{G} ({F ↾}_{({A ↾}_{dom {supp}_{\underset{˙}{0}} (F)})})$
43		mpteq1	$⊢ x = dom {supp}_{\underset{˙}{0}} (F) \to (j \in x ⟼ \underset{k \in A [\{j\}]}{\sum_{G}} (j F k)) = (j \in dom {supp}_{\underset{˙}{0}} (F) ⟼ \underset{k \in A [\{j\}]}{\sum_{G}} (j F k))$
44	43	oveq2d	$⊢ x = dom {supp}_{\underset{˙}{0}} (F) \to \underset{j \in x}{\sum_{G}} (\underset{k \in A [\{j\}]}{\sum_{G}}, (j F k)) = \underset{j \in dom {supp}_{\underset{˙}{0}} (F)}{\sum_{G}} (\underset{k \in A [\{j\}]}{\sum_{G}}, (j F k))$
45	42 44	eqeq12d	$⊢ x = dom {supp}_{\underset{˙}{0}} (F) \to (\sum_{G} ({F ↾}_{({A ↾}_{x})}) = \underset{j \in x}{\sum_{G}} (\underset{k \in A [\{j\}]}{\sum_{G}}, (j F k)) \leftrightarrow \sum_{G} ({F ↾}_{({A ↾}_{dom {supp}_{\underset{˙}{0}} (F)})}) = \underset{j \in dom {supp}_{\underset{˙}{0}} (F)}{\sum_{G}} (\underset{k \in A [\{j\}]}{\sum_{G}}, (j F k)))$
46	45	imbi2d	$⊢ x = dom {supp}_{\underset{˙}{0}} (F) \to ((φ \to \sum_{G} ({F ↾}_{({A ↾}_{x})}) = \underset{j \in x}{\sum_{G}} (\underset{k \in A [\{j\}]}{\sum_{G}}, (j F k))) \leftrightarrow (φ \to \sum_{G} ({F ↾}_{({A ↾}_{dom {supp}_{\underset{˙}{0}} (F)})}) = \underset{j \in dom {supp}_{\underset{˙}{0}} (F)}{\sum_{G}} (\underset{k \in A [\{j\}]}{\sum_{G}}, (j F k))))$
47		eqidd	$⊢ φ \to \sum_{G} \emptyset = \sum_{G} \emptyset$
48		oveq1	$⊢ \sum_{G} ({F ↾}_{({A ↾}_{y})}) = \underset{j \in y}{\sum_{G}} (\underset{k \in A [\{j\}]}{\sum_{G}}, (j F k)) \to (\sum_{G}, ({F ↾}_{({A ↾}_{y})})) +_{G} (\sum_{G}, ({F ↾}_{({A ↾}_{\{z\}})})) = (\underset{j \in y}{\sum_{G}}, (\underset{k \in A [\{j\}]}{\sum_{G}}, (j F k))) +_{G} (\sum_{G}, ({F ↾}_{({A ↾}_{\{z\}})}))$
49		eqid	$⊢ +_{G} = +_{G}$
50	3	adantr	$⊢ (φ \land (y \in Fin \land \neg z \in y)) \to G \in CMnd$
51	4	resexd	$⊢ φ \to {A ↾}_{(y \cup \{z\})} \in V$
52	51	adantr	$⊢ (φ \land (y \in Fin \land \neg z \in y)) \to {A ↾}_{(y \cup \{z\})} \in V$
53		resss	$⊢ {A ↾}_{(y \cup \{z\})} \subseteq A$
54		fssres	$⊢ (F : A ⟶ B \land {A ↾}_{(y \cup \{z\})} \subseteq A) \to ({F ↾}_{({A ↾}_{(y \cup \{z\})})}) : {A ↾}_{(y \cup \{z\})} ⟶ B$
55	8 53 54	sylancl	$⊢ φ \to ({F ↾}_{({A ↾}_{(y \cup \{z\})})}) : {A ↾}_{(y \cup \{z\})} ⟶ B$
56	55	adantr	$⊢ (φ \land (y \in Fin \land \neg z \in y)) \to ({F ↾}_{({A ↾}_{(y \cup \{z\})})}) : {A ↾}_{(y \cup \{z\})} ⟶ B$
57	8	ffund	$⊢ φ \to Fun F$
58	57	funresd	$⊢ φ \to Fun ({F ↾}_{({A ↾}_{(y \cup \{z\})})})$
59	58	adantr	$⊢ (φ \land (y \in Fin \land \neg z \in y)) \to Fun ({F ↾}_{({A ↾}_{(y \cup \{z\})})})$
60	10	adantr	$⊢ (φ \land (y \in Fin \land \neg z \in y)) \to F supp \underset{˙}{0} \in Fin$
61	8 4	fexd	$⊢ φ \to F \in V$
62	2	fvexi	$⊢ \underset{˙}{0} \in V$
63		ressuppss	$⊢ (F \in V \land \underset{˙}{0} \in V) \to ({F ↾}_{({A ↾}_{(y \cup \{z\})})}) supp \underset{˙}{0} \subseteq F supp \underset{˙}{0}$
64	61 62 63	sylancl	$⊢ φ \to ({F ↾}_{({A ↾}_{(y \cup \{z\})})}) supp \underset{˙}{0} \subseteq F supp \underset{˙}{0}$
65	64	adantr	$⊢ (φ \land (y \in Fin \land \neg z \in y)) \to ({F ↾}_{({A ↾}_{(y \cup \{z\})})}) supp \underset{˙}{0} \subseteq F supp \underset{˙}{0}$
66	60 65	ssfid	$⊢ (φ \land (y \in Fin \land \neg z \in y)) \to ({F ↾}_{({A ↾}_{(y \cup \{z\})})}) supp \underset{˙}{0} \in Fin$
67	61	resexd	$⊢ φ \to {F ↾}_{({A ↾}_{(y \cup \{z\})})} \in V$
68		isfsupp	$⊢ ({F ↾}_{({A ↾}_{(y \cup \{z\})})} \in V \land \underset{˙}{0} \in V) \to ({finSupp}_{\underset{˙}{0}} (({F ↾}_{({A ↾}_{(y \cup \{z\})})})) \leftrightarrow (Fun ({F ↾}_{({A ↾}_{(y \cup \{z\})})}) \land ({F ↾}_{({A ↾}_{(y \cup \{z\})})}) supp \underset{˙}{0} \in Fin))$
69	67 62 68	sylancl	$⊢ φ \to ({finSupp}_{\underset{˙}{0}} (({F ↾}_{({A ↾}_{(y \cup \{z\})})})) \leftrightarrow (Fun ({F ↾}_{({A ↾}_{(y \cup \{z\})})}) \land ({F ↾}_{({A ↾}_{(y \cup \{z\})})}) supp \underset{˙}{0} \in Fin))$
70	69	adantr	$⊢ (φ \land (y \in Fin \land \neg z \in y)) \to ({finSupp}_{\underset{˙}{0}} (({F ↾}_{({A ↾}_{(y \cup \{z\})})})) \leftrightarrow (Fun ({F ↾}_{({A ↾}_{(y \cup \{z\})})}) \land ({F ↾}_{({A ↾}_{(y \cup \{z\})})}) supp \underset{˙}{0} \in Fin))$
71	59 66 70	mpbir2and	$⊢ (φ \land (y \in Fin \land \neg z \in y)) \to {finSupp}_{\underset{˙}{0}} (({F ↾}_{({A ↾}_{(y \cup \{z\})})}))$
72		simprr	$⊢ (φ \land (y \in Fin \land \neg z \in y)) \to \neg z \in y$
73		disjsn	$⊢ y \cap \{z\} = \emptyset \leftrightarrow \neg z \in y$
74	72 73	sylibr	$⊢ (φ \land (y \in Fin \land \neg z \in y)) \to y \cap \{z\} = \emptyset$
75	74	reseq2d	$⊢ (φ \land (y \in Fin \land \neg z \in y)) \to {A ↾}_{(y \cap \{z\})} = {A ↾}_{\emptyset}$
76		resindi	$⊢ {A ↾}_{(y \cap \{z\})} = ({A ↾}_{y}) \cap ({A ↾}_{\{z\}})$
77	75 76 14	3eqtr3g	$⊢ (φ \land (y \in Fin \land \neg z \in y)) \to ({A ↾}_{y}) \cap ({A ↾}_{\{z\}}) = \emptyset$
78		resundi	$⊢ {A ↾}_{(y \cup \{z\})} = ({A ↾}_{y}) \cup ({A ↾}_{\{z\}})$
79	78	a1i	$⊢ (φ \land (y \in Fin \land \neg z \in y)) \to {A ↾}_{(y \cup \{z\})} = ({A ↾}_{y}) \cup ({A ↾}_{\{z\}})$
80	1 2 49 50 52 56 71 77 79	gsumsplit	$⊢ (φ \land (y \in Fin \land \neg z \in y)) \to \sum_{G} ({F ↾}_{({A ↾}_{(y \cup \{z\})})}) = (\sum_{G}, ({({F ↾}_{({A ↾}_{(y \cup \{z\})})}) ↾}_{({A ↾}_{y})})) +_{G} (\sum_{G}, ({({F ↾}_{({A ↾}_{(y \cup \{z\})})}) ↾}_{({A ↾}_{\{z\}})}))$
81		ssun1	$⊢ y \subseteq y \cup \{z\}$
82		ssres2	$⊢ y \subseteq y \cup \{z\} \to {A ↾}_{y} \subseteq {A ↾}_{(y \cup \{z\})}$
83		resabs1	$⊢ {A ↾}_{y} \subseteq {A ↾}_{(y \cup \{z\})} \to {({F ↾}_{({A ↾}_{(y \cup \{z\})})}) ↾}_{({A ↾}_{y})} = {F ↾}_{({A ↾}_{y})}$
84	81 82 83	mp2b	$⊢ {({F ↾}_{({A ↾}_{(y \cup \{z\})})}) ↾}_{({A ↾}_{y})} = {F ↾}_{({A ↾}_{y})}$
85	84	oveq2i	$⊢ \sum_{G} ({({F ↾}_{({A ↾}_{(y \cup \{z\})})}) ↾}_{({A ↾}_{y})}) = \sum_{G} ({F ↾}_{({A ↾}_{y})})$
86		ssun2	$⊢ \{z\} \subseteq y \cup \{z\}$
87		ssres2	$⊢ \{z\} \subseteq y \cup \{z\} \to {A ↾}_{\{z\}} \subseteq {A ↾}_{(y \cup \{z\})}$
88		resabs1	$⊢ {A ↾}_{\{z\}} \subseteq {A ↾}_{(y \cup \{z\})} \to {({F ↾}_{({A ↾}_{(y \cup \{z\})})}) ↾}_{({A ↾}_{\{z\}})} = {F ↾}_{({A ↾}_{\{z\}})}$
89	86 87 88	mp2b	$⊢ {({F ↾}_{({A ↾}_{(y \cup \{z\})})}) ↾}_{({A ↾}_{\{z\}})} = {F ↾}_{({A ↾}_{\{z\}})}$
90	89	oveq2i	$⊢ \sum_{G} ({({F ↾}_{({A ↾}_{(y \cup \{z\})})}) ↾}_{({A ↾}_{\{z\}})}) = \sum_{G} ({F ↾}_{({A ↾}_{\{z\}})})$
91	85 90	oveq12i	$⊢ (\sum_{G}, ({({F ↾}_{({A ↾}_{(y \cup \{z\})})}) ↾}_{({A ↾}_{y})})) +_{G} (\sum_{G}, ({({F ↾}_{({A ↾}_{(y \cup \{z\})})}) ↾}_{({A ↾}_{\{z\}})})) = (\sum_{G}, ({F ↾}_{({A ↾}_{y})})) +_{G} (\sum_{G}, ({F ↾}_{({A ↾}_{\{z\}})}))$
92	80 91	eqtrdi	$⊢ (φ \land (y \in Fin \land \neg z \in y)) \to \sum_{G} ({F ↾}_{({A ↾}_{(y \cup \{z\})})}) = (\sum_{G}, ({F ↾}_{({A ↾}_{y})})) +_{G} (\sum_{G}, ({F ↾}_{({A ↾}_{\{z\}})}))$
93		simprl	$⊢ (φ \land (y \in Fin \land \neg z \in y)) \to y \in Fin$
94	1 2 3 4 5 6 7 8 9	gsum2dlem1	$⊢ φ \to \underset{k \in A [\{j\}]}{\sum_{G}} (j F k) \in B$
95	94	ad2antrr	$⊢ ((φ \land (y \in Fin \land \neg z \in y)) \land j \in y) \to \underset{k \in A [\{j\}]}{\sum_{G}} (j F k) \in B$
96		vex	$⊢ z \in V$
97	96	a1i	$⊢ (φ \land (y \in Fin \land \neg z \in y)) \to z \in V$
98		sneq	$⊢ j = z \to \{j\} = \{z\}$
99	98	imaeq2d	$⊢ j = z \to A [\{j\}] = A [\{z\}]$
100		oveq1	$⊢ j = z \to j F k = z F k$
101	99 100	mpteq12dv	$⊢ j = z \to (k \in A [\{j\}] ⟼ j F k) = (k \in A [\{z\}] ⟼ z F k)$
102	101	oveq2d	$⊢ j = z \to \underset{k \in A [\{j\}]}{\sum_{G}} (j F k) = \underset{k \in A [\{z\}]}{\sum_{G}} (z F k)$
103	102	eleq1d	$⊢ j = z \to (\underset{k \in A [\{j\}]}{\sum_{G}} (j F k) \in B \leftrightarrow \underset{k \in A [\{z\}]}{\sum_{G}} (z F k) \in B)$
104	103	imbi2d	$⊢ j = z \to ((φ \to \underset{k \in A [\{j\}]}{\sum_{G}} (j F k) \in B) \leftrightarrow (φ \to \underset{k \in A [\{z\}]}{\sum_{G}} (z F k) \in B))$
105	104 94	chvarvv	$⊢ φ \to \underset{k \in A [\{z\}]}{\sum_{G}} (z F k) \in B$
106	105	adantr	$⊢ (φ \land (y \in Fin \land \neg z \in y)) \to \underset{k \in A [\{z\}]}{\sum_{G}} (z F k) \in B$
107	1 49 50 93 95 97 72 106 102	gsumunsn	$⊢ (φ \land (y \in Fin \land \neg z \in y)) \to \underset{j \in y \cup \{z\}}{\sum_{G}} (\underset{k \in A [\{j\}]}{\sum_{G}}, (j F k)) = (\underset{j \in y}{\sum_{G}}, (\underset{k \in A [\{j\}]}{\sum_{G}}, (j F k))) +_{G} (\underset{k \in A [\{z\}]}{\sum_{G}}, (z F k))$
108	98	reseq2d	$⊢ j = z \to {A ↾}_{\{j\}} = {A ↾}_{\{z\}}$
109	108	reseq2d	$⊢ j = z \to {F ↾}_{({A ↾}_{\{j\}})} = {F ↾}_{({A ↾}_{\{z\}})}$
110	109	oveq2d	$⊢ j = z \to \sum_{G} ({F ↾}_{({A ↾}_{\{j\}})}) = \sum_{G} ({F ↾}_{({A ↾}_{\{z\}})})$
111	102 110	eqeq12d	$⊢ j = z \to (\underset{k \in A [\{j\}]}{\sum_{G}} (j F k) = \sum_{G} ({F ↾}_{({A ↾}_{\{j\}})}) \leftrightarrow \underset{k \in A [\{z\}]}{\sum_{G}} (z F k) = \sum_{G} ({F ↾}_{({A ↾}_{\{z\}})}))$
112	111	imbi2d	$⊢ j = z \to ((φ \to \underset{k \in A [\{j\}]}{\sum_{G}} (j F k) = \sum_{G} ({F ↾}_{({A ↾}_{\{j\}})})) \leftrightarrow (φ \to \underset{k \in A [\{z\}]}{\sum_{G}} (z F k) = \sum_{G} ({F ↾}_{({A ↾}_{\{z\}})})))$
113		imaexg	$⊢ A \in V \to A [\{j\}] \in V$
114	4 113	syl	$⊢ φ \to A [\{j\}] \in V$
115		vex	$⊢ j \in V$
116		vex	$⊢ k \in V$
117	115 116	elimasn	$⊢ k \in A [\{j\}] \leftrightarrow ⟨j, k⟩ \in A$
118		df-ov	$⊢ j F k = F (⟨j, k⟩)$
119	8	ffvelrnda	$⊢ (φ \land ⟨j, k⟩ \in A) \to F (⟨j, k⟩) \in B$
120	118 119	eqeltrid	$⊢ (φ \land ⟨j, k⟩ \in A) \to j F k \in B$
121	117 120	sylan2b	$⊢ (φ \land k \in A [\{j\}]) \to j F k \in B$
122	121	fmpttd	$⊢ φ \to (k \in A [\{j\}] ⟼ j F k) : A [\{j\}] ⟶ B$
123		funmpt	$⊢ Fun (k \in A [\{j\}] ⟼ j F k)$
124	123	a1i	$⊢ φ \to Fun (k \in A [\{j\}] ⟼ j F k)$
125		rnfi	$⊢ F supp \underset{˙}{0} \in Fin \to ran {supp}_{\underset{˙}{0}} (F) \in Fin$
126	10 125	syl	$⊢ φ \to ran {supp}_{\underset{˙}{0}} (F) \in Fin$
127	117	biimpi	$⊢ k \in A [\{j\}] \to ⟨j, k⟩ \in A$
128	115 116	opelrn	$⊢ ⟨j, k⟩ \in {supp}_{\underset{˙}{0}} (F) \to k \in ran {supp}_{\underset{˙}{0}} (F)$
129	128	con3i	$⊢ \neg k \in ran {supp}_{\underset{˙}{0}} (F) \to \neg ⟨j, k⟩ \in {supp}_{\underset{˙}{0}} (F)$
130	127 129	anim12i	$⊢ (k \in A [\{j\}] \land \neg k \in ran {supp}_{\underset{˙}{0}} (F)) \to (⟨j, k⟩ \in A \land \neg ⟨j, k⟩ \in {supp}_{\underset{˙}{0}} (F))$
131		eldif	$⊢ k \in (A [\{j\}] ∖ ran {supp}_{\underset{˙}{0}} (F)) \leftrightarrow (k \in A [\{j\}] \land \neg k \in ran {supp}_{\underset{˙}{0}} (F))$
132		eldif	$⊢ ⟨j, k⟩ \in (A ∖ {supp}_{\underset{˙}{0}} (F)) \leftrightarrow (⟨j, k⟩ \in A \land \neg ⟨j, k⟩ \in {supp}_{\underset{˙}{0}} (F))$
133	130 131 132	3imtr4i	$⊢ k \in (A [\{j\}] ∖ ran {supp}_{\underset{˙}{0}} (F)) \to ⟨j, k⟩ \in (A ∖ {supp}_{\underset{˙}{0}} (F))$
134		ssidd	$⊢ φ \to F supp \underset{˙}{0} \subseteq F supp \underset{˙}{0}$
135	62	a1i	$⊢ φ \to \underset{˙}{0} \in V$
136	8 134 4 135	suppssr	$⊢ (φ \land ⟨j, k⟩ \in (A ∖ {supp}_{\underset{˙}{0}} (F))) \to F (⟨j, k⟩) = \underset{˙}{0}$
137	118 136	eqtrid	$⊢ (φ \land ⟨j, k⟩ \in (A ∖ {supp}_{\underset{˙}{0}} (F))) \to j F k = \underset{˙}{0}$
138	133 137	sylan2	$⊢ (φ \land k \in (A [\{j\}] ∖ ran {supp}_{\underset{˙}{0}} (F))) \to j F k = \underset{˙}{0}$
139	138 114	suppss2	$⊢ φ \to (k \in A [\{j\}] ⟼ j F k) supp \underset{˙}{0} \subseteq ran {supp}_{\underset{˙}{0}} (F)$
140	126 139	ssfid	$⊢ φ \to (k \in A [\{j\}] ⟼ j F k) supp \underset{˙}{0} \in Fin$
141	114	mptexd	$⊢ φ \to (k \in A [\{j\}] ⟼ j F k) \in V$
142		isfsupp	$⊢ ((k \in A [\{j\}] ⟼ j F k) \in V \land \underset{˙}{0} \in V) \to ({finSupp}_{\underset{˙}{0}} ((k \in A [\{j\}] ⟼ j F k)) \leftrightarrow (Fun (k \in A [\{j\}] ⟼ j F k) \land (k \in A [\{j\}] ⟼ j F k) supp \underset{˙}{0} \in Fin))$
143	141 62 142	sylancl	$⊢ φ \to ({finSupp}_{\underset{˙}{0}} ((k \in A [\{j\}] ⟼ j F k)) \leftrightarrow (Fun (k \in A [\{j\}] ⟼ j F k) \land (k \in A [\{j\}] ⟼ j F k) supp \underset{˙}{0} \in Fin))$
144	124 140 143	mpbir2and	$⊢ φ \to {finSupp}_{\underset{˙}{0}} ((k \in A [\{j\}] ⟼ j F k))$
145		2ndconst	$⊢ j \in V \to ({2^{nd} ↾}_{(\{j\} \times A [\{j\}])}) : \{j\} \times A [\{j\}] \underset{1-1 onto}{⟶} A [\{j\}]$
146	115 145	mp1i	$⊢ φ \to ({2^{nd} ↾}_{(\{j\} \times A [\{j\}])}) : \{j\} \times A [\{j\}] \underset{1-1 onto}{⟶} A [\{j\}]$
147	1 2 3 114 122 144 146	gsumf1o	$⊢ φ \to \underset{k \in A [\{j\}]}{\sum_{G}} (j F k) = \sum_{G} ((k \in A [\{j\}] ⟼ j F k) \circ ({2^{nd} ↾}_{(\{j\} \times A [\{j\}])}))$
148		1st2nd2	$⊢ x \in (\{j\} \times A [\{j\}]) \to x = ⟨1^{st} (x), 2^{nd} (x)⟩$
149		xp1st	$⊢ x \in (\{j\} \times A [\{j\}]) \to 1^{st} (x) \in \{j\}$
150		elsni	$⊢ 1^{st} (x) \in \{j\} \to 1^{st} (x) = j$
151	149 150	syl	$⊢ x \in (\{j\} \times A [\{j\}]) \to 1^{st} (x) = j$
152	151	opeq1d	$⊢ x \in (\{j\} \times A [\{j\}]) \to ⟨1^{st} (x), 2^{nd} (x)⟩ = ⟨j, 2^{nd} (x)⟩$
153	148 152	eqtrd	$⊢ x \in (\{j\} \times A [\{j\}]) \to x = ⟨j, 2^{nd} (x)⟩$
154	153	fveq2d	$⊢ x \in (\{j\} \times A [\{j\}]) \to F (x) = F (⟨j, 2^{nd} (x)⟩)$
155		df-ov	$⊢ j F 2^{nd} (x) = F (⟨j, 2^{nd} (x)⟩)$
156	154 155	eqtr4di	$⊢ x \in (\{j\} \times A [\{j\}]) \to F (x) = j F 2^{nd} (x)$
157	156	mpteq2ia	$⊢ (x \in (\{j\} \times A [\{j\}]) ⟼ F (x)) = (x \in (\{j\} \times A [\{j\}]) ⟼ j F 2^{nd} (x))$
158	8	feqmptd	$⊢ φ \to F = (x \in A ⟼ F (x))$
159	158	reseq1d	$⊢ φ \to {F ↾}_{({A ↾}_{\{j\}})} = {(x \in A ⟼ F (x)) ↾}_{({A ↾}_{\{j\}})}$
160		resss	$⊢ {A ↾}_{\{j\}} \subseteq A$
161		resmpt	$⊢ {A ↾}_{\{j\}} \subseteq A \to {(x \in A ⟼ F (x)) ↾}_{({A ↾}_{\{j\}})} = (x \in ({A ↾}_{\{j\}}) ⟼ F (x))$
162	160 161	ax-mp	$⊢ {(x \in A ⟼ F (x)) ↾}_{({A ↾}_{\{j\}})} = (x \in ({A ↾}_{\{j\}}) ⟼ F (x))$
163		ressn	$⊢ {A ↾}_{\{j\}} = \{j\} \times A [\{j\}]$
164	163	mpteq1i	$⊢ (x \in ({A ↾}_{\{j\}}) ⟼ F (x)) = (x \in (\{j\} \times A [\{j\}]) ⟼ F (x))$
165	162 164	eqtri	$⊢ {(x \in A ⟼ F (x)) ↾}_{({A ↾}_{\{j\}})} = (x \in (\{j\} \times A [\{j\}]) ⟼ F (x))$
166	159 165	eqtrdi	$⊢ φ \to {F ↾}_{({A ↾}_{\{j\}})} = (x \in (\{j\} \times A [\{j\}]) ⟼ F (x))$
167		xp2nd	$⊢ x \in (\{j\} \times A [\{j\}]) \to 2^{nd} (x) \in A [\{j\}]$
168	167	adantl	$⊢ (φ \land x \in (\{j\} \times A [\{j\}])) \to 2^{nd} (x) \in A [\{j\}]$
169		fo2nd	$⊢ 2^{nd} : V \underset{onto}{⟶} V$
170		fof	$⊢ 2^{nd} : V \underset{onto}{⟶} V \to 2^{nd} : V ⟶ V$
171	169 170	mp1i	$⊢ φ \to 2^{nd} : V ⟶ V$
172	171	feqmptd	$⊢ φ \to 2^{nd} = (x \in V ⟼ 2^{nd} (x))$
173	172	reseq1d	$⊢ φ \to {2^{nd} ↾}_{(\{j\} \times A [\{j\}])} = {(x \in V ⟼ 2^{nd} (x)) ↾}_{(\{j\} \times A [\{j\}])}$
174		ssv	$⊢ \{j\} \times A [\{j\}] \subseteq V$
175		resmpt	$⊢ \{j\} \times A [\{j\}] \subseteq V \to {(x \in V ⟼ 2^{nd} (x)) ↾}_{(\{j\} \times A [\{j\}])} = (x \in (\{j\} \times A [\{j\}]) ⟼ 2^{nd} (x))$
176	174 175	ax-mp	$⊢ {(x \in V ⟼ 2^{nd} (x)) ↾}_{(\{j\} \times A [\{j\}])} = (x \in (\{j\} \times A [\{j\}]) ⟼ 2^{nd} (x))$
177	173 176	eqtrdi	$⊢ φ \to {2^{nd} ↾}_{(\{j\} \times A [\{j\}])} = (x \in (\{j\} \times A [\{j\}]) ⟼ 2^{nd} (x))$
178		eqidd	$⊢ φ \to (k \in A [\{j\}] ⟼ j F k) = (k \in A [\{j\}] ⟼ j F k)$
179		oveq2	$⊢ k = 2^{nd} (x) \to j F k = j F 2^{nd} (x)$
180	168 177 178 179	fmptco	$⊢ φ \to (k \in A [\{j\}] ⟼ j F k) \circ ({2^{nd} ↾}_{(\{j\} \times A [\{j\}])}) = (x \in (\{j\} \times A [\{j\}]) ⟼ j F 2^{nd} (x))$
181	157 166 180	3eqtr4a	$⊢ φ \to {F ↾}_{({A ↾}_{\{j\}})} = (k \in A [\{j\}] ⟼ j F k) \circ ({2^{nd} ↾}_{(\{j\} \times A [\{j\}])})$
182	181	oveq2d	$⊢ φ \to \sum_{G} ({F ↾}_{({A ↾}_{\{j\}})}) = \sum_{G} ((k \in A [\{j\}] ⟼ j F k) \circ ({2^{nd} ↾}_{(\{j\} \times A [\{j\}])}))$
183	147 182	eqtr4d	$⊢ φ \to \underset{k \in A [\{j\}]}{\sum_{G}} (j F k) = \sum_{G} ({F ↾}_{({A ↾}_{\{j\}})})$
184	112 183	chvarvv	$⊢ φ \to \underset{k \in A [\{z\}]}{\sum_{G}} (z F k) = \sum_{G} ({F ↾}_{({A ↾}_{\{z\}})})$
185	184	adantr	$⊢ (φ \land (y \in Fin \land \neg z \in y)) \to \underset{k \in A [\{z\}]}{\sum_{G}} (z F k) = \sum_{G} ({F ↾}_{({A ↾}_{\{z\}})})$
186	185	oveq2d	$⊢ (φ \land (y \in Fin \land \neg z \in y)) \to (\underset{j \in y}{\sum_{G}}, (\underset{k \in A [\{j\}]}{\sum_{G}}, (j F k))) +_{G} (\underset{k \in A [\{z\}]}{\sum_{G}}, (z F k)) = (\underset{j \in y}{\sum_{G}}, (\underset{k \in A [\{j\}]}{\sum_{G}}, (j F k))) +_{G} (\sum_{G}, ({F ↾}_{({A ↾}_{\{z\}})}))$
187	107 186	eqtrd	$⊢ (φ \land (y \in Fin \land \neg z \in y)) \to \underset{j \in y \cup \{z\}}{\sum_{G}} (\underset{k \in A [\{j\}]}{\sum_{G}}, (j F k)) = (\underset{j \in y}{\sum_{G}}, (\underset{k \in A [\{j\}]}{\sum_{G}}, (j F k))) +_{G} (\sum_{G}, ({F ↾}_{({A ↾}_{\{z\}})}))$
188	92 187	eqeq12d	$⊢ (φ \land (y \in Fin \land \neg z \in y)) \to (\sum_{G} ({F ↾}_{({A ↾}_{(y \cup \{z\})})}) = \underset{j \in y \cup \{z\}}{\sum_{G}} (\underset{k \in A [\{j\}]}{\sum_{G}}, (j F k)) \leftrightarrow (\sum_{G}, ({F ↾}_{({A ↾}_{y})})) +_{G} (\sum_{G}, ({F ↾}_{({A ↾}_{\{z\}})})) = (\underset{j \in y}{\sum_{G}}, (\underset{k \in A [\{j\}]}{\sum_{G}}, (j F k))) +_{G} (\sum_{G}, ({F ↾}_{({A ↾}_{\{z\}})})))$
189	48 188	syl5ibr	$⊢ (φ \land (y \in Fin \land \neg z \in y)) \to (\sum_{G} ({F ↾}_{({A ↾}_{y})}) = \underset{j \in y}{\sum_{G}} (\underset{k \in A [\{j\}]}{\sum_{G}}, (j F k)) \to \sum_{G} ({F ↾}_{({A ↾}_{(y \cup \{z\})})}) = \underset{j \in y \cup \{z\}}{\sum_{G}} (\underset{k \in A [\{j\}]}{\sum_{G}}, (j F k)))$
190	189	expcom	$⊢ (y \in Fin \land \neg z \in y) \to (φ \to (\sum_{G} ({F ↾}_{({A ↾}_{y})}) = \underset{j \in y}{\sum_{G}} (\underset{k \in A [\{j\}]}{\sum_{G}}, (j F k)) \to \sum_{G} ({F ↾}_{({A ↾}_{(y \cup \{z\})})}) = \underset{j \in y \cup \{z\}}{\sum_{G}} (\underset{k \in A [\{j\}]}{\sum_{G}}, (j F k))))$
191	190	a2d	$⊢ (y \in Fin \land \neg z \in y) \to ((φ \to \sum_{G} ({F ↾}_{({A ↾}_{y})}) = \underset{j \in y}{\sum_{G}} (\underset{k \in A [\{j\}]}{\sum_{G}}, (j F k))) \to (φ \to \sum_{G} ({F ↾}_{({A ↾}_{(y \cup \{z\})})}) = \underset{j \in y \cup \{z\}}{\sum_{G}} (\underset{k \in A [\{j\}]}{\sum_{G}}, (j F k))))$
192	25 32 39 46 47 191	findcard2s	$⊢ dom {supp}_{\underset{˙}{0}} (F) \in Fin \to (φ \to \sum_{G} ({F ↾}_{({A ↾}_{dom {supp}_{\underset{˙}{0}} (F)})}) = \underset{j \in dom {supp}_{\underset{˙}{0}} (F)}{\sum_{G}} (\underset{k \in A [\{j\}]}{\sum_{G}}, (j F k)))$
193	12 192	mpcom	$⊢ φ \to \sum_{G} ({F ↾}_{({A ↾}_{dom {supp}_{\underset{˙}{0}} (F)})}) = \underset{j \in dom {supp}_{\underset{˙}{0}} (F)}{\sum_{G}} (\underset{k \in A [\{j\}]}{\sum_{G}}, (j F k))$

Metamath Proof Explorer

Theorem gsum2dlem2

Proof