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	bitr4di	$⊢ 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	3	ad2antrr	$⊢ ((φ \land a \in (𝒫 (A \cap W) \cap Fin)) \land z \in (𝒫 A \cap Fin)) \to G \in CMnd$
45	6	ad2antrr	$⊢ ((φ \land a \in (𝒫 (A \cap W) \cap Fin)) \land z \in (𝒫 A \cap Fin)) \to F : A ⟶ B$
46	45 16	fssresd	$⊢ ((φ \land a \in (𝒫 (A \cap W) \cap Fin)) \land z \in (𝒫 A \cap Fin)) \to ({F ↾}_{z}) : z ⟶ B$
47	6 5	fexd	$⊢ φ \to F \in V$
48	47	ad2antrr	$⊢ ((φ \land a \in (𝒫 (A \cap W) \cap Fin)) \land z \in (𝒫 A \cap Fin)) \to F \in V$
49	2	fvexi	$⊢ \underset{˙}{0} \in V$
50		ressuppss	$⊢ (F \in V \land \underset{˙}{0} \in V) \to ({F ↾}_{z}) supp \underset{˙}{0} \subseteq F supp \underset{˙}{0}$
51	48 49 50	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}$
52	7	ad2antrr	$⊢ ((φ \land a \in (𝒫 (A \cap W) \cap Fin)) \land z \in (𝒫 A \cap Fin)) \to F supp \underset{˙}{0} \subseteq W$
53	51 52	sstrd	$⊢ ((φ \land a \in (𝒫 (A \cap W) \cap Fin)) \land z \in (𝒫 A \cap Fin)) \to ({F ↾}_{z}) supp \underset{˙}{0} \subseteq W$
54	49	a1i	$⊢ ((φ \land a \in (𝒫 (A \cap W) \cap Fin)) \land z \in (𝒫 A \cap Fin)) \to \underset{˙}{0} \in V$
55	46 19 54	fdmfifsupp	$⊢ ((φ \land a \in (𝒫 (A \cap W) \cap Fin)) \land z \in (𝒫 A \cap Fin)) \to {finSupp}_{\underset{˙}{0}} (({F ↾}_{z}))$
56	1 2 44 19 46 53 55	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})$
57		resres	$⊢ {({F ↾}_{z}) ↾}_{W} = {F ↾}_{(z \cap W)}$
58	57	oveq2i	$⊢ \sum_{G} ({({F ↾}_{z}) ↾}_{W}) = \sum_{G} ({F ↾}_{(z \cap W)})$
59	56 58	eqtr3di	$⊢ ((φ \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)})$
60	59	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)$
61	43 60	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))$
62	37 61	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))$
63	62	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))$
64		sseq1	$⊢ y = a \to (y \subseteq z \leftrightarrow a \subseteq z)$
65	64	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)$
66	13 63 65	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))$
67	66	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))$
68		elfpw	$⊢ y \in (𝒫 A \cap Fin) \leftrightarrow (y \subseteq A \land y \in Fin)$
69	68	simplbi	$⊢ y \in (𝒫 A \cap Fin) \to y \subseteq A$
70	69	adantl	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to y \subseteq A$
71	70	ssrind	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to y \cap W \subseteq A \cap W$
72		elinel2	$⊢ y \in (𝒫 A \cap Fin) \to y \in Fin$
73	72	adantl	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to y \in Fin$
74		inss1	$⊢ y \cap W \subseteq y$
75		ssfi	$⊢ (y \in Fin \land y \cap W \subseteq y) \to y \cap W \in Fin$
76	73 74 75	sylancl	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to y \cap W \in Fin$
77		elfpw	$⊢ y \cap W \in (𝒫 (A \cap W) \cap Fin) \leftrightarrow (y \cap W \subseteq A \cap W \land y \cap W \in Fin)$
78	71 76 77	sylanbrc	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to y \cap W \in (𝒫 (A \cap W) \cap Fin)$
79	69	ad2antlr	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land b \in (𝒫 (A \cap W) \cap Fin)) \to y \subseteq A$
80		elfpw	$⊢ b \in (𝒫 (A \cap W) \cap Fin) \leftrightarrow (b \subseteq A \cap W \land b \in Fin)$
81	80	simplbi	$⊢ b \in (𝒫 (A \cap W) \cap Fin) \to b \subseteq A \cap W$
82	81	adantl	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land b \in (𝒫 (A \cap W) \cap Fin)) \to b \subseteq A \cap W$
83	82 8	sstrdi	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land b \in (𝒫 (A \cap W) \cap Fin)) \to b \subseteq A$
84	79 83	unssd	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land b \in (𝒫 (A \cap W) \cap Fin)) \to y \cup b \subseteq A$
85		elinel2	$⊢ b \in (𝒫 (A \cap W) \cap Fin) \to b \in Fin$
86		unfi	$⊢ (y \in Fin \land b \in Fin) \to y \cup b \in Fin$
87	73 85 86	syl2an	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land b \in (𝒫 (A \cap W) \cap Fin)) \to y \cup b \in Fin$
88		elfpw	$⊢ y \cup b \in (𝒫 A \cap Fin) \leftrightarrow (y \cup b \subseteq A \land y \cup b \in Fin)$
89	84 87 88	sylanbrc	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land b \in (𝒫 (A \cap W) \cap Fin)) \to y \cup b \in (𝒫 A \cap Fin)$
90		ssun1	$⊢ y \subseteq y \cup b$
91		id	$⊢ z = y \cup b \to z = y \cup b$
92	90 91	sseqtrrid	$⊢ z = y \cup b \to y \subseteq z$
93		pm5.5	$⊢ y \subseteq z \to ((y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in u) \leftrightarrow \sum_{G} ({F ↾}_{z}) \in u)$
94	92 93	syl	$⊢ z = y \cup b \to ((y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in u) \leftrightarrow \sum_{G} ({F ↾}_{z}) \in u)$
95		reseq2	$⊢ z = y \cup b \to {F ↾}_{z} = {F ↾}_{(y \cup b)}$
96	95	oveq2d	$⊢ z = y \cup b \to \sum_{G} ({F ↾}_{z}) = \sum_{G} ({F ↾}_{(y \cup b)})$
97	96	eleq1d	$⊢ z = y \cup b \to (\sum_{G} ({F ↾}_{z}) \in u \leftrightarrow \sum_{G} ({F ↾}_{(y \cup b)}) \in u)$
98	94 97	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)$
99	98	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)$
100	89 99	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)$
101	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$
102	87	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$
103	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$
104	84	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$
105	103 104	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$
106	47 49	jctir	$⊢ φ \to (F \in V \land \underset{˙}{0} \in V)$
107	106	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)$
108		ressuppss	$⊢ (F \in V \land \underset{˙}{0} \in V) \to ({F ↾}_{(y \cup b)}) supp \underset{˙}{0} \subseteq F supp \underset{˙}{0}$
109	107 108	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}$
110	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$
111	109 110	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$
112	49	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$
113	105 102 112	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)}))$
114	1 2 101 102 105 111 113	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)})$
115		resres	$⊢ {({F ↾}_{(y \cup b)}) ↾}_{W} = {F ↾}_{((y \cup b) \cap W)}$
116		indir	$⊢ (y \cup b) \cap W = (y \cap W) \cup (b \cap W)$
117	82 41	sstrdi	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land b \in (𝒫 (A \cap W) \cap Fin)) \to b \subseteq W$
118	117	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$
119		df-ss	$⊢ b \subseteq W \leftrightarrow b \cap W = b$
120	118 119	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$
121	120	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$
122		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$
123		ssequn1	$⊢ y \cap W \subseteq b \leftrightarrow (y \cap W) \cup b = b$
124	122 123	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$
125	121 124	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$
126	116 125	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$
127	126	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}$
128	115 127	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}$
129	118	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}$
130	128 129	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}$
131	130	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})$
132	114 131	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})$
133	132	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)$
134	133	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)$
135	134	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))$
136	135	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))$
137	100 136	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))$
138	137	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))$
139		sseq1	$⊢ a = y \cap W \to (a \subseteq b \leftrightarrow y \cap W \subseteq b)$
140	139	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)$
141	78 138 140	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))$
142	141	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))$
143	67 142	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))$
144	143	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)))$
145	144	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)))$
146	145	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))))$
147		eqid	$⊢ TopOpen (G) = TopOpen (G)$
148		eqid	$⊢ 𝒫 (A \cap W) \cap Fin = 𝒫 (A \cap W) \cap Fin$
149		inex1g	$⊢ A \in V \to A \cap W \in V$
150	5 149	syl	$⊢ φ \to A \cap W \in V$
151		fssres	$⊢ (F : A ⟶ B \land A \cap W \subseteq A) \to ({F ↾}_{(A \cap W)}) : A \cap W ⟶ B$
152	6 8 151	sylancl	$⊢ φ \to ({F ↾}_{(A \cap W)}) : A \cap W ⟶ B$
153		resres	$⊢ {({F ↾}_{A}) ↾}_{W} = {F ↾}_{(A \cap W)}$
154		ffn	$⊢ F : A ⟶ B \to F Fn A$
155		fnresdm	$⊢ F Fn A \to {F ↾}_{A} = F$
156	6 154 155	3syl	$⊢ φ \to {F ↾}_{A} = F$
157	156	reseq1d	$⊢ φ \to {({F ↾}_{A}) ↾}_{W} = {F ↾}_{W}$
158	153 157	eqtr3id	$⊢ φ \to {F ↾}_{(A \cap W)} = {F ↾}_{W}$
159	158	feq1d	$⊢ φ \to (({F ↾}_{(A \cap W)}) : A \cap W ⟶ B \leftrightarrow ({F ↾}_{W}) : A \cap W ⟶ B)$
160	152 159	mpbid	$⊢ φ \to ({F ↾}_{W}) : A \cap W ⟶ B$
161	1 147 148 3 4 150 160	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))))$
162		eqid	$⊢ 𝒫 A \cap Fin = 𝒫 A \cap Fin$
163	1 147 162 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))))$
164	146 161 163	3bitr4d	$⊢ φ \to (x \in (G tsums ({F ↾}_{W})) \leftrightarrow x \in (G tsums F))$
165	164	eqrdv	$⊢ φ \to G tsums ({F ↾}_{W}) = G tsums F$

Metamath Proof Explorer

Theorem tsmsres

Proof