tsmsres

Description: Extend an infinite group sum by padding outside with zeroes. (Contributed by Mario Carneiro, 18-Sep-2015) (Revised by AV, 25-Jul-2019)

	Ref	Expression
Hypotheses	tsmsres.b	$⊢ B = {Base}_{G}$
	tsmsres.z	$⊢ \underset{˙}{0} = 0_{G}$
	tsmsres.1	$⊢ φ \to G \in CMnd$
	tsmsres.2	$⊢ φ \to G \in TopSp$
	tsmsres.a	$⊢ φ \to A \in V$
	tsmsres.f	$⊢ φ \to F : A ⟶ B$
	tsmsres.s	$⊢ φ \to F supp \underset{˙}{0} \subseteq W$
Assertion	tsmsres	$⊢ φ \to G tsums ({F ↾}_{W}) = G tsums F$

Proof

Step	Hyp	Ref	Expression
1		tsmsres.b	$⊢ B = {Base}_{G}$
2		tsmsres.z	$⊢ \underset{˙}{0} = 0_{G}$
3		tsmsres.1	$⊢ φ \to G \in CMnd$
4		tsmsres.2	$⊢ φ \to G \in TopSp$
5		tsmsres.a	$⊢ φ \to A \in V$
6		tsmsres.f	$⊢ φ \to F : A ⟶ B$
7		tsmsres.s	$⊢ φ \to F supp \underset{˙}{0} \subseteq W$
8		inss1	$⊢ A \cap W \subseteq A$
9	8	sspwi	$⊢ 𝒫 (A \cap W) \subseteq 𝒫 A$
10		ssrin	$⊢ 𝒫 (A \cap W) \subseteq 𝒫 A \to 𝒫 (A \cap W) \cap Fin \subseteq 𝒫 A \cap Fin$
11	9 10	ax-mp	$⊢ 𝒫 (A \cap W) \cap Fin \subseteq 𝒫 A \cap Fin$
12		simpr	$⊢ (φ \land a \in (𝒫 (A \cap W) \cap Fin)) \to a \in (𝒫 (A \cap W) \cap Fin)$
13	11 12	sseldi	$⊢ (φ \land a \in (𝒫 (A \cap W) \cap Fin)) \to a \in (𝒫 A \cap Fin)$
14		elfpw	$⊢ z \in (𝒫 A \cap Fin) \leftrightarrow (z \subseteq A \land z \in Fin)$
15	14	simplbi	$⊢ z \in (𝒫 A \cap Fin) \to z \subseteq A$
16	15	adantl	$⊢ ((φ \land a \in (𝒫 (A \cap W) \cap Fin)) \land z \in (𝒫 A \cap Fin)) \to z \subseteq A$
17	16	ssrind	$⊢ ((φ \land a \in (𝒫 (A \cap W) \cap Fin)) \land z \in (𝒫 A \cap Fin)) \to z \cap W \subseteq A \cap W$
18		elinel2	$⊢ z \in (𝒫 A \cap Fin) \to z \in Fin$
19	18	adantl	$⊢ ((φ \land a \in (𝒫 (A \cap W) \cap Fin)) \land z \in (𝒫 A \cap Fin)) \to z \in Fin$
20		inss1	$⊢ z \cap W \subseteq z$
21		ssfi	$⊢ (z \in Fin \land z \cap W \subseteq z) \to z \cap W \in Fin$
22	19 20 21	sylancl	$⊢ ((φ \land a \in (𝒫 (A \cap W) \cap Fin)) \land z \in (𝒫 A \cap Fin)) \to z \cap W \in Fin$
23		elfpw	$⊢ z \cap W \in (𝒫 (A \cap W) \cap Fin) \leftrightarrow (z \cap W \subseteq A \cap W \land z \cap W \in Fin)$
24	17 22 23	sylanbrc	$⊢ ((φ \land a \in (𝒫 (A \cap W) \cap Fin)) \land z \in (𝒫 A \cap Fin)) \to z \cap W \in (𝒫 (A \cap W) \cap Fin)$
25		sseq2	$⊢ b = z \cap W \to (a \subseteq b \leftrightarrow a \subseteq z \cap W)$
26		ssin	$⊢ (a \subseteq z \land a \subseteq W) \leftrightarrow a \subseteq z \cap W$
27	25 26	syl6bbr	$⊢ b = z \cap W \to (a \subseteq b \leftrightarrow (a \subseteq z \land a \subseteq W))$
28		reseq2	$⊢ b = z \cap W \to {({F ↾}_{W}) ↾}_{b} = {({F ↾}_{W}) ↾}_{(z \cap W)}$
29		inss2	$⊢ z \cap W \subseteq W$
30		resabs1	$⊢ z \cap W \subseteq W \to {({F ↾}_{W}) ↾}_{(z \cap W)} = {F ↾}_{(z \cap W)}$
31	29 30	ax-mp	$⊢ {({F ↾}_{W}) ↾}_{(z \cap W)} = {F ↾}_{(z \cap W)}$
32	28 31	eqtrdi	$⊢ b = z \cap W \to {({F ↾}_{W}) ↾}_{b} = {F ↾}_{(z \cap W)}$
33	32	oveq2d	$⊢ b = z \cap W \to \sum_{G} ({({F ↾}_{W}) ↾}_{b}) = \sum_{G} ({F ↾}_{(z \cap W)})$
34	33	eleq1d	$⊢ b = z \cap W \to (\sum_{G} ({({F ↾}_{W}) ↾}_{b}) \in u \leftrightarrow \sum_{G} ({F ↾}_{(z \cap W)}) \in u)$
35	27 34	imbi12d	$⊢ b = z \cap W \to ((a \subseteq b \to \sum_{G} ({({F ↾}_{W}) ↾}_{b}) \in u) \leftrightarrow ((a \subseteq z \land a \subseteq W) \to \sum_{G} ({F ↾}_{(z \cap W)}) \in u))$
36	35	rspcv	$⊢ z \cap W \in (𝒫 (A \cap W) \cap Fin) \to (\forall b \in (𝒫 (A \cap W) \cap Fin) (a \subseteq b \to \sum_{G} ({({F ↾}_{W}) ↾}_{b}) \in u) \to ((a \subseteq z \land a \subseteq W) \to \sum_{G} ({F ↾}_{(z \cap W)}) \in u))$
37	24 36	syl	$⊢ ((φ \land a \in (𝒫 (A \cap W) \cap Fin)) \land z \in (𝒫 A \cap Fin)) \to (\forall b \in (𝒫 (A \cap W) \cap Fin) (a \subseteq b \to \sum_{G} ({({F ↾}_{W}) ↾}_{b}) \in u) \to ((a \subseteq z \land a \subseteq W) \to \sum_{G} ({F ↾}_{(z \cap W)}) \in u))$
38		elfpw	$⊢ a \in (𝒫 (A \cap W) \cap Fin) \leftrightarrow (a \subseteq A \cap W \land a \in Fin)$
39	38	simplbi	$⊢ a \in (𝒫 (A \cap W) \cap Fin) \to a \subseteq A \cap W$
40	39	ad2antlr	$⊢ ((φ \land a \in (𝒫 (A \cap W) \cap Fin)) \land z \in (𝒫 A \cap Fin)) \to a \subseteq A \cap W$
41		inss2	$⊢ A \cap W \subseteq W$
42	40 41	sstrdi	$⊢ ((φ \land a \in (𝒫 (A \cap W) \cap Fin)) \land z \in (𝒫 A \cap Fin)) \to a \subseteq W$
43	42	biantrud	$⊢ ((φ \land a \in (𝒫 (A \cap W) \cap Fin)) \land z \in (𝒫 A \cap Fin)) \to (a \subseteq z \leftrightarrow (a \subseteq z \land a \subseteq W))$
44		resres	$⊢ {({F ↾}_{z}) ↾}_{W} = {F ↾}_{(z \cap W)}$
45	44	oveq2i	$⊢ \sum_{G} ({({F ↾}_{z}) ↾}_{W}) = \sum_{G} ({F ↾}_{(z \cap W)})$
46	3	ad2antrr	$⊢ ((φ \land a \in (𝒫 (A \cap W) \cap Fin)) \land z \in (𝒫 A \cap Fin)) \to G \in CMnd$
47	6	ad2antrr	$⊢ ((φ \land a \in (𝒫 (A \cap W) \cap Fin)) \land z \in (𝒫 A \cap Fin)) \to F : A ⟶ B$
48	47 16	fssresd	$⊢ ((φ \land a \in (𝒫 (A \cap W) \cap Fin)) \land z \in (𝒫 A \cap Fin)) \to ({F ↾}_{z}) : z ⟶ B$
49		fex	$⊢ (F : A ⟶ B \land A \in V) \to F \in V$
50	6 5 49	syl2anc	$⊢ φ \to F \in V$
51	50	ad2antrr	$⊢ ((φ \land a \in (𝒫 (A \cap W) \cap Fin)) \land z \in (𝒫 A \cap Fin)) \to F \in V$
52	2	fvexi	$⊢ \underset{˙}{0} \in V$
53		ressuppss	$⊢ (F \in V \land \underset{˙}{0} \in V) \to ({F ↾}_{z}) supp \underset{˙}{0} \subseteq F supp \underset{˙}{0}$
54	51 52 53	sylancl	$⊢ ((φ \land a \in (𝒫 (A \cap W) \cap Fin)) \land z \in (𝒫 A \cap Fin)) \to ({F ↾}_{z}) supp \underset{˙}{0} \subseteq F supp \underset{˙}{0}$
55	7	ad2antrr	$⊢ ((φ \land a \in (𝒫 (A \cap W) \cap Fin)) \land z \in (𝒫 A \cap Fin)) \to F supp \underset{˙}{0} \subseteq W$
56	54 55	sstrd	$⊢ ((φ \land a \in (𝒫 (A \cap W) \cap Fin)) \land z \in (𝒫 A \cap Fin)) \to ({F ↾}_{z}) supp \underset{˙}{0} \subseteq W$
57	52	a1i	$⊢ ((φ \land a \in (𝒫 (A \cap W) \cap Fin)) \land z \in (𝒫 A \cap Fin)) \to \underset{˙}{0} \in V$
58	48 19 57	fdmfifsupp	$⊢ ((φ \land a \in (𝒫 (A \cap W) \cap Fin)) \land z \in (𝒫 A \cap Fin)) \to {finSupp}_{\underset{˙}{0}} (({F ↾}_{z}))$
59	1 2 46 19 48 56 58	gsumres	$⊢ ((φ \land a \in (𝒫 (A \cap W) \cap Fin)) \land z \in (𝒫 A \cap Fin)) \to \sum_{G} ({({F ↾}_{z}) ↾}_{W}) = \sum_{G} ({F ↾}_{z})$
60	45 59	syl5reqr	$⊢ ((φ \land a \in (𝒫 (A \cap W) \cap Fin)) \land z \in (𝒫 A \cap Fin)) \to \sum_{G} ({F ↾}_{z}) = \sum_{G} ({F ↾}_{(z \cap W)})$
61	60	eleq1d	$⊢ ((φ \land a \in (𝒫 (A \cap W) \cap Fin)) \land z \in (𝒫 A \cap Fin)) \to (\sum_{G} ({F ↾}_{z}) \in u \leftrightarrow \sum_{G} ({F ↾}_{(z \cap W)}) \in u)$
62	43 61	imbi12d	$⊢ ((φ \land a \in (𝒫 (A \cap W) \cap Fin)) \land z \in (𝒫 A \cap Fin)) \to ((a \subseteq z \to \sum_{G} ({F ↾}_{z}) \in u) \leftrightarrow ((a \subseteq z \land a \subseteq W) \to \sum_{G} ({F ↾}_{(z \cap W)}) \in u))$
63	37 62	sylibrd	$⊢ ((φ \land a \in (𝒫 (A \cap W) \cap Fin)) \land z \in (𝒫 A \cap Fin)) \to (\forall b \in (𝒫 (A \cap W) \cap Fin) (a \subseteq b \to \sum_{G} ({({F ↾}_{W}) ↾}_{b}) \in u) \to (a \subseteq z \to \sum_{G} ({F ↾}_{z}) \in u))$
64	63	ralrimdva	$⊢ (φ \land a \in (𝒫 (A \cap W) \cap Fin)) \to (\forall b \in (𝒫 (A \cap W) \cap Fin) (a \subseteq b \to \sum_{G} ({({F ↾}_{W}) ↾}_{b}) \in u) \to \forall z \in (𝒫 A \cap Fin) (a \subseteq z \to \sum_{G} ({F ↾}_{z}) \in u))$
65		sseq1	$⊢ y = a \to (y \subseteq z \leftrightarrow a \subseteq z)$
66	65	rspceaimv	$⊢ (a \in (𝒫 A \cap Fin) \land \forall z \in (𝒫 A \cap Fin) (a \subseteq z \to \sum_{G} ({F ↾}_{z}) \in u)) \to \exists y \in (𝒫 A \cap Fin) \forall z \in (𝒫 A \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in u)$
67	13 64 66	syl6an	$⊢ (φ \land a \in (𝒫 (A \cap W) \cap Fin)) \to (\forall b \in (𝒫 (A \cap W) \cap Fin) (a \subseteq b \to \sum_{G} ({({F ↾}_{W}) ↾}_{b}) \in u) \to \exists y \in (𝒫 A \cap Fin) \forall z \in (𝒫 A \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in u))$
68	67	rexlimdva	$⊢ φ \to (\exists a \in (𝒫 (A \cap W) \cap Fin) \forall b \in (𝒫 (A \cap W) \cap Fin) (a \subseteq b \to \sum_{G} ({({F ↾}_{W}) ↾}_{b}) \in u) \to \exists y \in (𝒫 A \cap Fin) \forall z \in (𝒫 A \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in u))$
69		elfpw	$⊢ y \in (𝒫 A \cap Fin) \leftrightarrow (y \subseteq A \land y \in Fin)$
70	69	simplbi	$⊢ y \in (𝒫 A \cap Fin) \to y \subseteq A$
71	70	adantl	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to y \subseteq A$
72	71	ssrind	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to y \cap W \subseteq A \cap W$
73		elinel2	$⊢ y \in (𝒫 A \cap Fin) \to y \in Fin$
74	73	adantl	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to y \in Fin$
75		inss1	$⊢ y \cap W \subseteq y$
76		ssfi	$⊢ (y \in Fin \land y \cap W \subseteq y) \to y \cap W \in Fin$
77	74 75 76	sylancl	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to y \cap W \in Fin$
78		elfpw	$⊢ y \cap W \in (𝒫 (A \cap W) \cap Fin) \leftrightarrow (y \cap W \subseteq A \cap W \land y \cap W \in Fin)$
79	72 77 78	sylanbrc	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to y \cap W \in (𝒫 (A \cap W) \cap Fin)$
80	70	ad2antlr	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land b \in (𝒫 (A \cap W) \cap Fin)) \to y \subseteq A$
81		elfpw	$⊢ b \in (𝒫 (A \cap W) \cap Fin) \leftrightarrow (b \subseteq A \cap W \land b \in Fin)$
82	81	simplbi	$⊢ b \in (𝒫 (A \cap W) \cap Fin) \to b \subseteq A \cap W$
83	82	adantl	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land b \in (𝒫 (A \cap W) \cap Fin)) \to b \subseteq A \cap W$
84	83 8	sstrdi	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land b \in (𝒫 (A \cap W) \cap Fin)) \to b \subseteq A$
85	80 84	unssd	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land b \in (𝒫 (A \cap W) \cap Fin)) \to y \cup b \subseteq A$
86		elinel2	$⊢ b \in (𝒫 (A \cap W) \cap Fin) \to b \in Fin$
87		unfi	$⊢ (y \in Fin \land b \in Fin) \to y \cup b \in Fin$
88	74 86 87	syl2an	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land b \in (𝒫 (A \cap W) \cap Fin)) \to y \cup b \in Fin$
89		elfpw	$⊢ y \cup b \in (𝒫 A \cap Fin) \leftrightarrow (y \cup b \subseteq A \land y \cup b \in Fin)$
90	85 88 89	sylanbrc	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land b \in (𝒫 (A \cap W) \cap Fin)) \to y \cup b \in (𝒫 A \cap Fin)$
91		ssun1	$⊢ y \subseteq y \cup b$
92		id	$⊢ z = y \cup b \to z = y \cup b$
93	91 92	sseqtrrid	$⊢ z = y \cup b \to y \subseteq z$
94		pm5.5	$⊢ y \subseteq z \to ((y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in u) \leftrightarrow \sum_{G} ({F ↾}_{z}) \in u)$
95	93 94	syl	$⊢ z = y \cup b \to ((y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in u) \leftrightarrow \sum_{G} ({F ↾}_{z}) \in u)$
96		reseq2	$⊢ z = y \cup b \to {F ↾}_{z} = {F ↾}_{(y \cup b)}$
97	96	oveq2d	$⊢ z = y \cup b \to \sum_{G} ({F ↾}_{z}) = \sum_{G} ({F ↾}_{(y \cup b)})$
98	97	eleq1d	$⊢ z = y \cup b \to (\sum_{G} ({F ↾}_{z}) \in u \leftrightarrow \sum_{G} ({F ↾}_{(y \cup b)}) \in u)$
99	95 98	bitrd	$⊢ z = y \cup b \to ((y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in u) \leftrightarrow \sum_{G} ({F ↾}_{(y \cup b)}) \in u)$
100	99	rspcv	$⊢ y \cup b \in (𝒫 A \cap Fin) \to (\forall z \in (𝒫 A \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in u) \to \sum_{G} ({F ↾}_{(y \cup b)}) \in u)$
101	90 100	syl	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land b \in (𝒫 (A \cap W) \cap Fin)) \to (\forall z \in (𝒫 A \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in u) \to \sum_{G} ({F ↾}_{(y \cup b)}) \in u)$
102	3	ad2antrr	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land (b \in (𝒫 (A \cap W) \cap Fin) \land y \cap W \subseteq b)) \to G \in CMnd$
103	88	adantrr	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land (b \in (𝒫 (A \cap W) \cap Fin) \land y \cap W \subseteq b)) \to y \cup b \in Fin$
104	6	ad2antrr	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land (b \in (𝒫 (A \cap W) \cap Fin) \land y \cap W \subseteq b)) \to F : A ⟶ B$
105	85	adantrr	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land (b \in (𝒫 (A \cap W) \cap Fin) \land y \cap W \subseteq b)) \to y \cup b \subseteq A$
106	104 105	fssresd	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land (b \in (𝒫 (A \cap W) \cap Fin) \land y \cap W \subseteq b)) \to ({F ↾}_{(y \cup b)}) : y \cup b ⟶ B$
107	50 52	jctir	$⊢ φ \to (F \in V \land \underset{˙}{0} \in V)$
108	107	ad2antrr	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land (b \in (𝒫 (A \cap W) \cap Fin) \land y \cap W \subseteq b)) \to (F \in V \land \underset{˙}{0} \in V)$
109		ressuppss	$⊢ (F \in V \land \underset{˙}{0} \in V) \to ({F ↾}_{(y \cup b)}) supp \underset{˙}{0} \subseteq F supp \underset{˙}{0}$
110	108 109	syl	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land (b \in (𝒫 (A \cap W) \cap Fin) \land y \cap W \subseteq b)) \to ({F ↾}_{(y \cup b)}) supp \underset{˙}{0} \subseteq F supp \underset{˙}{0}$
111	7	ad2antrr	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land (b \in (𝒫 (A \cap W) \cap Fin) \land y \cap W \subseteq b)) \to F supp \underset{˙}{0} \subseteq W$
112	110 111	sstrd	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land (b \in (𝒫 (A \cap W) \cap Fin) \land y \cap W \subseteq b)) \to ({F ↾}_{(y \cup b)}) supp \underset{˙}{0} \subseteq W$
113	52	a1i	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land (b \in (𝒫 (A \cap W) \cap Fin) \land y \cap W \subseteq b)) \to \underset{˙}{0} \in V$
114	106 103 113	fdmfifsupp	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land (b \in (𝒫 (A \cap W) \cap Fin) \land y \cap W \subseteq b)) \to {finSupp}_{\underset{˙}{0}} (({F ↾}_{(y \cup b)}))$
115	1 2 102 103 106 112 114	gsumres	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land (b \in (𝒫 (A \cap W) \cap Fin) \land y \cap W \subseteq b)) \to \sum_{G} ({({F ↾}_{(y \cup b)}) ↾}_{W}) = \sum_{G} ({F ↾}_{(y \cup b)})$
116		resres	$⊢ {({F ↾}_{(y \cup b)}) ↾}_{W} = {F ↾}_{((y \cup b) \cap W)}$
117		indir	$⊢ (y \cup b) \cap W = (y \cap W) \cup (b \cap W)$
118	83 41	sstrdi	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land b \in (𝒫 (A \cap W) \cap Fin)) \to b \subseteq W$
119	118	adantrr	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land (b \in (𝒫 (A \cap W) \cap Fin) \land y \cap W \subseteq b)) \to b \subseteq W$
120		df-ss	$⊢ b \subseteq W \leftrightarrow b \cap W = b$
121	119 120	sylib	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land (b \in (𝒫 (A \cap W) \cap Fin) \land y \cap W \subseteq b)) \to b \cap W = b$
122	121	uneq2d	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land (b \in (𝒫 (A \cap W) \cap Fin) \land y \cap W \subseteq b)) \to (y \cap W) \cup (b \cap W) = (y \cap W) \cup b$
123		simprr	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land (b \in (𝒫 (A \cap W) \cap Fin) \land y \cap W \subseteq b)) \to y \cap W \subseteq b$
124		ssequn1	$⊢ y \cap W \subseteq b \leftrightarrow (y \cap W) \cup b = b$
125	123 124	sylib	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land (b \in (𝒫 (A \cap W) \cap Fin) \land y \cap W \subseteq b)) \to (y \cap W) \cup b = b$
126	122 125	eqtrd	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land (b \in (𝒫 (A \cap W) \cap Fin) \land y \cap W \subseteq b)) \to (y \cap W) \cup (b \cap W) = b$
127	117 126	syl5eq	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land (b \in (𝒫 (A \cap W) \cap Fin) \land y \cap W \subseteq b)) \to (y \cup b) \cap W = b$
128	127	reseq2d	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land (b \in (𝒫 (A \cap W) \cap Fin) \land y \cap W \subseteq b)) \to {F ↾}_{((y \cup b) \cap W)} = {F ↾}_{b}$
129	116 128	syl5eq	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land (b \in (𝒫 (A \cap W) \cap Fin) \land y \cap W \subseteq b)) \to {({F ↾}_{(y \cup b)}) ↾}_{W} = {F ↾}_{b}$
130	119	resabs1d	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land (b \in (𝒫 (A \cap W) \cap Fin) \land y \cap W \subseteq b)) \to {({F ↾}_{W}) ↾}_{b} = {F ↾}_{b}$
131	129 130	eqtr4d	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land (b \in (𝒫 (A \cap W) \cap Fin) \land y \cap W \subseteq b)) \to {({F ↾}_{(y \cup b)}) ↾}_{W} = {({F ↾}_{W}) ↾}_{b}$
132	131	oveq2d	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land (b \in (𝒫 (A \cap W) \cap Fin) \land y \cap W \subseteq b)) \to \sum_{G} ({({F ↾}_{(y \cup b)}) ↾}_{W}) = \sum_{G} ({({F ↾}_{W}) ↾}_{b})$
133	115 132	eqtr3d	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land (b \in (𝒫 (A \cap W) \cap Fin) \land y \cap W \subseteq b)) \to \sum_{G} ({F ↾}_{(y \cup b)}) = \sum_{G} ({({F ↾}_{W}) ↾}_{b})$
134	133	eleq1d	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land (b \in (𝒫 (A \cap W) \cap Fin) \land y \cap W \subseteq b)) \to (\sum_{G} ({F ↾}_{(y \cup b)}) \in u \leftrightarrow \sum_{G} ({({F ↾}_{W}) ↾}_{b}) \in u)$
135	134	biimpd	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land (b \in (𝒫 (A \cap W) \cap Fin) \land y \cap W \subseteq b)) \to (\sum_{G} ({F ↾}_{(y \cup b)}) \in u \to \sum_{G} ({({F ↾}_{W}) ↾}_{b}) \in u)$
136	135	expr	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land b \in (𝒫 (A \cap W) \cap Fin)) \to (y \cap W \subseteq b \to (\sum_{G} ({F ↾}_{(y \cup b)}) \in u \to \sum_{G} ({({F ↾}_{W}) ↾}_{b}) \in u))$
137	136	com23	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land b \in (𝒫 (A \cap W) \cap Fin)) \to (\sum_{G} ({F ↾}_{(y \cup b)}) \in u \to (y \cap W \subseteq b \to \sum_{G} ({({F ↾}_{W}) ↾}_{b}) \in u))$
138	101 137	syld	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land b \in (𝒫 (A \cap W) \cap Fin)) \to (\forall z \in (𝒫 A \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in u) \to (y \cap W \subseteq b \to \sum_{G} ({({F ↾}_{W}) ↾}_{b}) \in u))$
139	138	ralrimdva	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to (\forall z \in (𝒫 A \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in u) \to \forall b \in (𝒫 (A \cap W) \cap Fin) (y \cap W \subseteq b \to \sum_{G} ({({F ↾}_{W}) ↾}_{b}) \in u))$
140		sseq1	$⊢ a = y \cap W \to (a \subseteq b \leftrightarrow y \cap W \subseteq b)$
141	140	rspceaimv	$⊢ (y \cap W \in (𝒫 (A \cap W) \cap Fin) \land \forall b \in (𝒫 (A \cap W) \cap Fin) (y \cap W \subseteq b \to \sum_{G} ({({F ↾}_{W}) ↾}_{b}) \in u)) \to \exists a \in (𝒫 (A \cap W) \cap Fin) \forall b \in (𝒫 (A \cap W) \cap Fin) (a \subseteq b \to \sum_{G} ({({F ↾}_{W}) ↾}_{b}) \in u)$
142	79 139 141	syl6an	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to (\forall z \in (𝒫 A \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in u) \to \exists a \in (𝒫 (A \cap W) \cap Fin) \forall b \in (𝒫 (A \cap W) \cap Fin) (a \subseteq b \to \sum_{G} ({({F ↾}_{W}) ↾}_{b}) \in u))$
143	142	rexlimdva	$⊢ φ \to (\exists y \in (𝒫 A \cap Fin) \forall z \in (𝒫 A \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in u) \to \exists a \in (𝒫 (A \cap W) \cap Fin) \forall b \in (𝒫 (A \cap W) \cap Fin) (a \subseteq b \to \sum_{G} ({({F ↾}_{W}) ↾}_{b}) \in u))$
144	68 143	impbid	$⊢ φ \to (\exists a \in (𝒫 (A \cap W) \cap Fin) \forall b \in (𝒫 (A \cap W) \cap Fin) (a \subseteq b \to \sum_{G} ({({F ↾}_{W}) ↾}_{b}) \in u) \leftrightarrow \exists y \in (𝒫 A \cap Fin) \forall z \in (𝒫 A \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in u))$
145	144	imbi2d	$⊢ φ \to ((x \in u \to \exists a \in (𝒫 (A \cap W) \cap Fin) \forall b \in (𝒫 (A \cap W) \cap Fin) (a \subseteq b \to \sum_{G} ({({F ↾}_{W}) ↾}_{b}) \in u)) \leftrightarrow (x \in u \to \exists y \in (𝒫 A \cap Fin) \forall z \in (𝒫 A \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in u)))$
146	145	ralbidv	$⊢ φ \to (\forall u \in TopOpen (G) (x \in u \to \exists a \in (𝒫 (A \cap W) \cap Fin) \forall b \in (𝒫 (A \cap W) \cap Fin) (a \subseteq b \to \sum_{G} ({({F ↾}_{W}) ↾}_{b}) \in u)) \leftrightarrow \forall u \in TopOpen (G) (x \in u \to \exists y \in (𝒫 A \cap Fin) \forall z \in (𝒫 A \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in u)))$
147	146	anbi2d	$⊢ φ \to ((x \in B \land \forall u \in TopOpen (G) (x \in u \to \exists a \in (𝒫 (A \cap W) \cap Fin) \forall b \in (𝒫 (A \cap W) \cap Fin) (a \subseteq b \to \sum_{G} ({({F ↾}_{W}) ↾}_{b}) \in u))) \leftrightarrow (x \in B \land \forall u \in TopOpen (G) (x \in u \to \exists y \in (𝒫 A \cap Fin) \forall z \in (𝒫 A \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in u))))$
148		eqid	$⊢ TopOpen (G) = TopOpen (G)$
149		eqid	$⊢ 𝒫 (A \cap W) \cap Fin = 𝒫 (A \cap W) \cap Fin$
150		inex1g	$⊢ A \in V \to A \cap W \in V$
151	5 150	syl	$⊢ φ \to A \cap W \in V$
152		fssres	$⊢ (F : A ⟶ B \land A \cap W \subseteq A) \to ({F ↾}_{(A \cap W)}) : A \cap W ⟶ B$
153	6 8 152	sylancl	$⊢ φ \to ({F ↾}_{(A \cap W)}) : A \cap W ⟶ B$
154		resres	$⊢ {({F ↾}_{A}) ↾}_{W} = {F ↾}_{(A \cap W)}$
155		ffn	$⊢ F : A ⟶ B \to F Fn A$
156		fnresdm	$⊢ F Fn A \to {F ↾}_{A} = F$
157	6 155 156	3syl	$⊢ φ \to {F ↾}_{A} = F$
158	157	reseq1d	$⊢ φ \to {({F ↾}_{A}) ↾}_{W} = {F ↾}_{W}$
159	154 158	syl5eqr	$⊢ φ \to {F ↾}_{(A \cap W)} = {F ↾}_{W}$
160	159	feq1d	$⊢ φ \to (({F ↾}_{(A \cap W)}) : A \cap W ⟶ B \leftrightarrow ({F ↾}_{W}) : A \cap W ⟶ B)$
161	153 160	mpbid	$⊢ φ \to ({F ↾}_{W}) : A \cap W ⟶ B$
162	1 148 149 3 4 151 161	eltsms	$⊢ φ \to (x \in (G tsums ({F ↾}_{W})) \leftrightarrow (x \in B \land \forall u \in TopOpen (G) (x \in u \to \exists a \in (𝒫 (A \cap W) \cap Fin) \forall b \in (𝒫 (A \cap W) \cap Fin) (a \subseteq b \to \sum_{G} ({({F ↾}_{W}) ↾}_{b}) \in u))))$
163		eqid	$⊢ 𝒫 A \cap Fin = 𝒫 A \cap Fin$
164	1 148 163 3 4 5 6	eltsms	$⊢ φ \to (x \in (G tsums F) \leftrightarrow (x \in B \land \forall u \in TopOpen (G) (x \in u \to \exists y \in (𝒫 A \cap Fin) \forall z \in (𝒫 A \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in u))))$
165	147 162 164	3bitr4d	$⊢ φ \to (x \in (G tsums ({F ↾}_{W})) \leftrightarrow x \in (G tsums F))$
166	165	eqrdv	$⊢ φ \to G tsums ({F ↾}_{W}) = G tsums F$

Metamath Proof Explorer

Theorem tsmsres

Proof