tsmssubm

Description: Evaluate an infinite group sum in a submonoid. (Contributed by Mario Carneiro, 18-Sep-2015)

	Ref	Expression
Hypotheses	tsmssubm.a	$⊢ φ \to A \in V$
	tsmssubm.1	$⊢ φ \to G \in CMnd$
	tsmssubm.2	$⊢ φ \to G \in TopSp$
	tsmssubm.s	$⊢ φ \to S \in SubMnd (G)$
	tsmssubm.f	$⊢ φ \to F : A ⟶ S$
	tsmssubm.h	$⊢ H = G ↾_{𝑠} S$
Assertion	tsmssubm	$⊢ φ \to H tsums F = (G tsums F) \cap S$

Proof

Step	Hyp	Ref	Expression
1		tsmssubm.a	$⊢ φ \to A \in V$
2		tsmssubm.1	$⊢ φ \to G \in CMnd$
3		tsmssubm.2	$⊢ φ \to G \in TopSp$
4		tsmssubm.s	$⊢ φ \to S \in SubMnd (G)$
5		tsmssubm.f	$⊢ φ \to F : A ⟶ S$
6		tsmssubm.h	$⊢ H = G ↾_{𝑠} S$
7	6	submbas	$⊢ S \in SubMnd (G) \to S = {Base}_{H}$
8	4 7	syl	$⊢ φ \to S = {Base}_{H}$
9	8	eleq2d	$⊢ φ \to (x \in S \leftrightarrow x \in {Base}_{H})$
10	9	anbi1d	$⊢ φ \to ((x \in S \land \forall v \in TopOpen (H) (x \in v \to \exists z \in (𝒫 A \cap Fin) \forall y \in (𝒫 A \cap Fin) (z \subseteq y \to \sum_{H} ({F ↾}_{y}) \in v))) \leftrightarrow (x \in {Base}_{H} \land \forall v \in TopOpen (H) (x \in v \to \exists z \in (𝒫 A \cap Fin) \forall y \in (𝒫 A \cap Fin) (z \subseteq y \to \sum_{H} ({F ↾}_{y}) \in v))))$
11		elin	$⊢ x \in ((G tsums F) \cap S) \leftrightarrow (x \in (G tsums F) \land x \in S)$
12	11	biancomi	$⊢ x \in ((G tsums F) \cap S) \leftrightarrow (x \in S \land x \in (G tsums F))$
13		eqid	$⊢ {Base}_{G} = {Base}_{G}$
14	13	submss	$⊢ S \in SubMnd (G) \to S \subseteq {Base}_{G}$
15	4 14	syl	$⊢ φ \to S \subseteq {Base}_{G}$
16	15	sselda	$⊢ (φ \land x \in S) \to x \in {Base}_{G}$
17		eqid	$⊢ TopOpen (G) = TopOpen (G)$
18		eqid	$⊢ 𝒫 A \cap Fin = 𝒫 A \cap Fin$
19	5 15	fssd	$⊢ φ \to F : A ⟶ {Base}_{G}$
20	13 17 18 2 3 1 19	eltsms	$⊢ φ \to (x \in (G tsums F) \leftrightarrow (x \in {Base}_{G} \land \forall u \in TopOpen (G) (x \in u \to \exists z \in (𝒫 A \cap Fin) \forall y \in (𝒫 A \cap Fin) (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in u))))$
21	20	baibd	$⊢ (φ \land x \in {Base}_{G}) \to (x \in (G tsums F) \leftrightarrow \forall u \in TopOpen (G) (x \in u \to \exists z \in (𝒫 A \cap Fin) \forall y \in (𝒫 A \cap Fin) (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in u)))$
22	16 21	syldan	$⊢ (φ \land x \in S) \to (x \in (G tsums F) \leftrightarrow \forall u \in TopOpen (G) (x \in u \to \exists z \in (𝒫 A \cap Fin) \forall y \in (𝒫 A \cap Fin) (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in u)))$
23		vex	$⊢ u \in V$
24	23	inex1	$⊢ u \cap S \in V$
25	24	a1i	$⊢ ((φ \land x \in S) \land u \in TopOpen (G)) \to u \cap S \in V$
26	6 17	resstopn	$⊢ TopOpen (G) ↾_{𝑡} S = TopOpen (H)$
27	26	eleq2i	$⊢ v \in (TopOpen (G) ↾_{𝑡} S) \leftrightarrow v \in TopOpen (H)$
28		fvex	$⊢ TopOpen (G) \in V$
29		elrest	$⊢ (TopOpen (G) \in V \land S \in SubMnd (G)) \to (v \in (TopOpen (G) ↾_{𝑡} S) \leftrightarrow \exists u \in TopOpen (G) v = u \cap S)$
30	28 4 29	sylancr	$⊢ φ \to (v \in (TopOpen (G) ↾_{𝑡} S) \leftrightarrow \exists u \in TopOpen (G) v = u \cap S)$
31	30	adantr	$⊢ (φ \land x \in S) \to (v \in (TopOpen (G) ↾_{𝑡} S) \leftrightarrow \exists u \in TopOpen (G) v = u \cap S)$
32	27 31	bitr3id	$⊢ (φ \land x \in S) \to (v \in TopOpen (H) \leftrightarrow \exists u \in TopOpen (G) v = u \cap S)$
33		eleq2	$⊢ v = u \cap S \to (x \in v \leftrightarrow x \in (u \cap S))$
34		elin	$⊢ x \in (u \cap S) \leftrightarrow (x \in u \land x \in S)$
35	34	rbaib	$⊢ x \in S \to (x \in (u \cap S) \leftrightarrow x \in u)$
36	35	adantl	$⊢ (φ \land x \in S) \to (x \in (u \cap S) \leftrightarrow x \in u)$
37	33 36	sylan9bbr	$⊢ ((φ \land x \in S) \land v = u \cap S) \to (x \in v \leftrightarrow x \in u)$
38		eleq2	$⊢ v = u \cap S \to (\sum_{H} ({F ↾}_{y}) \in v \leftrightarrow \sum_{H} ({F ↾}_{y}) \in (u \cap S))$
39		eqid	$⊢ {Base}_{H} = {Base}_{H}$
40		eqid	$⊢ 0_{H} = 0_{H}$
41	6	submmnd	$⊢ S \in SubMnd (G) \to H \in Mnd$
42	4 41	syl	$⊢ φ \to H \in Mnd$
43	6	subcmn	$⊢ (G \in CMnd \land H \in Mnd) \to H \in CMnd$
44	2 42 43	syl2anc	$⊢ φ \to H \in CMnd$
45	44	ad2antrr	$⊢ ((φ \land x \in S) \land y \in (𝒫 A \cap Fin)) \to H \in CMnd$
46		elinel2	$⊢ y \in (𝒫 A \cap Fin) \to y \in Fin$
47	46	adantl	$⊢ ((φ \land x \in S) \land y \in (𝒫 A \cap Fin)) \to y \in Fin$
48	5	ad2antrr	$⊢ ((φ \land x \in S) \land y \in (𝒫 A \cap Fin)) \to F : A ⟶ S$
49		elfpw	$⊢ y \in (𝒫 A \cap Fin) \leftrightarrow (y \subseteq A \land y \in Fin)$
50	49	simplbi	$⊢ y \in (𝒫 A \cap Fin) \to y \subseteq A$
51	50	adantl	$⊢ ((φ \land x \in S) \land y \in (𝒫 A \cap Fin)) \to y \subseteq A$
52	48 51	fssresd	$⊢ ((φ \land x \in S) \land y \in (𝒫 A \cap Fin)) \to ({F ↾}_{y}) : y ⟶ S$
53	8	ad2antrr	$⊢ ((φ \land x \in S) \land y \in (𝒫 A \cap Fin)) \to S = {Base}_{H}$
54	53	feq3d	$⊢ ((φ \land x \in S) \land y \in (𝒫 A \cap Fin)) \to (({F ↾}_{y}) : y ⟶ S \leftrightarrow ({F ↾}_{y}) : y ⟶ {Base}_{H})$
55	52 54	mpbid	$⊢ ((φ \land x \in S) \land y \in (𝒫 A \cap Fin)) \to ({F ↾}_{y}) : y ⟶ {Base}_{H}$
56		fvex	$⊢ 0_{H} \in V$
57	56	a1i	$⊢ ((φ \land x \in S) \land y \in (𝒫 A \cap Fin)) \to 0_{H} \in V$
58	52 47 57	fdmfifsupp	$⊢ ((φ \land x \in S) \land y \in (𝒫 A \cap Fin)) \to {finSupp}_{0_{H}} (({F ↾}_{y}))$
59	39 40 45 47 55 58	gsumcl	$⊢ ((φ \land x \in S) \land y \in (𝒫 A \cap Fin)) \to \sum_{H} ({F ↾}_{y}) \in {Base}_{H}$
60	59 53	eleqtrrd	$⊢ ((φ \land x \in S) \land y \in (𝒫 A \cap Fin)) \to \sum_{H} ({F ↾}_{y}) \in S$
61		elin	$⊢ \sum_{H} ({F ↾}_{y}) \in (u \cap S) \leftrightarrow (\sum_{H} ({F ↾}_{y}) \in u \land \sum_{H} ({F ↾}_{y}) \in S)$
62	61	rbaib	$⊢ \sum_{H} ({F ↾}_{y}) \in S \to (\sum_{H} ({F ↾}_{y}) \in (u \cap S) \leftrightarrow \sum_{H} ({F ↾}_{y}) \in u)$
63	60 62	syl	$⊢ ((φ \land x \in S) \land y \in (𝒫 A \cap Fin)) \to (\sum_{H} ({F ↾}_{y}) \in (u \cap S) \leftrightarrow \sum_{H} ({F ↾}_{y}) \in u)$
64	4	ad2antrr	$⊢ ((φ \land x \in S) \land y \in (𝒫 A \cap Fin)) \to S \in SubMnd (G)$
65	47 64 52 6	gsumsubm	$⊢ ((φ \land x \in S) \land y \in (𝒫 A \cap Fin)) \to \sum_{G} ({F ↾}_{y}) = \sum_{H} ({F ↾}_{y})$
66	65	eleq1d	$⊢ ((φ \land x \in S) \land y \in (𝒫 A \cap Fin)) \to (\sum_{G} ({F ↾}_{y}) \in u \leftrightarrow \sum_{H} ({F ↾}_{y}) \in u)$
67	63 66	bitr4d	$⊢ ((φ \land x \in S) \land y \in (𝒫 A \cap Fin)) \to (\sum_{H} ({F ↾}_{y}) \in (u \cap S) \leftrightarrow \sum_{G} ({F ↾}_{y}) \in u)$
68	38 67	sylan9bbr	$⊢ (((φ \land x \in S) \land y \in (𝒫 A \cap Fin)) \land v = u \cap S) \to (\sum_{H} ({F ↾}_{y}) \in v \leftrightarrow \sum_{G} ({F ↾}_{y}) \in u)$
69	68	an32s	$⊢ (((φ \land x \in S) \land v = u \cap S) \land y \in (𝒫 A \cap Fin)) \to (\sum_{H} ({F ↾}_{y}) \in v \leftrightarrow \sum_{G} ({F ↾}_{y}) \in u)$
70	69	imbi2d	$⊢ (((φ \land x \in S) \land v = u \cap S) \land y \in (𝒫 A \cap Fin)) \to ((z \subseteq y \to \sum_{H} ({F ↾}_{y}) \in v) \leftrightarrow (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in u))$
71	70	ralbidva	$⊢ ((φ \land x \in S) \land v = u \cap S) \to (\forall y \in (𝒫 A \cap Fin) (z \subseteq y \to \sum_{H} ({F ↾}_{y}) \in v) \leftrightarrow \forall y \in (𝒫 A \cap Fin) (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in u))$
72	71	rexbidv	$⊢ ((φ \land x \in S) \land v = u \cap S) \to (\exists z \in (𝒫 A \cap Fin) \forall y \in (𝒫 A \cap Fin) (z \subseteq y \to \sum_{H} ({F ↾}_{y}) \in v) \leftrightarrow \exists z \in (𝒫 A \cap Fin) \forall y \in (𝒫 A \cap Fin) (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in u))$
73	37 72	imbi12d	$⊢ ((φ \land x \in S) \land v = u \cap S) \to ((x \in v \to \exists z \in (𝒫 A \cap Fin) \forall y \in (𝒫 A \cap Fin) (z \subseteq y \to \sum_{H} ({F ↾}_{y}) \in v)) \leftrightarrow (x \in u \to \exists z \in (𝒫 A \cap Fin) \forall y \in (𝒫 A \cap Fin) (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in u)))$
74	25 32 73	ralxfr2d	$⊢ (φ \land x \in S) \to (\forall v \in TopOpen (H) (x \in v \to \exists z \in (𝒫 A \cap Fin) \forall y \in (𝒫 A \cap Fin) (z \subseteq y \to \sum_{H} ({F ↾}_{y}) \in v)) \leftrightarrow \forall u \in TopOpen (G) (x \in u \to \exists z \in (𝒫 A \cap Fin) \forall y \in (𝒫 A \cap Fin) (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in u)))$
75	22 74	bitr4d	$⊢ (φ \land x \in S) \to (x \in (G tsums F) \leftrightarrow \forall v \in TopOpen (H) (x \in v \to \exists z \in (𝒫 A \cap Fin) \forall y \in (𝒫 A \cap Fin) (z \subseteq y \to \sum_{H} ({F ↾}_{y}) \in v)))$
76	75	pm5.32da	$⊢ φ \to ((x \in S \land x \in (G tsums F)) \leftrightarrow (x \in S \land \forall v \in TopOpen (H) (x \in v \to \exists z \in (𝒫 A \cap Fin) \forall y \in (𝒫 A \cap Fin) (z \subseteq y \to \sum_{H} ({F ↾}_{y}) \in v))))$
77	12 76	bitrid	$⊢ φ \to (x \in ((G tsums F) \cap S) \leftrightarrow (x \in S \land \forall v \in TopOpen (H) (x \in v \to \exists z \in (𝒫 A \cap Fin) \forall y \in (𝒫 A \cap Fin) (z \subseteq y \to \sum_{H} ({F ↾}_{y}) \in v))))$
78		eqid	$⊢ TopOpen (H) = TopOpen (H)$
79		resstps	$⊢ (G \in TopSp \land S \in SubMnd (G)) \to G ↾_{𝑠} S \in TopSp$
80	3 4 79	syl2anc	$⊢ φ \to G ↾_{𝑠} S \in TopSp$
81	6 80	eqeltrid	$⊢ φ \to H \in TopSp$
82	8	feq3d	$⊢ φ \to (F : A ⟶ S \leftrightarrow F : A ⟶ {Base}_{H})$
83	5 82	mpbid	$⊢ φ \to F : A ⟶ {Base}_{H}$
84	39 78 18 44 81 1 83	eltsms	$⊢ φ \to (x \in (H tsums F) \leftrightarrow (x \in {Base}_{H} \land \forall v \in TopOpen (H) (x \in v \to \exists z \in (𝒫 A \cap Fin) \forall y \in (𝒫 A \cap Fin) (z \subseteq y \to \sum_{H} ({F ↾}_{y}) \in v))))$
85	10 77 84	3bitr4rd	$⊢ φ \to (x \in (H tsums F) \leftrightarrow x \in ((G tsums F) \cap S))$
86	85	eqrdv	$⊢ φ \to H tsums F = (G tsums F) \cap S$

Metamath Proof Explorer

Theorem tsmssubm

Proof