eltsms

Description: The property of being a sum of the sequence F in the topological commutative monoid G . (Contributed by Mario Carneiro, 2-Sep-2015)

	Ref	Expression
Hypotheses	eltsms.b	$⊢ B = {Base}_{G}$
	eltsms.j	$⊢ J = TopOpen (G)$
	eltsms.s	$⊢ S = 𝒫 A \cap Fin$
	eltsms.1	$⊢ φ \to G \in CMnd$
	eltsms.2	$⊢ φ \to G \in TopSp$
	eltsms.a	$⊢ φ \to A \in V$
	eltsms.f	$⊢ φ \to F : A ⟶ B$
Assertion	eltsms	$⊢ φ \to (C \in (G tsums F) \leftrightarrow (C \in B \land \forall u \in J (C \in u \to \exists z \in S \forall y \in S (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in u))))$

Proof

Step	Hyp	Ref	Expression
1		eltsms.b	$⊢ B = {Base}_{G}$
2		eltsms.j	$⊢ J = TopOpen (G)$
3		eltsms.s	$⊢ S = 𝒫 A \cap Fin$
4		eltsms.1	$⊢ φ \to G \in CMnd$
5		eltsms.2	$⊢ φ \to G \in TopSp$
6		eltsms.a	$⊢ φ \to A \in V$
7		eltsms.f	$⊢ φ \to F : A ⟶ B$
8		eqid	$⊢ ran (z \in S ⟼ \{y \in S \| z \subseteq y\}) = ran (z \in S ⟼ \{y \in S \| z \subseteq y\})$
9	1 2 3 8 4 6 7	tsmsval	$⊢ φ \to G tsums F = (J fLimf (S filGen ran (z \in S ⟼ \{y \in S \| z \subseteq y\}))) ((y \in S ⟼ \sum_{G} ({F ↾}_{y})))$
10	9	eleq2d	$⊢ φ \to (C \in (G tsums F) \leftrightarrow C \in (J fLimf (S filGen ran (z \in S ⟼ \{y \in S \| z \subseteq y\}))) ((y \in S ⟼ \sum_{G} ({F ↾}_{y}))))$
11	1 2	istps	$⊢ G \in TopSp \leftrightarrow J \in TopOn (B)$
12	5 11	sylib	$⊢ φ \to J \in TopOn (B)$
13		eqid	$⊢ (z \in S ⟼ \{y \in S \| z \subseteq y\}) = (z \in S ⟼ \{y \in S \| z \subseteq y\})$
14	3 13 8 6	tsmsfbas	$⊢ φ \to ran (z \in S ⟼ \{y \in S \| z \subseteq y\}) \in fBas (S)$
15	1 3 4 6 7	tsmslem1	$⊢ (φ \land y \in S) \to \sum_{G} ({F ↾}_{y}) \in B$
16	15	fmpttd	$⊢ φ \to (y \in S ⟼ \sum_{G} ({F ↾}_{y})) : S ⟶ B$
17		eqid	$⊢ S filGen ran (z \in S ⟼ \{y \in S \| z \subseteq y\}) = S filGen ran (z \in S ⟼ \{y \in S \| z \subseteq y\})$
18	17	flffbas	$⊢ (J \in TopOn (B) \land ran (z \in S ⟼ \{y \in S \| z \subseteq y\}) \in fBas (S) \land (y \in S ⟼ \sum_{G} ({F ↾}_{y})) : S ⟶ B) \to (C \in (J fLimf (S filGen ran (z \in S ⟼ \{y \in S \| z \subseteq y\}))) ((y \in S ⟼ \sum_{G} ({F ↾}_{y}))) \leftrightarrow (C \in B \land \forall u \in J (C \in u \to \exists w \in ran (z \in S ⟼ \{y \in S \| z \subseteq y\}) (y \in S ⟼ \sum_{G} ({F ↾}_{y})) [w] \subseteq u)))$
19	12 14 16 18	syl3anc	$⊢ φ \to (C \in (J fLimf (S filGen ran (z \in S ⟼ \{y \in S \| z \subseteq y\}))) ((y \in S ⟼ \sum_{G} ({F ↾}_{y}))) \leftrightarrow (C \in B \land \forall u \in J (C \in u \to \exists w \in ran (z \in S ⟼ \{y \in S \| z \subseteq y\}) (y \in S ⟼ \sum_{G} ({F ↾}_{y})) [w] \subseteq u)))$
20		pwexg	$⊢ A \in V \to 𝒫 A \in V$
21		inex1g	$⊢ 𝒫 A \in V \to 𝒫 A \cap Fin \in V$
22	6 20 21	3syl	$⊢ φ \to 𝒫 A \cap Fin \in V$
23	3 22	eqeltrid	$⊢ φ \to S \in V$
24	23	adantr	$⊢ (φ \land u \in J) \to S \in V$
25		rabexg	$⊢ S \in V \to \{y \in S \| z \subseteq y\} \in V$
26	24 25	syl	$⊢ (φ \land u \in J) \to \{y \in S \| z \subseteq y\} \in V$
27	26	ralrimivw	$⊢ (φ \land u \in J) \to \forall z \in S \{y \in S \| z \subseteq y\} \in V$
28		imaeq2	$⊢ w = \{y \in S \| z \subseteq y\} \to (y \in S ⟼ \sum_{G} ({F ↾}_{y})) [w] = (y \in S ⟼ \sum_{G} ({F ↾}_{y})) [\{y \in S \| z \subseteq y\}]$
29	28	sseq1d	$⊢ w = \{y \in S \| z \subseteq y\} \to ((y \in S ⟼ \sum_{G} ({F ↾}_{y})) [w] \subseteq u \leftrightarrow (y \in S ⟼ \sum_{G} ({F ↾}_{y})) [\{y \in S \| z \subseteq y\}] \subseteq u)$
30	13 29	rexrnmptw	$⊢ \forall z \in S \{y \in S \| z \subseteq y\} \in V \to (\exists w \in ran (z \in S ⟼ \{y \in S \| z \subseteq y\}) (y \in S ⟼ \sum_{G} ({F ↾}_{y})) [w] \subseteq u \leftrightarrow \exists z \in S (y \in S ⟼ \sum_{G} ({F ↾}_{y})) [\{y \in S \| z \subseteq y\}] \subseteq u)$
31	27 30	syl	$⊢ (φ \land u \in J) \to (\exists w \in ran (z \in S ⟼ \{y \in S \| z \subseteq y\}) (y \in S ⟼ \sum_{G} ({F ↾}_{y})) [w] \subseteq u \leftrightarrow \exists z \in S (y \in S ⟼ \sum_{G} ({F ↾}_{y})) [\{y \in S \| z \subseteq y\}] \subseteq u)$
32		funmpt	$⊢ Fun (y \in S ⟼ \sum_{G} ({F ↾}_{y}))$
33		ssrab2	$⊢ \{y \in S \| z \subseteq y\} \subseteq S$
34		ovex	$⊢ \sum_{G} ({F ↾}_{y}) \in V$
35		eqid	$⊢ (y \in S ⟼ \sum_{G} ({F ↾}_{y})) = (y \in S ⟼ \sum_{G} ({F ↾}_{y}))$
36	34 35	dmmpti	$⊢ dom (y \in S ⟼ \sum_{G} ({F ↾}_{y})) = S$
37	33 36	sseqtrri	$⊢ \{y \in S \| z \subseteq y\} \subseteq dom (y \in S ⟼ \sum_{G} ({F ↾}_{y}))$
38		funimass3	$⊢ (Fun (y \in S ⟼ \sum_{G} ({F ↾}_{y})) \land \{y \in S \| z \subseteq y\} \subseteq dom (y \in S ⟼ \sum_{G} ({F ↾}_{y}))) \to ((y \in S ⟼ \sum_{G} ({F ↾}_{y})) [\{y \in S \| z \subseteq y\}] \subseteq u \leftrightarrow \{y \in S \| z \subseteq y\} \subseteq {(y \in S ⟼ \sum_{G} ({F ↾}_{y}))}^{-1} [u])$
39	32 37 38	mp2an	$⊢ (y \in S ⟼ \sum_{G} ({F ↾}_{y})) [\{y \in S \| z \subseteq y\}] \subseteq u \leftrightarrow \{y \in S \| z \subseteq y\} \subseteq {(y \in S ⟼ \sum_{G} ({F ↾}_{y}))}^{-1} [u]$
40	35	mptpreima	$⊢ {(y \in S ⟼ \sum_{G} ({F ↾}_{y}))}^{-1} [u] = \{y \in S \| \sum_{G} ({F ↾}_{y}) \in u\}$
41	40	sseq2i	$⊢ \{y \in S \| z \subseteq y\} \subseteq {(y \in S ⟼ \sum_{G} ({F ↾}_{y}))}^{-1} [u] \leftrightarrow \{y \in S \| z \subseteq y\} \subseteq \{y \in S \| \sum_{G} ({F ↾}_{y}) \in u\}$
42		ss2rab	$⊢ \{y \in S \| z \subseteq y\} \subseteq \{y \in S \| \sum_{G} ({F ↾}_{y}) \in u\} \leftrightarrow \forall y \in S (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in u)$
43	39 41 42	3bitri	$⊢ (y \in S ⟼ \sum_{G} ({F ↾}_{y})) [\{y \in S \| z \subseteq y\}] \subseteq u \leftrightarrow \forall y \in S (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in u)$
44	43	rexbii	$⊢ \exists z \in S (y \in S ⟼ \sum_{G} ({F ↾}_{y})) [\{y \in S \| z \subseteq y\}] \subseteq u \leftrightarrow \exists z \in S \forall y \in S (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in u)$
45	31 44	bitrdi	$⊢ (φ \land u \in J) \to (\exists w \in ran (z \in S ⟼ \{y \in S \| z \subseteq y\}) (y \in S ⟼ \sum_{G} ({F ↾}_{y})) [w] \subseteq u \leftrightarrow \exists z \in S \forall y \in S (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in u))$
46	45	imbi2d	$⊢ (φ \land u \in J) \to ((C \in u \to \exists w \in ran (z \in S ⟼ \{y \in S \| z \subseteq y\}) (y \in S ⟼ \sum_{G} ({F ↾}_{y})) [w] \subseteq u) \leftrightarrow (C \in u \to \exists z \in S \forall y \in S (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in u)))$
47	46	ralbidva	$⊢ φ \to (\forall u \in J (C \in u \to \exists w \in ran (z \in S ⟼ \{y \in S \| z \subseteq y\}) (y \in S ⟼ \sum_{G} ({F ↾}_{y})) [w] \subseteq u) \leftrightarrow \forall u \in J (C \in u \to \exists z \in S \forall y \in S (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in u)))$
48	47	anbi2d	$⊢ φ \to ((C \in B \land \forall u \in J (C \in u \to \exists w \in ran (z \in S ⟼ \{y \in S \| z \subseteq y\}) (y \in S ⟼ \sum_{G} ({F ↾}_{y})) [w] \subseteq u)) \leftrightarrow (C \in B \land \forall u \in J (C \in u \to \exists z \in S \forall y \in S (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in u))))$
49	10 19 48	3bitrd	$⊢ φ \to (C \in (G tsums F) \leftrightarrow (C \in B \land \forall u \in J (C \in u \to \exists z \in S \forall y \in S (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in u))))$

Metamath Proof Explorer

Theorem eltsms

Proof