tsmsadd

Description: The sum of two infinite group sums. (Contributed by Mario Carneiro, 19-Sep-2015) (Proof shortened by AV, 24-Jul-2019)

	Ref	Expression
Hypotheses	tsmsadd.b	$⊢ B = {Base}_{G}$
	tsmsadd.p	$⊢ \underset{˙}{+} = +_{G}$
	tsmsadd.1	$⊢ φ \to G \in CMnd$
	tsmsadd.2	$⊢ φ \to G \in TopMnd$
	tsmsadd.a	$⊢ φ \to A \in V$
	tsmsadd.f	$⊢ φ \to F : A ⟶ B$
	tsmsadd.h	$⊢ φ \to H : A ⟶ B$
	tsmsadd.x	$⊢ φ \to X \in (G tsums F)$
	tsmsadd.y	$⊢ φ \to Y \in (G tsums H)$
Assertion	tsmsadd	$⊢ φ \to X \underset{˙}{+} Y \in (G tsums (F {\underset{˙}{+}}_{f} H))$

Proof

Step	Hyp	Ref	Expression
1		tsmsadd.b	$⊢ B = {Base}_{G}$
2		tsmsadd.p	$⊢ \underset{˙}{+} = +_{G}$
3		tsmsadd.1	$⊢ φ \to G \in CMnd$
4		tsmsadd.2	$⊢ φ \to G \in TopMnd$
5		tsmsadd.a	$⊢ φ \to A \in V$
6		tsmsadd.f	$⊢ φ \to F : A ⟶ B$
7		tsmsadd.h	$⊢ φ \to H : A ⟶ B$
8		tsmsadd.x	$⊢ φ \to X \in (G tsums F)$
9		tsmsadd.y	$⊢ φ \to Y \in (G tsums H)$
10		tmdtps	$⊢ G \in TopMnd \to G \in TopSp$
11	4 10	syl	$⊢ φ \to G \in TopSp$
12	1 3 11 5 6	tsmscl	$⊢ φ \to G tsums F \subseteq B$
13	12 8	sseldd	$⊢ φ \to X \in B$
14	1 3 11 5 7	tsmscl	$⊢ φ \to G tsums H \subseteq B$
15	14 9	sseldd	$⊢ φ \to Y \in B$
16		eqid	$⊢ +_{𝑓} (G) = +_{𝑓} (G)$
17	1 2 16	plusfval	$⊢ (X \in B \land Y \in B) \to X +_{𝑓} (G) Y = X \underset{˙}{+} Y$
18	13 15 17	syl2anc	$⊢ φ \to X +_{𝑓} (G) Y = X \underset{˙}{+} Y$
19		eqid	$⊢ TopOpen (G) = TopOpen (G)$
20	1 19	istps	$⊢ G \in TopSp \leftrightarrow TopOpen (G) \in TopOn (B)$
21	11 20	sylib	$⊢ φ \to TopOpen (G) \in TopOn (B)$
22		eqid	$⊢ 𝒫 A \cap Fin = 𝒫 A \cap Fin$
23		eqid	$⊢ (y \in (𝒫 A \cap Fin) ⟼ \{z \in (𝒫 A \cap Fin) \| y \subseteq z\}) = (y \in (𝒫 A \cap Fin) ⟼ \{z \in (𝒫 A \cap Fin) \| y \subseteq z\})$
24		eqid	$⊢ ran (y \in (𝒫 A \cap Fin) ⟼ \{z \in (𝒫 A \cap Fin) \| y \subseteq z\}) = ran (y \in (𝒫 A \cap Fin) ⟼ \{z \in (𝒫 A \cap Fin) \| y \subseteq z\})$
25	22 23 24 5	tsmsfbas	$⊢ φ \to ran (y \in (𝒫 A \cap Fin) ⟼ \{z \in (𝒫 A \cap Fin) \| y \subseteq z\}) \in fBas (𝒫 A \cap Fin)$
26		fgcl	$⊢ ran (y \in (𝒫 A \cap Fin) ⟼ \{z \in (𝒫 A \cap Fin) \| y \subseteq z\}) \in fBas (𝒫 A \cap Fin) \to (𝒫 A \cap Fin) filGen ran (y \in (𝒫 A \cap Fin) ⟼ \{z \in (𝒫 A \cap Fin) \| y \subseteq z\}) \in Fil (𝒫 A \cap Fin)$
27	25 26	syl	$⊢ φ \to (𝒫 A \cap Fin) filGen ran (y \in (𝒫 A \cap Fin) ⟼ \{z \in (𝒫 A \cap Fin) \| y \subseteq z\}) \in Fil (𝒫 A \cap Fin)$
28	1 22 3 5 6	tsmslem1	$⊢ (φ \land z \in (𝒫 A \cap Fin)) \to \sum_{G} ({F ↾}_{z}) \in B$
29	1 22 3 5 7	tsmslem1	$⊢ (φ \land z \in (𝒫 A \cap Fin)) \to \sum_{G} ({H ↾}_{z}) \in B$
30	1 19 22 24 3 5 6	tsmsval	$⊢ φ \to G tsums F = (TopOpen (G) fLimf ((𝒫 A \cap Fin) filGen ran (y \in (𝒫 A \cap Fin) ⟼ \{z \in (𝒫 A \cap Fin) \| y \subseteq z\}))) ((z \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{z})))$
31	8 30	eleqtrd	$⊢ φ \to X \in (TopOpen (G) fLimf ((𝒫 A \cap Fin) filGen ran (y \in (𝒫 A \cap Fin) ⟼ \{z \in (𝒫 A \cap Fin) \| y \subseteq z\}))) ((z \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{z})))$
32	1 19 22 24 3 5 7	tsmsval	$⊢ φ \to G tsums H = (TopOpen (G) fLimf ((𝒫 A \cap Fin) filGen ran (y \in (𝒫 A \cap Fin) ⟼ \{z \in (𝒫 A \cap Fin) \| y \subseteq z\}))) ((z \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({H ↾}_{z})))$
33	9 32	eleqtrd	$⊢ φ \to Y \in (TopOpen (G) fLimf ((𝒫 A \cap Fin) filGen ran (y \in (𝒫 A \cap Fin) ⟼ \{z \in (𝒫 A \cap Fin) \| y \subseteq z\}))) ((z \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({H ↾}_{z})))$
34	19 16	tmdcn	$⊢ G \in TopMnd \to +_{𝑓} (G) \in ((TopOpen (G) \times_{t} TopOpen (G)) Cn TopOpen (G))$
35	4 34	syl	$⊢ φ \to +_{𝑓} (G) \in ((TopOpen (G) \times_{t} TopOpen (G)) Cn TopOpen (G))$
36	13 15	opelxpd	$⊢ φ \to ⟨X, Y⟩ \in (B \times B)$
37		txtopon	$⊢ (TopOpen (G) \in TopOn (B) \land TopOpen (G) \in TopOn (B)) \to TopOpen (G) \times_{t} TopOpen (G) \in TopOn (B \times B)$
38	21 21 37	syl2anc	$⊢ φ \to TopOpen (G) \times_{t} TopOpen (G) \in TopOn (B \times B)$
39		toponuni	$⊢ TopOpen (G) \times_{t} TopOpen (G) \in TopOn (B \times B) \to B \times B = ⋃ (TopOpen (G) \times_{t} TopOpen (G))$
40	38 39	syl	$⊢ φ \to B \times B = ⋃ (TopOpen (G) \times_{t} TopOpen (G))$
41	36 40	eleqtrd	$⊢ φ \to ⟨X, Y⟩ \in ⋃ (TopOpen (G) \times_{t} TopOpen (G))$
42		eqid	$⊢ ⋃ (TopOpen (G) \times_{t} TopOpen (G)) = ⋃ (TopOpen (G) \times_{t} TopOpen (G))$
43	42	cncnpi	$⊢ (+_{𝑓} (G) \in ((TopOpen (G) \times_{t} TopOpen (G)) Cn TopOpen (G)) \land ⟨X, Y⟩ \in ⋃ (TopOpen (G) \times_{t} TopOpen (G))) \to +_{𝑓} (G) \in ((TopOpen (G) \times_{t} TopOpen (G)) CnP TopOpen (G)) (⟨X, Y⟩)$
44	35 41 43	syl2anc	$⊢ φ \to +_{𝑓} (G) \in ((TopOpen (G) \times_{t} TopOpen (G)) CnP TopOpen (G)) (⟨X, Y⟩)$
45	21 21 27 28 29 31 33 44	flfcnp2	$⊢ φ \to X +_{𝑓} (G) Y \in (TopOpen (G) fLimf ((𝒫 A \cap Fin) filGen ran (y \in (𝒫 A \cap Fin) ⟼ \{z \in (𝒫 A \cap Fin) \| y \subseteq z\}))) ((z \in (𝒫 A \cap Fin) ⟼ (\sum_{G}, ({F ↾}_{z})) +_{𝑓} (G) (\sum_{G}, ({H ↾}_{z}))))$
46	18 45	eqeltrrd	$⊢ φ \to X \underset{˙}{+} Y \in (TopOpen (G) fLimf ((𝒫 A \cap Fin) filGen ran (y \in (𝒫 A \cap Fin) ⟼ \{z \in (𝒫 A \cap Fin) \| y \subseteq z\}))) ((z \in (𝒫 A \cap Fin) ⟼ (\sum_{G}, ({F ↾}_{z})) +_{𝑓} (G) (\sum_{G}, ({H ↾}_{z}))))$
47		cmnmnd	$⊢ G \in CMnd \to G \in Mnd$
48	3 47	syl	$⊢ φ \to G \in Mnd$
49	1 2	mndcl	$⊢ (G \in Mnd \land x \in B \land y \in B) \to x \underset{˙}{+} y \in B$
50	49	3expb	$⊢ (G \in Mnd \land (x \in B \land y \in B)) \to x \underset{˙}{+} y \in B$
51	48 50	sylan	$⊢ (φ \land (x \in B \land y \in B)) \to x \underset{˙}{+} y \in B$
52		inidm	$⊢ A \cap A = A$
53	51 6 7 5 5 52	off	$⊢ φ \to (F {\underset{˙}{+}}_{f} H) : A ⟶ B$
54	1 19 22 24 3 5 53	tsmsval	$⊢ φ \to G tsums (F {\underset{˙}{+}}_{f} H) = (TopOpen (G) fLimf ((𝒫 A \cap Fin) filGen ran (y \in (𝒫 A \cap Fin) ⟼ \{z \in (𝒫 A \cap Fin) \| y \subseteq z\}))) ((z \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({(F {\underset{˙}{+}}_{f} H) ↾}_{z})))$
55		eqid	$⊢ 0_{G} = 0_{G}$
56	3	adantr	$⊢ (φ \land z \in (𝒫 A \cap Fin)) \to G \in CMnd$
57		elinel2	$⊢ z \in (𝒫 A \cap Fin) \to z \in Fin$
58	57	adantl	$⊢ (φ \land z \in (𝒫 A \cap Fin)) \to z \in Fin$
59		elfpw	$⊢ z \in (𝒫 A \cap Fin) \leftrightarrow (z \subseteq A \land z \in Fin)$
60	59	simplbi	$⊢ z \in (𝒫 A \cap Fin) \to z \subseteq A$
61		fssres	$⊢ (F : A ⟶ B \land z \subseteq A) \to ({F ↾}_{z}) : z ⟶ B$
62	6 60 61	syl2an	$⊢ (φ \land z \in (𝒫 A \cap Fin)) \to ({F ↾}_{z}) : z ⟶ B$
63		fssres	$⊢ (H : A ⟶ B \land z \subseteq A) \to ({H ↾}_{z}) : z ⟶ B$
64	7 60 63	syl2an	$⊢ (φ \land z \in (𝒫 A \cap Fin)) \to ({H ↾}_{z}) : z ⟶ B$
65		fvexd	$⊢ (φ \land z \in (𝒫 A \cap Fin)) \to 0_{G} \in V$
66	62 58 65	fdmfifsupp	$⊢ (φ \land z \in (𝒫 A \cap Fin)) \to {finSupp}_{0_{G}} (({F ↾}_{z}))$
67	64 58 65	fdmfifsupp	$⊢ (φ \land z \in (𝒫 A \cap Fin)) \to {finSupp}_{0_{G}} (({H ↾}_{z}))$
68	1 55 2 56 58 62 64 66 67	gsumadd	$⊢ (φ \land z \in (𝒫 A \cap Fin)) \to \sum_{G} (({F ↾}_{z}) {\underset{˙}{+}}_{f} ({H ↾}_{z})) = (\sum_{G}, ({F ↾}_{z})) \underset{˙}{+} (\sum_{G}, ({H ↾}_{z}))$
69	6 5	fexd	$⊢ φ \to F \in V$
70	7 5	fexd	$⊢ φ \to H \in V$
71		offres	$⊢ (F \in V \land H \in V) \to {(F {\underset{˙}{+}}_{f} H) ↾}_{z} = ({F ↾}_{z}) {\underset{˙}{+}}_{f} ({H ↾}_{z})$
72	69 70 71	syl2anc	$⊢ φ \to {(F {\underset{˙}{+}}_{f} H) ↾}_{z} = ({F ↾}_{z}) {\underset{˙}{+}}_{f} ({H ↾}_{z})$
73	72	adantr	$⊢ (φ \land z \in (𝒫 A \cap Fin)) \to {(F {\underset{˙}{+}}_{f} H) ↾}_{z} = ({F ↾}_{z}) {\underset{˙}{+}}_{f} ({H ↾}_{z})$
74	73	oveq2d	$⊢ (φ \land z \in (𝒫 A \cap Fin)) \to \sum_{G} ({(F {\underset{˙}{+}}_{f} H) ↾}_{z}) = \sum_{G} (({F ↾}_{z}) {\underset{˙}{+}}_{f} ({H ↾}_{z}))$
75	1 2 16	plusfval	$⊢ (\sum_{G} ({F ↾}_{z}) \in B \land \sum_{G} ({H ↾}_{z}) \in B) \to (\sum_{G}, ({F ↾}_{z})) +_{𝑓} (G) (\sum_{G}, ({H ↾}_{z})) = (\sum_{G}, ({F ↾}_{z})) \underset{˙}{+} (\sum_{G}, ({H ↾}_{z}))$
76	28 29 75	syl2anc	$⊢ (φ \land z \in (𝒫 A \cap Fin)) \to (\sum_{G}, ({F ↾}_{z})) +_{𝑓} (G) (\sum_{G}, ({H ↾}_{z})) = (\sum_{G}, ({F ↾}_{z})) \underset{˙}{+} (\sum_{G}, ({H ↾}_{z}))$
77	68 74 76	3eqtr4d	$⊢ (φ \land z \in (𝒫 A \cap Fin)) \to \sum_{G} ({(F {\underset{˙}{+}}_{f} H) ↾}_{z}) = (\sum_{G}, ({F ↾}_{z})) +_{𝑓} (G) (\sum_{G}, ({H ↾}_{z}))$
78	77	mpteq2dva	$⊢ φ \to (z \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({(F {\underset{˙}{+}}_{f} H) ↾}_{z})) = (z \in (𝒫 A \cap Fin) ⟼ (\sum_{G}, ({F ↾}_{z})) +_{𝑓} (G) (\sum_{G}, ({H ↾}_{z})))$
79	78	fveq2d	$⊢ φ \to (TopOpen (G) fLimf ((𝒫 A \cap Fin) filGen ran (y \in (𝒫 A \cap Fin) ⟼ \{z \in (𝒫 A \cap Fin) \| y \subseteq z\}))) ((z \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({(F {\underset{˙}{+}}_{f} H) ↾}_{z}))) = (TopOpen (G) fLimf ((𝒫 A \cap Fin) filGen ran (y \in (𝒫 A \cap Fin) ⟼ \{z \in (𝒫 A \cap Fin) \| y \subseteq z\}))) ((z \in (𝒫 A \cap Fin) ⟼ (\sum_{G}, ({F ↾}_{z})) +_{𝑓} (G) (\sum_{G}, ({H ↾}_{z}))))$
80	54 79	eqtrd	$⊢ φ \to G tsums (F {\underset{˙}{+}}_{f} H) = (TopOpen (G) fLimf ((𝒫 A \cap Fin) filGen ran (y \in (𝒫 A \cap Fin) ⟼ \{z \in (𝒫 A \cap Fin) \| y \subseteq z\}))) ((z \in (𝒫 A \cap Fin) ⟼ (\sum_{G}, ({F ↾}_{z})) +_{𝑓} (G) (\sum_{G}, ({H ↾}_{z}))))$
81	46 80	eleqtrrd	$⊢ φ \to X \underset{˙}{+} Y \in (G tsums (F {\underset{˙}{+}}_{f} H))$

Metamath Proof Explorer

Theorem tsmsadd

Proof