tsmsgsum

Description: The convergent points of a finite topological group sum are the closure of the finite group sum operation. (Contributed by Mario Carneiro, 19-Sep-2015) (Revised by AV, 24-Jul-2019)

	Ref	Expression
Hypotheses	tsmsid.b	$⊢ B = {Base}_{G}$
	tsmsid.z	$⊢ \underset{˙}{0} = 0_{G}$
	tsmsid.1	$⊢ φ \to G \in CMnd$
	tsmsid.2	$⊢ φ \to G \in TopSp$
	tsmsid.a	$⊢ φ \to A \in V$
	tsmsid.f	$⊢ φ \to F : A ⟶ B$
	tsmsid.w	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (F)$
	tsmsgsum.j	$⊢ J = TopOpen (G)$
Assertion	tsmsgsum	$⊢ φ \to G tsums F = cls (J) (\{\sum_{G} F\})$

Proof

Step	Hyp	Ref	Expression
1		tsmsid.b	$⊢ B = {Base}_{G}$
2		tsmsid.z	$⊢ \underset{˙}{0} = 0_{G}$
3		tsmsid.1	$⊢ φ \to G \in CMnd$
4		tsmsid.2	$⊢ φ \to G \in TopSp$
5		tsmsid.a	$⊢ φ \to A \in V$
6		tsmsid.f	$⊢ φ \to F : A ⟶ B$
7		tsmsid.w	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (F)$
8		tsmsgsum.j	$⊢ J = TopOpen (G)$
9	1 8	istps	$⊢ G \in TopSp \leftrightarrow J \in TopOn (B)$
10	4 9	sylib	$⊢ φ \to J \in TopOn (B)$
11		toponuni	$⊢ J \in TopOn (B) \to B = ⋃ J$
12	10 11	syl	$⊢ φ \to B = ⋃ J$
13	12	eleq2d	$⊢ φ \to (x \in B \leftrightarrow x \in ⋃ J)$
14		elfpw	$⊢ y \in (𝒫 A \cap Fin) \leftrightarrow (y \subseteq A \land y \in Fin)$
15	14	simplbi	$⊢ y \in (𝒫 A \cap Fin) \to y \subseteq A$
16	15	adantl	$⊢ ((φ \land u \in J) \land y \in (𝒫 A \cap Fin)) \to y \subseteq A$
17		suppssdm	$⊢ F supp \underset{˙}{0} \subseteq dom F$
18	17 6	fssdm	$⊢ φ \to F supp \underset{˙}{0} \subseteq A$
19	18	ad2antrr	$⊢ ((φ \land u \in J) \land y \in (𝒫 A \cap Fin)) \to F supp \underset{˙}{0} \subseteq A$
20	16 19	unssd	$⊢ ((φ \land u \in J) \land y \in (𝒫 A \cap Fin)) \to y \cup {supp}_{\underset{˙}{0}} (F) \subseteq A$
21		elinel2	$⊢ y \in (𝒫 A \cap Fin) \to y \in Fin$
22	21	adantl	$⊢ ((φ \land u \in J) \land y \in (𝒫 A \cap Fin)) \to y \in Fin$
23	7	ad2antrr	$⊢ ((φ \land u \in J) \land y \in (𝒫 A \cap Fin)) \to {finSupp}_{\underset{˙}{0}} (F)$
24	23	fsuppimpd	$⊢ ((φ \land u \in J) \land y \in (𝒫 A \cap Fin)) \to F supp \underset{˙}{0} \in Fin$
25		unfi	$⊢ (y \in Fin \land F supp \underset{˙}{0} \in Fin) \to y \cup {supp}_{\underset{˙}{0}} (F) \in Fin$
26	22 24 25	syl2anc	$⊢ ((φ \land u \in J) \land y \in (𝒫 A \cap Fin)) \to y \cup {supp}_{\underset{˙}{0}} (F) \in Fin$
27		elfpw	$⊢ y \cup {supp}_{\underset{˙}{0}} (F) \in (𝒫 A \cap Fin) \leftrightarrow (y \cup {supp}_{\underset{˙}{0}} (F) \subseteq A \land y \cup {supp}_{\underset{˙}{0}} (F) \in Fin)$
28	20 26 27	sylanbrc	$⊢ ((φ \land u \in J) \land y \in (𝒫 A \cap Fin)) \to y \cup {supp}_{\underset{˙}{0}} (F) \in (𝒫 A \cap Fin)$
29		ssun1	$⊢ y \subseteq y \cup {supp}_{\underset{˙}{0}} (F)$
30		id	$⊢ z = y \cup {supp}_{\underset{˙}{0}} (F) \to z = y \cup {supp}_{\underset{˙}{0}} (F)$
31	29 30	sseqtrrid	$⊢ z = y \cup {supp}_{\underset{˙}{0}} (F) \to y \subseteq z$
32		pm5.5	$⊢ y \subseteq z \to ((y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in u) \leftrightarrow \sum_{G} ({F ↾}_{z}) \in u)$
33	31 32	syl	$⊢ z = y \cup {supp}_{\underset{˙}{0}} (F) \to ((y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in u) \leftrightarrow \sum_{G} ({F ↾}_{z}) \in u)$
34		reseq2	$⊢ z = y \cup {supp}_{\underset{˙}{0}} (F) \to {F ↾}_{z} = {F ↾}_{(y \cup {supp}_{\underset{˙}{0}} (F))}$
35	34	oveq2d	$⊢ z = y \cup {supp}_{\underset{˙}{0}} (F) \to \sum_{G} ({F ↾}_{z}) = \sum_{G} ({F ↾}_{(y \cup {supp}_{\underset{˙}{0}} (F))})$
36	35	eleq1d	$⊢ z = y \cup {supp}_{\underset{˙}{0}} (F) \to (\sum_{G} ({F ↾}_{z}) \in u \leftrightarrow \sum_{G} ({F ↾}_{(y \cup {supp}_{\underset{˙}{0}} (F))}) \in u)$
37	33 36	bitrd	$⊢ z = y \cup {supp}_{\underset{˙}{0}} (F) \to ((y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in u) \leftrightarrow \sum_{G} ({F ↾}_{(y \cup {supp}_{\underset{˙}{0}} (F))}) \in u)$
38	37	rspcv	$⊢ y \cup {supp}_{\underset{˙}{0}} (F) \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 {supp}_{\underset{˙}{0}} (F))}) \in u)$
39	28 38	syl	$⊢ ((φ \land u \in J) \land y \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 {supp}_{\underset{˙}{0}} (F))}) \in u)$
40	3	ad2antrr	$⊢ ((φ \land u \in J) \land y \in (𝒫 A \cap Fin)) \to G \in CMnd$
41	5	ad2antrr	$⊢ ((φ \land u \in J) \land y \in (𝒫 A \cap Fin)) \to A \in V$
42	6	ad2antrr	$⊢ ((φ \land u \in J) \land y \in (𝒫 A \cap Fin)) \to F : A ⟶ B$
43		ssun2	$⊢ F supp \underset{˙}{0} \subseteq y \cup {supp}_{\underset{˙}{0}} (F)$
44	43	a1i	$⊢ ((φ \land u \in J) \land y \in (𝒫 A \cap Fin)) \to F supp \underset{˙}{0} \subseteq y \cup {supp}_{\underset{˙}{0}} (F)$
45	1 2 40 41 42 44 23	gsumres	$⊢ ((φ \land u \in J) \land y \in (𝒫 A \cap Fin)) \to \sum_{G} ({F ↾}_{(y \cup {supp}_{\underset{˙}{0}} (F))}) = \sum_{G} F$
46	45	eleq1d	$⊢ ((φ \land u \in J) \land y \in (𝒫 A \cap Fin)) \to (\sum_{G} ({F ↾}_{(y \cup {supp}_{\underset{˙}{0}} (F))}) \in u \leftrightarrow \sum_{G} F \in u)$
47	39 46	sylibd	$⊢ ((φ \land u \in J) \land y \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 \in u)$
48	47	rexlimdva	$⊢ (φ \land u \in J) \to (\exists y \in (𝒫 A \cap Fin) \forall z \in (𝒫 A \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in u) \to \sum_{G} F \in u)$
49	7	fsuppimpd	$⊢ φ \to F supp \underset{˙}{0} \in Fin$
50		elfpw	$⊢ F supp \underset{˙}{0} \in (𝒫 A \cap Fin) \leftrightarrow (F supp \underset{˙}{0} \subseteq A \land F supp \underset{˙}{0} \in Fin)$
51	18 49 50	sylanbrc	$⊢ φ \to F supp \underset{˙}{0} \in (𝒫 A \cap Fin)$
52	3	ad2antrr	$⊢ ((φ \land (u \in J \land \sum_{G} F \in u)) \land (z \in (𝒫 A \cap Fin) \land F supp \underset{˙}{0} \subseteq z)) \to G \in CMnd$
53	5	ad2antrr	$⊢ ((φ \land (u \in J \land \sum_{G} F \in u)) \land (z \in (𝒫 A \cap Fin) \land F supp \underset{˙}{0} \subseteq z)) \to A \in V$
54	6	ad2antrr	$⊢ ((φ \land (u \in J \land \sum_{G} F \in u)) \land (z \in (𝒫 A \cap Fin) \land F supp \underset{˙}{0} \subseteq z)) \to F : A ⟶ B$
55		simprr	$⊢ ((φ \land (u \in J \land \sum_{G} F \in u)) \land (z \in (𝒫 A \cap Fin) \land F supp \underset{˙}{0} \subseteq z)) \to F supp \underset{˙}{0} \subseteq z$
56	7	ad2antrr	$⊢ ((φ \land (u \in J \land \sum_{G} F \in u)) \land (z \in (𝒫 A \cap Fin) \land F supp \underset{˙}{0} \subseteq z)) \to {finSupp}_{\underset{˙}{0}} (F)$
57	1 2 52 53 54 55 56	gsumres	$⊢ ((φ \land (u \in J \land \sum_{G} F \in u)) \land (z \in (𝒫 A \cap Fin) \land F supp \underset{˙}{0} \subseteq z)) \to \sum_{G} ({F ↾}_{z}) = \sum_{G} F$
58		simplrr	$⊢ ((φ \land (u \in J \land \sum_{G} F \in u)) \land (z \in (𝒫 A \cap Fin) \land F supp \underset{˙}{0} \subseteq z)) \to \sum_{G} F \in u$
59	57 58	eqeltrd	$⊢ ((φ \land (u \in J \land \sum_{G} F \in u)) \land (z \in (𝒫 A \cap Fin) \land F supp \underset{˙}{0} \subseteq z)) \to \sum_{G} ({F ↾}_{z}) \in u$
60	59	expr	$⊢ ((φ \land (u \in J \land \sum_{G} F \in u)) \land z \in (𝒫 A \cap Fin)) \to (F supp \underset{˙}{0} \subseteq z \to \sum_{G} ({F ↾}_{z}) \in u)$
61	60	ralrimiva	$⊢ (φ \land (u \in J \land \sum_{G} F \in u)) \to \forall z \in (𝒫 A \cap Fin) (F supp \underset{˙}{0} \subseteq z \to \sum_{G} ({F ↾}_{z}) \in u)$
62		sseq1	$⊢ y = F supp \underset{˙}{0} \to (y \subseteq z \leftrightarrow F supp \underset{˙}{0} \subseteq z)$
63	62	rspceaimv	$⊢ (F supp \underset{˙}{0} \in (𝒫 A \cap Fin) \land \forall z \in (𝒫 A \cap Fin) (F supp \underset{˙}{0} \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)$
64	51 61 63	syl2an2r	$⊢ (φ \land (u \in J \land \sum_{G} F \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)$
65	64	expr	$⊢ (φ \land u \in J) \to (\sum_{G} F \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	48 65	impbid	$⊢ (φ \land u \in J) \to (\exists y \in (𝒫 A \cap Fin) \forall z \in (𝒫 A \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in u) \leftrightarrow \sum_{G} F \in u)$
67		disjsn	$⊢ u \cap \{\sum_{G} F\} = \emptyset \leftrightarrow \neg \sum_{G} F \in u$
68	67	necon2abii	$⊢ \sum_{G} F \in u \leftrightarrow u \cap \{\sum_{G} F\} \neq \emptyset$
69	66 68	bitrdi	$⊢ (φ \land u \in J) \to (\exists y \in (𝒫 A \cap Fin) \forall z \in (𝒫 A \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in u) \leftrightarrow u \cap \{\sum_{G} F\} \neq \emptyset)$
70	69	imbi2d	$⊢ (φ \land u \in J) \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 u \cap \{\sum_{G} F\} \neq \emptyset))$
71	70	ralbidva	$⊢ φ \to (\forall u \in J (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 J (x \in u \to u \cap \{\sum_{G} F\} \neq \emptyset))$
72	13 71	anbi12d	$⊢ φ \to ((x \in B \land \forall u \in J (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 ⋃ J \land \forall u \in J (x \in u \to u \cap \{\sum_{G} F\} \neq \emptyset)))$
73		eqid	$⊢ 𝒫 A \cap Fin = 𝒫 A \cap Fin$
74	1 8 73 3 4 5 6	eltsms	$⊢ φ \to (x \in (G tsums F) \leftrightarrow (x \in B \land \forall u \in J (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))))$
75		topontop	$⊢ J \in TopOn (B) \to J \in Top$
76	10 75	syl	$⊢ φ \to J \in Top$
77	1 2 3 5 6 7	gsumcl	$⊢ φ \to \sum_{G} F \in B$
78	77	snssd	$⊢ φ \to \{\sum_{G} F\} \subseteq B$
79	78 12	sseqtrd	$⊢ φ \to \{\sum_{G} F\} \subseteq ⋃ J$
80		eqid	$⊢ ⋃ J = ⋃ J$
81	80	elcls2	$⊢ (J \in Top \land \{\sum_{G} F\} \subseteq ⋃ J) \to (x \in cls (J) (\{\sum_{G} F\}) \leftrightarrow (x \in ⋃ J \land \forall u \in J (x \in u \to u \cap \{\sum_{G} F\} \neq \emptyset)))$
82	76 79 81	syl2anc	$⊢ φ \to (x \in cls (J) (\{\sum_{G} F\}) \leftrightarrow (x \in ⋃ J \land \forall u \in J (x \in u \to u \cap \{\sum_{G} F\} \neq \emptyset)))$
83	72 74 82	3bitr4d	$⊢ φ \to (x \in (G tsums F) \leftrightarrow x \in cls (J) (\{\sum_{G} F\}))$
84	83	eqrdv	$⊢ φ \to G tsums F = cls (J) (\{\sum_{G} F\})$

Metamath Proof Explorer

Theorem tsmsgsum

Proof