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		resexg	$⊢ A \in V \to {A ↾}_{(y \cup \{z\})} \in V$
52	4 51	syl	$⊢ φ \to {A ↾}_{(y \cup \{z\})} \in V$
53	52	adantr	$⊢ (φ \land (y \in Fin \land \neg z \in y)) \to {A ↾}_{(y \cup \{z\})} \in V$
54		resss	$⊢ {A ↾}_{(y \cup \{z\})} \subseteq A$
55		fssres	$⊢ (F : A ⟶ B \land {A ↾}_{(y \cup \{z\})} \subseteq A) \to ({F ↾}_{({A ↾}_{(y \cup \{z\})})}) : {A ↾}_{(y \cup \{z\})} ⟶ B$
56	8 54 55	sylancl	$⊢ φ \to ({F ↾}_{({A ↾}_{(y \cup \{z\})})}) : {A ↾}_{(y \cup \{z\})} ⟶ B$
57	56	adantr	$⊢ (φ \land (y \in Fin \land \neg z \in y)) \to ({F ↾}_{({A ↾}_{(y \cup \{z\})})}) : {A ↾}_{(y \cup \{z\})} ⟶ B$
58	8	ffund	$⊢ φ \to Fun F$
59		funres	$⊢ Fun F \to Fun ({F ↾}_{({A ↾}_{(y \cup \{z\})})})$
60	58 59	syl	$⊢ φ \to Fun ({F ↾}_{({A ↾}_{(y \cup \{z\})})})$
61	60	adantr	$⊢ (φ \land (y \in Fin \land \neg z \in y)) \to Fun ({F ↾}_{({A ↾}_{(y \cup \{z\})})})$
62	10	adantr	$⊢ (φ \land (y \in Fin \land \neg z \in y)) \to F supp \underset{˙}{0} \in Fin$
63		fex	$⊢ (F : A ⟶ B \land A \in V) \to F \in V$
64	8 4 63	syl2anc	$⊢ φ \to F \in V$
65	2	fvexi	$⊢ \underset{˙}{0} \in V$
66		ressuppss	$⊢ (F \in V \land \underset{˙}{0} \in V) \to ({F ↾}_{({A ↾}_{(y \cup \{z\})})}) supp \underset{˙}{0} \subseteq F supp \underset{˙}{0}$
67	64 65 66	sylancl	$⊢ φ \to ({F ↾}_{({A ↾}_{(y \cup \{z\})})}) supp \underset{˙}{0} \subseteq F supp \underset{˙}{0}$
68	67	adantr	$⊢ (φ \land (y \in Fin \land \neg z \in y)) \to ({F ↾}_{({A ↾}_{(y \cup \{z\})})}) supp \underset{˙}{0} \subseteq F supp \underset{˙}{0}$
69	62 68	ssfid	$⊢ (φ \land (y \in Fin \land \neg z \in y)) \to ({F ↾}_{({A ↾}_{(y \cup \{z\})})}) supp \underset{˙}{0} \in Fin$
70		resexg	$⊢ F \in V \to {F ↾}_{({A ↾}_{(y \cup \{z\})})} \in V$
71	64 70	syl	$⊢ φ \to {F ↾}_{({A ↾}_{(y \cup \{z\})})} \in V$
72		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))$
73	71 65 72	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))$
74	73	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))$
75	61 69 74	mpbir2and	$⊢ (φ \land (y \in Fin \land \neg z \in y)) \to {finSupp}_{\underset{˙}{0}} (({F ↾}_{({A ↾}_{(y \cup \{z\})})}))$
76		simprr	$⊢ (φ \land (y \in Fin \land \neg z \in y)) \to \neg z \in y$
77		disjsn	$⊢ y \cap \{z\} = \emptyset \leftrightarrow \neg z \in y$
78	76 77	sylibr	$⊢ (φ \land (y \in Fin \land \neg z \in y)) \to y \cap \{z\} = \emptyset$
79	78	reseq2d	$⊢ (φ \land (y \in Fin \land \neg z \in y)) \to {A ↾}_{(y \cap \{z\})} = {A ↾}_{\emptyset}$
80		resindi	$⊢ {A ↾}_{(y \cap \{z\})} = ({A ↾}_{y}) \cap ({A ↾}_{\{z\}})$
81	79 80 14	3eqtr3g	$⊢ (φ \land (y \in Fin \land \neg z \in y)) \to ({A ↾}_{y}) \cap ({A ↾}_{\{z\}}) = \emptyset$
82		resundi	$⊢ {A ↾}_{(y \cup \{z\})} = ({A ↾}_{y}) \cup ({A ↾}_{\{z\}})$
83	82	a1i	$⊢ (φ \land (y \in Fin \land \neg z \in y)) \to {A ↾}_{(y \cup \{z\})} = ({A ↾}_{y}) \cup ({A ↾}_{\{z\}})$
84	1 2 49 50 53 57 75 81 83	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\}})}))$
85		ssun1	$⊢ y \subseteq y \cup \{z\}$
86		ssres2	$⊢ y \subseteq y \cup \{z\} \to {A ↾}_{y} \subseteq {A ↾}_{(y \cup \{z\})}$
87		resabs1	$⊢ {A ↾}_{y} \subseteq {A ↾}_{(y \cup \{z\})} \to {({F ↾}_{({A ↾}_{(y \cup \{z\})})}) ↾}_{({A ↾}_{y})} = {F ↾}_{({A ↾}_{y})}$
88	85 86 87	mp2b	$⊢ {({F ↾}_{({A ↾}_{(y \cup \{z\})})}) ↾}_{({A ↾}_{y})} = {F ↾}_{({A ↾}_{y})}$
89	88	oveq2i	$⊢ \sum_{G} ({({F ↾}_{({A ↾}_{(y \cup \{z\})})}) ↾}_{({A ↾}_{y})}) = \sum_{G} ({F ↾}_{({A ↾}_{y})})$
90		ssun2	$⊢ \{z\} \subseteq y \cup \{z\}$
91		ssres2	$⊢ \{z\} \subseteq y \cup \{z\} \to {A ↾}_{\{z\}} \subseteq {A ↾}_{(y \cup \{z\})}$
92		resabs1	$⊢ {A ↾}_{\{z\}} \subseteq {A ↾}_{(y \cup \{z\})} \to {({F ↾}_{({A ↾}_{(y \cup \{z\})})}) ↾}_{({A ↾}_{\{z\}})} = {F ↾}_{({A ↾}_{\{z\}})}$
93	90 91 92	mp2b	$⊢ {({F ↾}_{({A ↾}_{(y \cup \{z\})})}) ↾}_{({A ↾}_{\{z\}})} = {F ↾}_{({A ↾}_{\{z\}})}$
94	93	oveq2i	$⊢ \sum_{G} ({({F ↾}_{({A ↾}_{(y \cup \{z\})})}) ↾}_{({A ↾}_{\{z\}})}) = \sum_{G} ({F ↾}_{({A ↾}_{\{z\}})})$
95	89 94	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\}})}))$
96	84 95	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\}})}))$
97		simprl	$⊢ (φ \land (y \in Fin \land \neg z \in y)) \to y \in Fin$
98	1 2 3 4 5 6 7 8 9	gsum2dlem1	$⊢ φ \to \underset{k \in A [\{j\}]}{\sum_{G}} (j F k) \in B$
99	98	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$
100		vex	$⊢ z \in V$
101	100	a1i	$⊢ (φ \land (y \in Fin \land \neg z \in y)) \to z \in V$
102		sneq	$⊢ j = z \to \{j\} = \{z\}$
103	102	imaeq2d	$⊢ j = z \to A [\{j\}] = A [\{z\}]$
104		oveq1	$⊢ j = z \to j F k = z F k$
105	103 104	mpteq12dv	$⊢ j = z \to (k \in A [\{j\}] ⟼ j F k) = (k \in A [\{z\}] ⟼ z F k)$
106	105	oveq2d	$⊢ j = z \to \underset{k \in A [\{j\}]}{\sum_{G}} (j F k) = \underset{k \in A [\{z\}]}{\sum_{G}} (z F k)$
107	106	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)$
108	107	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))$
109	108 98	chvarvv	$⊢ φ \to \underset{k \in A [\{z\}]}{\sum_{G}} (z F k) \in B$
110	109	adantr	$⊢ (φ \land (y \in Fin \land \neg z \in y)) \to \underset{k \in A [\{z\}]}{\sum_{G}} (z F k) \in B$
111	1 49 50 97 99 101 76 110 106	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))$
112	102	reseq2d	$⊢ j = z \to {A ↾}_{\{j\}} = {A ↾}_{\{z\}}$
113	112	reseq2d	$⊢ j = z \to {F ↾}_{({A ↾}_{\{j\}})} = {F ↾}_{({A ↾}_{\{z\}})}$
114	113	oveq2d	$⊢ j = z \to \sum_{G} ({F ↾}_{({A ↾}_{\{j\}})}) = \sum_{G} ({F ↾}_{({A ↾}_{\{z\}})})$
115	106 114	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\}})}))$
116	115	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\}})})))$
117		imaexg	$⊢ A \in V \to A [\{j\}] \in V$
118	4 117	syl	$⊢ φ \to A [\{j\}] \in V$
119		vex	$⊢ j \in V$
120		vex	$⊢ k \in V$
121	119 120	elimasn	$⊢ k \in A [\{j\}] \leftrightarrow ⟨j, k⟩ \in A$
122		df-ov	$⊢ j F k = F (⟨j, k⟩)$
123	8	ffvelrnda	$⊢ (φ \land ⟨j, k⟩ \in A) \to F (⟨j, k⟩) \in B$
124	122 123	eqeltrid	$⊢ (φ \land ⟨j, k⟩ \in A) \to j F k \in B$
125	121 124	sylan2b	$⊢ (φ \land k \in A [\{j\}]) \to j F k \in B$
126	125	fmpttd	$⊢ φ \to (k \in A [\{j\}] ⟼ j F k) : A [\{j\}] ⟶ B$
127		funmpt	$⊢ Fun (k \in A [\{j\}] ⟼ j F k)$
128	127	a1i	$⊢ φ \to Fun (k \in A [\{j\}] ⟼ j F k)$
129		rnfi	$⊢ F supp \underset{˙}{0} \in Fin \to ran {supp}_{\underset{˙}{0}} (F) \in Fin$
130	10 129	syl	$⊢ φ \to ran {supp}_{\underset{˙}{0}} (F) \in Fin$
131	121	biimpi	$⊢ k \in A [\{j\}] \to ⟨j, k⟩ \in A$
132	119 120	opelrn	$⊢ ⟨j, k⟩ \in {supp}_{\underset{˙}{0}} (F) \to k \in ran {supp}_{\underset{˙}{0}} (F)$
133	132	con3i	$⊢ \neg k \in ran {supp}_{\underset{˙}{0}} (F) \to \neg ⟨j, k⟩ \in {supp}_{\underset{˙}{0}} (F)$
134	131 133	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))$
135		eldif	$⊢ k \in (A [\{j\}] ∖ ran {supp}_{\underset{˙}{0}} (F)) \leftrightarrow (k \in A [\{j\}] \land \neg k \in ran {supp}_{\underset{˙}{0}} (F))$
136		eldif	$⊢ ⟨j, k⟩ \in (A ∖ {supp}_{\underset{˙}{0}} (F)) \leftrightarrow (⟨j, k⟩ \in A \land \neg ⟨j, k⟩ \in {supp}_{\underset{˙}{0}} (F))$
137	134 135 136	3imtr4i	$⊢ k \in (A [\{j\}] ∖ ran {supp}_{\underset{˙}{0}} (F)) \to ⟨j, k⟩ \in (A ∖ {supp}_{\underset{˙}{0}} (F))$
138		ssidd	$⊢ φ \to F supp \underset{˙}{0} \subseteq F supp \underset{˙}{0}$
139	65	a1i	$⊢ φ \to \underset{˙}{0} \in V$
140	8 138 4 139	suppssr	$⊢ (φ \land ⟨j, k⟩ \in (A ∖ {supp}_{\underset{˙}{0}} (F))) \to F (⟨j, k⟩) = \underset{˙}{0}$
141	122 140	syl5eq	$⊢ (φ \land ⟨j, k⟩ \in (A ∖ {supp}_{\underset{˙}{0}} (F))) \to j F k = \underset{˙}{0}$
142	137 141	sylan2	$⊢ (φ \land k \in (A [\{j\}] ∖ ran {supp}_{\underset{˙}{0}} (F))) \to j F k = \underset{˙}{0}$
143	142 118	suppss2	$⊢ φ \to (k \in A [\{j\}] ⟼ j F k) supp \underset{˙}{0} \subseteq ran {supp}_{\underset{˙}{0}} (F)$
144	130 143	ssfid	$⊢ φ \to (k \in A [\{j\}] ⟼ j F k) supp \underset{˙}{0} \in Fin$
145	118	mptexd	$⊢ φ \to (k \in A [\{j\}] ⟼ j F k) \in V$
146		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))$
147	145 65 146	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))$
148	128 144 147	mpbir2and	$⊢ φ \to {finSupp}_{\underset{˙}{0}} ((k \in A [\{j\}] ⟼ j F k))$
149		2ndconst	$⊢ j \in V \to ({2^{nd} ↾}_{(\{j\} \times A [\{j\}])}) : \{j\} \times A [\{j\}] \underset{1-1 onto}{⟶} A [\{j\}]$
150	119 149	mp1i	$⊢ φ \to ({2^{nd} ↾}_{(\{j\} \times A [\{j\}])}) : \{j\} \times A [\{j\}] \underset{1-1 onto}{⟶} A [\{j\}]$
151	1 2 3 118 126 148 150	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\}])}))$
152		1st2nd2	$⊢ x \in (\{j\} \times A [\{j\}]) \to x = ⟨1^{st} (x), 2^{nd} (x)⟩$
153		xp1st	$⊢ x \in (\{j\} \times A [\{j\}]) \to 1^{st} (x) \in \{j\}$
154		elsni	$⊢ 1^{st} (x) \in \{j\} \to 1^{st} (x) = j$
155	153 154	syl	$⊢ x \in (\{j\} \times A [\{j\}]) \to 1^{st} (x) = j$
156	155	opeq1d	$⊢ x \in (\{j\} \times A [\{j\}]) \to ⟨1^{st} (x), 2^{nd} (x)⟩ = ⟨j, 2^{nd} (x)⟩$
157	152 156	eqtrd	$⊢ x \in (\{j\} \times A [\{j\}]) \to x = ⟨j, 2^{nd} (x)⟩$
158	157	fveq2d	$⊢ x \in (\{j\} \times A [\{j\}]) \to F (x) = F (⟨j, 2^{nd} (x)⟩)$
159		df-ov	$⊢ j F 2^{nd} (x) = F (⟨j, 2^{nd} (x)⟩)$
160	158 159	eqtr4di	$⊢ x \in (\{j\} \times A [\{j\}]) \to F (x) = j F 2^{nd} (x)$
161	160	mpteq2ia	$⊢ (x \in (\{j\} \times A [\{j\}]) ⟼ F (x)) = (x \in (\{j\} \times A [\{j\}]) ⟼ j F 2^{nd} (x))$
162	8	feqmptd	$⊢ φ \to F = (x \in A ⟼ F (x))$
163	162	reseq1d	$⊢ φ \to {F ↾}_{({A ↾}_{\{j\}})} = {(x \in A ⟼ F (x)) ↾}_{({A ↾}_{\{j\}})}$
164		resss	$⊢ {A ↾}_{\{j\}} \subseteq A$
165		resmpt	$⊢ {A ↾}_{\{j\}} \subseteq A \to {(x \in A ⟼ F (x)) ↾}_{({A ↾}_{\{j\}})} = (x \in ({A ↾}_{\{j\}}) ⟼ F (x))$
166	164 165	ax-mp	$⊢ {(x \in A ⟼ F (x)) ↾}_{({A ↾}_{\{j\}})} = (x \in ({A ↾}_{\{j\}}) ⟼ F (x))$
167		ressn	$⊢ {A ↾}_{\{j\}} = \{j\} \times A [\{j\}]$
168	167	mpteq1i	$⊢ (x \in ({A ↾}_{\{j\}}) ⟼ F (x)) = (x \in (\{j\} \times A [\{j\}]) ⟼ F (x))$
169	166 168	eqtri	$⊢ {(x \in A ⟼ F (x)) ↾}_{({A ↾}_{\{j\}})} = (x \in (\{j\} \times A [\{j\}]) ⟼ F (x))$
170	163 169	eqtrdi	$⊢ φ \to {F ↾}_{({A ↾}_{\{j\}})} = (x \in (\{j\} \times A [\{j\}]) ⟼ F (x))$
171		xp2nd	$⊢ x \in (\{j\} \times A [\{j\}]) \to 2^{nd} (x) \in A [\{j\}]$
172	171	adantl	$⊢ (φ \land x \in (\{j\} \times A [\{j\}])) \to 2^{nd} (x) \in A [\{j\}]$
173		fo2nd	$⊢ 2^{nd} : V \underset{onto}{⟶} V$
174		fof	$⊢ 2^{nd} : V \underset{onto}{⟶} V \to 2^{nd} : V ⟶ V$
175	173 174	mp1i	$⊢ φ \to 2^{nd} : V ⟶ V$
176	175	feqmptd	$⊢ φ \to 2^{nd} = (x \in V ⟼ 2^{nd} (x))$
177	176	reseq1d	$⊢ φ \to {2^{nd} ↾}_{(\{j\} \times A [\{j\}])} = {(x \in V ⟼ 2^{nd} (x)) ↾}_{(\{j\} \times A [\{j\}])}$
178		ssv	$⊢ \{j\} \times A [\{j\}] \subseteq V$
179		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))$
180	178 179	ax-mp	$⊢ {(x \in V ⟼ 2^{nd} (x)) ↾}_{(\{j\} \times A [\{j\}])} = (x \in (\{j\} \times A [\{j\}]) ⟼ 2^{nd} (x))$
181	177 180	eqtrdi	$⊢ φ \to {2^{nd} ↾}_{(\{j\} \times A [\{j\}])} = (x \in (\{j\} \times A [\{j\}]) ⟼ 2^{nd} (x))$
182		eqidd	$⊢ φ \to (k \in A [\{j\}] ⟼ j F k) = (k \in A [\{j\}] ⟼ j F k)$
183		oveq2	$⊢ k = 2^{nd} (x) \to j F k = j F 2^{nd} (x)$
184	172 181 182 183	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))$
185	161 170 184	3eqtr4a	$⊢ φ \to {F ↾}_{({A ↾}_{\{j\}})} = (k \in A [\{j\}] ⟼ j F k) \circ ({2^{nd} ↾}_{(\{j\} \times A [\{j\}])})$
186	185	oveq2d	$⊢ φ \to \sum_{G} ({F ↾}_{({A ↾}_{\{j\}})}) = \sum_{G} ((k \in A [\{j\}] ⟼ j F k) \circ ({2^{nd} ↾}_{(\{j\} \times A [\{j\}])}))$
187	151 186	eqtr4d	$⊢ φ \to \underset{k \in A [\{j\}]}{\sum_{G}} (j F k) = \sum_{G} ({F ↾}_{({A ↾}_{\{j\}})})$
188	116 187	chvarvv	$⊢ φ \to \underset{k \in A [\{z\}]}{\sum_{G}} (z F k) = \sum_{G} ({F ↾}_{({A ↾}_{\{z\}})})$
189	188	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\}})})$
190	189	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\}})}))$
191	111 190	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\}})}))$
192	96 191	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\}})})))$
193	48 192	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)))$
194	193	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))))$
195	194	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))))$
196	25 32 39 46 47 195	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)))$
197	12 196	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