tsmsmhm

Description: Apply a continuous group homomorphism to an infinite group sum. (Contributed by Mario Carneiro, 18-Sep-2015)

	Ref	Expression
Hypotheses	tsmsmhm.b	$⊢ B = {Base}_{G}$
	tsmsmhm.j	$⊢ J = TopOpen (G)$
	tsmsmhm.k	$⊢ K = TopOpen (H)$
	tsmsmhm.1	$⊢ φ \to G \in CMnd$
	tsmsmhm.2	$⊢ φ \to G \in TopSp$
	tsmsmhm.3	$⊢ φ \to H \in CMnd$
	tsmsmhm.4	$⊢ φ \to H \in TopSp$
	tsmsmhm.5	$⊢ φ \to C \in (G MndHom H)$
	tsmsmhm.6	$⊢ φ \to C \in (J Cn K)$
	tsmsmhm.a	$⊢ φ \to A \in V$
	tsmsmhm.f	$⊢ φ \to F : A ⟶ B$
	tsmsmhm.x	$⊢ φ \to X \in (G tsums F)$
Assertion	tsmsmhm	$⊢ φ \to C (X) \in (H tsums (C \circ F))$

Proof

Step	Hyp	Ref	Expression
1		tsmsmhm.b	$⊢ B = {Base}_{G}$
2		tsmsmhm.j	$⊢ J = TopOpen (G)$
3		tsmsmhm.k	$⊢ K = TopOpen (H)$
4		tsmsmhm.1	$⊢ φ \to G \in CMnd$
5		tsmsmhm.2	$⊢ φ \to G \in TopSp$
6		tsmsmhm.3	$⊢ φ \to H \in CMnd$
7		tsmsmhm.4	$⊢ φ \to H \in TopSp$
8		tsmsmhm.5	$⊢ φ \to C \in (G MndHom H)$
9		tsmsmhm.6	$⊢ φ \to C \in (J Cn K)$
10		tsmsmhm.a	$⊢ φ \to A \in V$
11		tsmsmhm.f	$⊢ φ \to F : A ⟶ B$
12		tsmsmhm.x	$⊢ φ \to X \in (G tsums F)$
13	1 2	istps	$⊢ G \in TopSp \leftrightarrow J \in TopOn (B)$
14	5 13	sylib	$⊢ φ \to J \in TopOn (B)$
15		eqid	$⊢ 𝒫 A \cap Fin = 𝒫 A \cap Fin$
16		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\})$
17		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\})$
18	15 16 17 10	tsmsfbas	$⊢ φ \to ran (y \in (𝒫 A \cap Fin) ⟼ \{z \in (𝒫 A \cap Fin) \| y \subseteq z\}) \in fBas (𝒫 A \cap Fin)$
19		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)$
20	18 19	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)$
21	1 15 4 10 11	tsmslem1	$⊢ (φ \land z \in (𝒫 A \cap Fin)) \to \sum_{G} ({F ↾}_{z}) \in B$
22	21	fmpttd	$⊢ φ \to (z \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{z})) : 𝒫 A \cap Fin ⟶ B$
23	1 2 15 17 5 10 11	tsmsval	$⊢ φ \to G tsums F = (J 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})))$
24	12 23	eleqtrd	$⊢ φ \to X \in (J 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})))$
25	1 4 5 10 11	tsmscl	$⊢ φ \to G tsums F \subseteq B$
26	25 12	sseldd	$⊢ φ \to X \in B$
27		toponuni	$⊢ J \in TopOn (B) \to B = ⋃ J$
28	14 27	syl	$⊢ φ \to B = ⋃ J$
29	26 28	eleqtrd	$⊢ φ \to X \in ⋃ J$
30		eqid	$⊢ ⋃ J = ⋃ J$
31	30	cncnpi	$⊢ (C \in (J Cn K) \land X \in ⋃ J) \to C \in (J CnP K) (X)$
32	9 29 31	syl2anc	$⊢ φ \to C \in (J CnP K) (X)$
33		flfcnp	$⊢ ((J \in TopOn (B) \land (𝒫 A \cap Fin) filGen ran (y \in (𝒫 A \cap Fin) ⟼ \{z \in (𝒫 A \cap Fin) \| y \subseteq z\}) \in Fil (𝒫 A \cap Fin) \land (z \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{z})) : 𝒫 A \cap Fin ⟶ B) \land (X \in (J 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}))) \land C \in (J CnP K) (X))) \to C (X) \in (K fLimf ((𝒫 A \cap Fin) filGen ran (y \in (𝒫 A \cap Fin) ⟼ \{z \in (𝒫 A \cap Fin) \| y \subseteq z\}))) (C \circ (z \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{z})))$
34	14 20 22 24 32 33	syl32anc	$⊢ φ \to C (X) \in (K fLimf ((𝒫 A \cap Fin) filGen ran (y \in (𝒫 A \cap Fin) ⟼ \{z \in (𝒫 A \cap Fin) \| y \subseteq z\}))) (C \circ (z \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{z})))$
35		eqid	$⊢ {Base}_{H} = {Base}_{H}$
36	35 3	istps	$⊢ H \in TopSp \leftrightarrow K \in TopOn ({Base}_{H})$
37	7 36	sylib	$⊢ φ \to K \in TopOn ({Base}_{H})$
38		cnf2	$⊢ (J \in TopOn (B) \land K \in TopOn ({Base}_{H}) \land C \in (J Cn K)) \to C : B ⟶ {Base}_{H}$
39	14 37 9 38	syl3anc	$⊢ φ \to C : B ⟶ {Base}_{H}$
40		fco	$⊢ (C : B ⟶ {Base}_{H} \land F : A ⟶ B) \to (C \circ F) : A ⟶ {Base}_{H}$
41	39 11 40	syl2anc	$⊢ φ \to (C \circ F) : A ⟶ {Base}_{H}$
42	35 3 15 17 6 10 41	tsmsval	$⊢ φ \to H tsums (C \circ F) = (K 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_{H} ({(C \circ F) ↾}_{z})))$
43	39 21	cofmpt	$⊢ φ \to C \circ (z \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{z})) = (z \in (𝒫 A \cap Fin) ⟼ C (\sum_{G} ({F ↾}_{z})))$
44		resco	$⊢ {(C \circ F) ↾}_{z} = C \circ ({F ↾}_{z})$
45	44	oveq2i	$⊢ \sum_{H} ({(C \circ F) ↾}_{z}) = \sum_{H} (C \circ ({F ↾}_{z}))$
46		eqid	$⊢ 0_{G} = 0_{G}$
47	4	adantr	$⊢ (φ \land z \in (𝒫 A \cap Fin)) \to G \in CMnd$
48	6	adantr	$⊢ (φ \land z \in (𝒫 A \cap Fin)) \to H \in CMnd$
49		cmnmnd	$⊢ H \in CMnd \to H \in Mnd$
50	48 49	syl	$⊢ (φ \land z \in (𝒫 A \cap Fin)) \to H \in Mnd$
51		elinel2	$⊢ z \in (𝒫 A \cap Fin) \to z \in Fin$
52	51	adantl	$⊢ (φ \land z \in (𝒫 A \cap Fin)) \to z \in Fin$
53	8	adantr	$⊢ (φ \land z \in (𝒫 A \cap Fin)) \to C \in (G MndHom H)$
54		elfpw	$⊢ z \in (𝒫 A \cap Fin) \leftrightarrow (z \subseteq A \land z \in Fin)$
55	54	simplbi	$⊢ z \in (𝒫 A \cap Fin) \to z \subseteq A$
56		fssres	$⊢ (F : A ⟶ B \land z \subseteq A) \to ({F ↾}_{z}) : z ⟶ B$
57	11 55 56	syl2an	$⊢ (φ \land z \in (𝒫 A \cap Fin)) \to ({F ↾}_{z}) : z ⟶ B$
58		fvexd	$⊢ (φ \land z \in (𝒫 A \cap Fin)) \to 0_{G} \in V$
59	57 52 58	fdmfifsupp	$⊢ (φ \land z \in (𝒫 A \cap Fin)) \to {finSupp}_{0_{G}} (({F ↾}_{z}))$
60	1 46 47 50 52 53 57 59	gsummhm	$⊢ (φ \land z \in (𝒫 A \cap Fin)) \to \sum_{H} (C \circ ({F ↾}_{z})) = C (\sum_{G} ({F ↾}_{z}))$
61	45 60	eqtrid	$⊢ (φ \land z \in (𝒫 A \cap Fin)) \to \sum_{H} ({(C \circ F) ↾}_{z}) = C (\sum_{G} ({F ↾}_{z}))$
62	61	mpteq2dva	$⊢ φ \to (z \in (𝒫 A \cap Fin) ⟼ \sum_{H} ({(C \circ F) ↾}_{z})) = (z \in (𝒫 A \cap Fin) ⟼ C (\sum_{G} ({F ↾}_{z})))$
63	43 62	eqtr4d	$⊢ φ \to C \circ (z \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{z})) = (z \in (𝒫 A \cap Fin) ⟼ \sum_{H} ({(C \circ F) ↾}_{z}))$
64	63	fveq2d	$⊢ φ \to (K fLimf ((𝒫 A \cap Fin) filGen ran (y \in (𝒫 A \cap Fin) ⟼ \{z \in (𝒫 A \cap Fin) \| y \subseteq z\}))) (C \circ (z \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{z}))) = (K 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_{H} ({(C \circ F) ↾}_{z})))$
65	42 64	eqtr4d	$⊢ φ \to H tsums (C \circ F) = (K fLimf ((𝒫 A \cap Fin) filGen ran (y \in (𝒫 A \cap Fin) ⟼ \{z \in (𝒫 A \cap Fin) \| y \subseteq z\}))) (C \circ (z \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{z})))$
66	34 65	eleqtrrd	$⊢ φ \to C (X) \in (H tsums (C \circ F))$

Metamath Proof Explorer

Theorem tsmsmhm

Proof