tsmsf1o

Description: Re-index an infinite group sum using a bijection. (Contributed by Mario Carneiro, 18-Sep-2015)

	Ref	Expression
Hypotheses	tsmsf1o.b	$⊢ B = {Base}_{G}$
	tsmsf1o.1	$⊢ φ \to G \in CMnd$
	tsmsf1o.2	$⊢ φ \to G \in TopSp$
	tsmsf1o.a	$⊢ φ \to A \in V$
	tsmsf1o.f	$⊢ φ \to F : A ⟶ B$
	tsmsf1o.s	$⊢ φ \to H : C \underset{1-1 onto}{⟶} A$
Assertion	tsmsf1o	$⊢ φ \to G tsums F = G tsums (F \circ H)$

Proof

Step	Hyp	Ref	Expression
1		tsmsf1o.b	$⊢ B = {Base}_{G}$
2		tsmsf1o.1	$⊢ φ \to G \in CMnd$
3		tsmsf1o.2	$⊢ φ \to G \in TopSp$
4		tsmsf1o.a	$⊢ φ \to A \in V$
5		tsmsf1o.f	$⊢ φ \to F : A ⟶ B$
6		tsmsf1o.s	$⊢ φ \to H : C \underset{1-1 onto}{⟶} A$
7		f1opwfi	$⊢ H : C \underset{1-1 onto}{⟶} A \to (a \in (𝒫 C \cap Fin) ⟼ H [a]) : 𝒫 C \cap Fin \underset{1-1 onto}{⟶} 𝒫 A \cap Fin$
8	6 7	syl	$⊢ φ \to (a \in (𝒫 C \cap Fin) ⟼ H [a]) : 𝒫 C \cap Fin \underset{1-1 onto}{⟶} 𝒫 A \cap Fin$
9		f1of	$⊢ (a \in (𝒫 C \cap Fin) ⟼ H [a]) : 𝒫 C \cap Fin \underset{1-1 onto}{⟶} 𝒫 A \cap Fin \to (a \in (𝒫 C \cap Fin) ⟼ H [a]) : 𝒫 C \cap Fin ⟶ 𝒫 A \cap Fin$
10	8 9	syl	$⊢ φ \to (a \in (𝒫 C \cap Fin) ⟼ H [a]) : 𝒫 C \cap Fin ⟶ 𝒫 A \cap Fin$
11		eqid	$⊢ (a \in (𝒫 C \cap Fin) ⟼ H [a]) = (a \in (𝒫 C \cap Fin) ⟼ H [a])$
12	11	fmpt	$⊢ \forall a \in (𝒫 C \cap Fin) H [a] \in (𝒫 A \cap Fin) \leftrightarrow (a \in (𝒫 C \cap Fin) ⟼ H [a]) : 𝒫 C \cap Fin ⟶ 𝒫 A \cap Fin$
13	10 12	sylibr	$⊢ φ \to \forall a \in (𝒫 C \cap Fin) H [a] \in (𝒫 A \cap Fin)$
14		sseq1	$⊢ y = H [a] \to (y \subseteq z \leftrightarrow H [a] \subseteq z)$
15	14	imbi1d	$⊢ y = H [a] \to ((y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in u) \leftrightarrow (H [a] \subseteq z \to \sum_{G} ({F ↾}_{z}) \in u))$
16	15	ralbidv	$⊢ y = H [a] \to (\forall z \in (𝒫 A \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in u) \leftrightarrow \forall z \in (𝒫 A \cap Fin) (H [a] \subseteq z \to \sum_{G} ({F ↾}_{z}) \in u))$
17	11 16	rexrnmptw	$⊢ \forall a \in (𝒫 C \cap Fin) H [a] \in (𝒫 A \cap Fin) \to (\exists y \in ran (a \in (𝒫 C \cap Fin) ⟼ H [a]) \forall z \in (𝒫 A \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in u) \leftrightarrow \exists a \in (𝒫 C \cap Fin) \forall z \in (𝒫 A \cap Fin) (H [a] \subseteq z \to \sum_{G} ({F ↾}_{z}) \in u))$
18	13 17	syl	$⊢ φ \to (\exists y \in ran (a \in (𝒫 C \cap Fin) ⟼ H [a]) \forall z \in (𝒫 A \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in u) \leftrightarrow \exists a \in (𝒫 C \cap Fin) \forall z \in (𝒫 A \cap Fin) (H [a] \subseteq z \to \sum_{G} ({F ↾}_{z}) \in u))$
19		f1ofo	$⊢ (a \in (𝒫 C \cap Fin) ⟼ H [a]) : 𝒫 C \cap Fin \underset{1-1 onto}{⟶} 𝒫 A \cap Fin \to (a \in (𝒫 C \cap Fin) ⟼ H [a]) : 𝒫 C \cap Fin \underset{onto}{⟶} 𝒫 A \cap Fin$
20		forn	$⊢ (a \in (𝒫 C \cap Fin) ⟼ H [a]) : 𝒫 C \cap Fin \underset{onto}{⟶} 𝒫 A \cap Fin \to ran (a \in (𝒫 C \cap Fin) ⟼ H [a]) = 𝒫 A \cap Fin$
21	8 19 20	3syl	$⊢ φ \to ran (a \in (𝒫 C \cap Fin) ⟼ H [a]) = 𝒫 A \cap Fin$
22	21	rexeqdv	$⊢ φ \to (\exists y \in ran (a \in (𝒫 C \cap Fin) ⟼ H [a]) \forall z \in (𝒫 A \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \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))$
23		imaeq2	$⊢ a = b \to H [a] = H [b]$
24	23	cbvmptv	$⊢ (a \in (𝒫 C \cap Fin) ⟼ H [a]) = (b \in (𝒫 C \cap Fin) ⟼ H [b])$
25	24	fmpt	$⊢ \forall b \in (𝒫 C \cap Fin) H [b] \in (𝒫 A \cap Fin) \leftrightarrow (a \in (𝒫 C \cap Fin) ⟼ H [a]) : 𝒫 C \cap Fin ⟶ 𝒫 A \cap Fin$
26	10 25	sylibr	$⊢ φ \to \forall b \in (𝒫 C \cap Fin) H [b] \in (𝒫 A \cap Fin)$
27		sseq2	$⊢ z = H [b] \to (H [a] \subseteq z \leftrightarrow H [a] \subseteq H [b])$
28		reseq2	$⊢ z = H [b] \to {F ↾}_{z} = {F ↾}_{H [b]}$
29	28	oveq2d	$⊢ z = H [b] \to \sum_{G} ({F ↾}_{z}) = \sum_{G} ({F ↾}_{H [b]})$
30	29	eleq1d	$⊢ z = H [b] \to (\sum_{G} ({F ↾}_{z}) \in u \leftrightarrow \sum_{G} ({F ↾}_{H [b]}) \in u)$
31	27 30	imbi12d	$⊢ z = H [b] \to ((H [a] \subseteq z \to \sum_{G} ({F ↾}_{z}) \in u) \leftrightarrow (H [a] \subseteq H [b] \to \sum_{G} ({F ↾}_{H [b]}) \in u))$
32	24 31	ralrnmptw	$⊢ \forall b \in (𝒫 C \cap Fin) H [b] \in (𝒫 A \cap Fin) \to (\forall z \in ran (a \in (𝒫 C \cap Fin) ⟼ H [a]) (H [a] \subseteq z \to \sum_{G} ({F ↾}_{z}) \in u) \leftrightarrow \forall b \in (𝒫 C \cap Fin) (H [a] \subseteq H [b] \to \sum_{G} ({F ↾}_{H [b]}) \in u))$
33	26 32	syl	$⊢ φ \to (\forall z \in ran (a \in (𝒫 C \cap Fin) ⟼ H [a]) (H [a] \subseteq z \to \sum_{G} ({F ↾}_{z}) \in u) \leftrightarrow \forall b \in (𝒫 C \cap Fin) (H [a] \subseteq H [b] \to \sum_{G} ({F ↾}_{H [b]}) \in u))$
34	21	raleqdv	$⊢ φ \to (\forall z \in ran (a \in (𝒫 C \cap Fin) ⟼ H [a]) (H [a] \subseteq z \to \sum_{G} ({F ↾}_{z}) \in u) \leftrightarrow \forall z \in (𝒫 A \cap Fin) (H [a] \subseteq z \to \sum_{G} ({F ↾}_{z}) \in u))$
35	33 34	bitr3d	$⊢ φ \to (\forall b \in (𝒫 C \cap Fin) (H [a] \subseteq H [b] \to \sum_{G} ({F ↾}_{H [b]}) \in u) \leftrightarrow \forall z \in (𝒫 A \cap Fin) (H [a] \subseteq z \to \sum_{G} ({F ↾}_{z}) \in u))$
36	35	adantr	$⊢ (φ \land a \in (𝒫 C \cap Fin)) \to (\forall b \in (𝒫 C \cap Fin) (H [a] \subseteq H [b] \to \sum_{G} ({F ↾}_{H [b]}) \in u) \leftrightarrow \forall z \in (𝒫 A \cap Fin) (H [a] \subseteq z \to \sum_{G} ({F ↾}_{z}) \in u))$
37		f1of1	$⊢ H : C \underset{1-1 onto}{⟶} A \to H : C \underset{1-1}{⟶} A$
38	6 37	syl	$⊢ φ \to H : C \underset{1-1}{⟶} A$
39	38	ad2antrr	$⊢ ((φ \land a \in (𝒫 C \cap Fin)) \land b \in (𝒫 C \cap Fin)) \to H : C \underset{1-1}{⟶} A$
40		elfpw	$⊢ a \in (𝒫 C \cap Fin) \leftrightarrow (a \subseteq C \land a \in Fin)$
41	40	simplbi	$⊢ a \in (𝒫 C \cap Fin) \to a \subseteq C$
42	41	ad2antlr	$⊢ ((φ \land a \in (𝒫 C \cap Fin)) \land b \in (𝒫 C \cap Fin)) \to a \subseteq C$
43		elfpw	$⊢ b \in (𝒫 C \cap Fin) \leftrightarrow (b \subseteq C \land b \in Fin)$
44	43	simplbi	$⊢ b \in (𝒫 C \cap Fin) \to b \subseteq C$
45	44	adantl	$⊢ ((φ \land a \in (𝒫 C \cap Fin)) \land b \in (𝒫 C \cap Fin)) \to b \subseteq C$
46		f1imass	$⊢ (H : C \underset{1-1}{⟶} A \land (a \subseteq C \land b \subseteq C)) \to (H [a] \subseteq H [b] \leftrightarrow a \subseteq b)$
47	39 42 45 46	syl12anc	$⊢ ((φ \land a \in (𝒫 C \cap Fin)) \land b \in (𝒫 C \cap Fin)) \to (H [a] \subseteq H [b] \leftrightarrow a \subseteq b)$
48		eqid	$⊢ 0_{G} = 0_{G}$
49	2	ad2antrr	$⊢ ((φ \land a \in (𝒫 C \cap Fin)) \land b \in (𝒫 C \cap Fin)) \to G \in CMnd$
50		elinel2	$⊢ b \in (𝒫 C \cap Fin) \to b \in Fin$
51	50	adantl	$⊢ ((φ \land a \in (𝒫 C \cap Fin)) \land b \in (𝒫 C \cap Fin)) \to b \in Fin$
52		f1ores	$⊢ (H : C \underset{1-1}{⟶} A \land b \subseteq C) \to ({H ↾}_{b}) : b \underset{1-1 onto}{⟶} H [b]$
53	39 45 52	syl2anc	$⊢ ((φ \land a \in (𝒫 C \cap Fin)) \land b \in (𝒫 C \cap Fin)) \to ({H ↾}_{b}) : b \underset{1-1 onto}{⟶} H [b]$
54		f1ofo	$⊢ ({H ↾}_{b}) : b \underset{1-1 onto}{⟶} H [b] \to ({H ↾}_{b}) : b \underset{onto}{⟶} H [b]$
55	53 54	syl	$⊢ ((φ \land a \in (𝒫 C \cap Fin)) \land b \in (𝒫 C \cap Fin)) \to ({H ↾}_{b}) : b \underset{onto}{⟶} H [b]$
56		fofi	$⊢ (b \in Fin \land ({H ↾}_{b}) : b \underset{onto}{⟶} H [b]) \to H [b] \in Fin$
57	51 55 56	syl2anc	$⊢ ((φ \land a \in (𝒫 C \cap Fin)) \land b \in (𝒫 C \cap Fin)) \to H [b] \in Fin$
58	5	ad2antrr	$⊢ ((φ \land a \in (𝒫 C \cap Fin)) \land b \in (𝒫 C \cap Fin)) \to F : A ⟶ B$
59		imassrn	$⊢ H [b] \subseteq ran H$
60	6	ad2antrr	$⊢ ((φ \land a \in (𝒫 C \cap Fin)) \land b \in (𝒫 C \cap Fin)) \to H : C \underset{1-1 onto}{⟶} A$
61		f1ofo	$⊢ H : C \underset{1-1 onto}{⟶} A \to H : C \underset{onto}{⟶} A$
62		forn	$⊢ H : C \underset{onto}{⟶} A \to ran H = A$
63	60 61 62	3syl	$⊢ ((φ \land a \in (𝒫 C \cap Fin)) \land b \in (𝒫 C \cap Fin)) \to ran H = A$
64	59 63	sseqtrid	$⊢ ((φ \land a \in (𝒫 C \cap Fin)) \land b \in (𝒫 C \cap Fin)) \to H [b] \subseteq A$
65	58 64	fssresd	$⊢ ((φ \land a \in (𝒫 C \cap Fin)) \land b \in (𝒫 C \cap Fin)) \to ({F ↾}_{H [b]}) : H [b] ⟶ B$
66		fvexd	$⊢ ((φ \land a \in (𝒫 C \cap Fin)) \land b \in (𝒫 C \cap Fin)) \to 0_{G} \in V$
67	65 57 66	fdmfifsupp	$⊢ ((φ \land a \in (𝒫 C \cap Fin)) \land b \in (𝒫 C \cap Fin)) \to {finSupp}_{0_{G}} (({F ↾}_{H [b]}))$
68	1 48 49 57 65 67 53	gsumf1o	$⊢ ((φ \land a \in (𝒫 C \cap Fin)) \land b \in (𝒫 C \cap Fin)) \to \sum_{G} ({F ↾}_{H [b]}) = \sum_{G} (({F ↾}_{H [b]}) \circ ({H ↾}_{b}))$
69		df-ima	$⊢ H [b] = ran ({H ↾}_{b})$
70	69	eqimss2i	$⊢ ran ({H ↾}_{b}) \subseteq H [b]$
71		cores	$⊢ ran ({H ↾}_{b}) \subseteq H [b] \to ({F ↾}_{H [b]}) \circ ({H ↾}_{b}) = F \circ ({H ↾}_{b})$
72	70 71	ax-mp	$⊢ ({F ↾}_{H [b]}) \circ ({H ↾}_{b}) = F \circ ({H ↾}_{b})$
73		resco	$⊢ {(F \circ H) ↾}_{b} = F \circ ({H ↾}_{b})$
74	72 73	eqtr4i	$⊢ ({F ↾}_{H [b]}) \circ ({H ↾}_{b}) = {(F \circ H) ↾}_{b}$
75	74	oveq2i	$⊢ \sum_{G} (({F ↾}_{H [b]}) \circ ({H ↾}_{b})) = \sum_{G} ({(F \circ H) ↾}_{b})$
76	68 75	eqtrdi	$⊢ ((φ \land a \in (𝒫 C \cap Fin)) \land b \in (𝒫 C \cap Fin)) \to \sum_{G} ({F ↾}_{H [b]}) = \sum_{G} ({(F \circ H) ↾}_{b})$
77	76	eleq1d	$⊢ ((φ \land a \in (𝒫 C \cap Fin)) \land b \in (𝒫 C \cap Fin)) \to (\sum_{G} ({F ↾}_{H [b]}) \in u \leftrightarrow \sum_{G} ({(F \circ H) ↾}_{b}) \in u)$
78	47 77	imbi12d	$⊢ ((φ \land a \in (𝒫 C \cap Fin)) \land b \in (𝒫 C \cap Fin)) \to ((H [a] \subseteq H [b] \to \sum_{G} ({F ↾}_{H [b]}) \in u) \leftrightarrow (a \subseteq b \to \sum_{G} ({(F \circ H) ↾}_{b}) \in u))$
79	78	ralbidva	$⊢ (φ \land a \in (𝒫 C \cap Fin)) \to (\forall b \in (𝒫 C \cap Fin) (H [a] \subseteq H [b] \to \sum_{G} ({F ↾}_{H [b]}) \in u) \leftrightarrow \forall b \in (𝒫 C \cap Fin) (a \subseteq b \to \sum_{G} ({(F \circ H) ↾}_{b}) \in u))$
80	36 79	bitr3d	$⊢ (φ \land a \in (𝒫 C \cap Fin)) \to (\forall z \in (𝒫 A \cap Fin) (H [a] \subseteq z \to \sum_{G} ({F ↾}_{z}) \in u) \leftrightarrow \forall b \in (𝒫 C \cap Fin) (a \subseteq b \to \sum_{G} ({(F \circ H) ↾}_{b}) \in u))$
81	80	rexbidva	$⊢ φ \to (\exists a \in (𝒫 C \cap Fin) \forall z \in (𝒫 A \cap Fin) (H [a] \subseteq z \to \sum_{G} ({F ↾}_{z}) \in u) \leftrightarrow \exists a \in (𝒫 C \cap Fin) \forall b \in (𝒫 C \cap Fin) (a \subseteq b \to \sum_{G} ({(F \circ H) ↾}_{b}) \in u))$
82	18 22 81	3bitr3d	$⊢ φ \to (\exists y \in (𝒫 A \cap Fin) \forall z \in (𝒫 A \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in u) \leftrightarrow \exists a \in (𝒫 C \cap Fin) \forall b \in (𝒫 C \cap Fin) (a \subseteq b \to \sum_{G} ({(F \circ H) ↾}_{b}) \in u))$
83	82	imbi2d	$⊢ φ \to ((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)) \leftrightarrow (x \in u \to \exists a \in (𝒫 C \cap Fin) \forall b \in (𝒫 C \cap Fin) (a \subseteq b \to \sum_{G} ({(F \circ H) ↾}_{b}) \in u)))$
84	83	ralbidv	$⊢ φ \to (\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)) \leftrightarrow \forall u \in TopOpen (G) (x \in u \to \exists a \in (𝒫 C \cap Fin) \forall b \in (𝒫 C \cap Fin) (a \subseteq b \to \sum_{G} ({(F \circ H) ↾}_{b}) \in u)))$
85	84	anbi2d	$⊢ φ \to ((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))) \leftrightarrow (x \in B \land \forall u \in TopOpen (G) (x \in u \to \exists a \in (𝒫 C \cap Fin) \forall b \in (𝒫 C \cap Fin) (a \subseteq b \to \sum_{G} ({(F \circ H) ↾}_{b}) \in u))))$
86		eqid	$⊢ TopOpen (G) = TopOpen (G)$
87		eqid	$⊢ 𝒫 A \cap Fin = 𝒫 A \cap Fin$
88	1 86 87 2 3 4 5	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))))$
89		eqid	$⊢ 𝒫 C \cap Fin = 𝒫 C \cap Fin$
90		f1dmex	$⊢ (H : C \underset{1-1}{⟶} A \land A \in V) \to C \in V$
91	38 4 90	syl2anc	$⊢ φ \to C \in V$
92		f1of	$⊢ H : C \underset{1-1 onto}{⟶} A \to H : C ⟶ A$
93	6 92	syl	$⊢ φ \to H : C ⟶ A$
94		fco	$⊢ (F : A ⟶ B \land H : C ⟶ A) \to (F \circ H) : C ⟶ B$
95	5 93 94	syl2anc	$⊢ φ \to (F \circ H) : C ⟶ B$
96	1 86 89 2 3 91 95	eltsms	$⊢ φ \to (x \in (G tsums (F \circ H)) \leftrightarrow (x \in B \land \forall u \in TopOpen (G) (x \in u \to \exists a \in (𝒫 C \cap Fin) \forall b \in (𝒫 C \cap Fin) (a \subseteq b \to \sum_{G} ({(F \circ H) ↾}_{b}) \in u))))$
97	85 88 96	3bitr4d	$⊢ φ \to (x \in (G tsums F) \leftrightarrow x \in (G tsums (F \circ H)))$
98	97	eqrdv	$⊢ φ \to G tsums F = G tsums (F \circ H)$

Metamath Proof Explorer

Theorem tsmsf1o

Proof