tgptsmscls

Description: A sum in a topological group is uniquely determined up to a coset of cls ( { 0 } ) , which is a normal subgroup by clsnsg , 0nsg . (Contributed by Mario Carneiro, 22-Sep-2015) (Proof shortened by AV, 24-Jul-2019)

	Ref	Expression
Hypotheses	tgptsmscls.b	$⊢ B = {Base}_{G}$
	tgptsmscls.j	$⊢ J = TopOpen (G)$
	tgptsmscls.1	$⊢ φ \to G \in CMnd$
	tgptsmscls.2	$⊢ φ \to G \in TopGrp$
	tgptsmscls.a	$⊢ φ \to A \in V$
	tgptsmscls.f	$⊢ φ \to F : A ⟶ B$
	tgptsmscls.x	$⊢ φ \to X \in (G tsums F)$
Assertion	tgptsmscls	$⊢ φ \to G tsums F = cls (J) (\{X\})$

Proof

Step	Hyp	Ref	Expression
1		tgptsmscls.b	$⊢ B = {Base}_{G}$
2		tgptsmscls.j	$⊢ J = TopOpen (G)$
3		tgptsmscls.1	$⊢ φ \to G \in CMnd$
4		tgptsmscls.2	$⊢ φ \to G \in TopGrp$
5		tgptsmscls.a	$⊢ φ \to A \in V$
6		tgptsmscls.f	$⊢ φ \to F : A ⟶ B$
7		tgptsmscls.x	$⊢ φ \to X \in (G tsums F)$
8	4	adantr	$⊢ (φ \land x \in (G tsums F)) \to G \in TopGrp$
9		tgpgrp	$⊢ G \in TopGrp \to G \in Grp$
10	8 9	syl	$⊢ (φ \land x \in (G tsums F)) \to G \in Grp$
11		eqid	$⊢ 0_{G} = 0_{G}$
12	11	0subg	$⊢ G \in Grp \to \{0_{G}\} \in SubGrp (G)$
13	10 12	syl	$⊢ (φ \land x \in (G tsums F)) \to \{0_{G}\} \in SubGrp (G)$
14	2	clssubg	$⊢ (G \in TopGrp \land \{0_{G}\} \in SubGrp (G)) \to cls (J) (\{0_{G}\}) \in SubGrp (G)$
15	8 13 14	syl2anc	$⊢ (φ \land x \in (G tsums F)) \to cls (J) (\{0_{G}\}) \in SubGrp (G)$
16		eqid	$⊢ G ~_{QG} cls (J) (\{0_{G}\}) = G ~_{QG} cls (J) (\{0_{G}\})$
17	1 16	eqger	$⊢ cls (J) (\{0_{G}\}) \in SubGrp (G) \to (G ~_{QG} cls (J) (\{0_{G}\})) Er B$
18	15 17	syl	$⊢ (φ \land x \in (G tsums F)) \to (G ~_{QG} cls (J) (\{0_{G}\})) Er B$
19		tgptps	$⊢ G \in TopGrp \to G \in TopSp$
20	4 19	syl	$⊢ φ \to G \in TopSp$
21	1 3 20 5 6	tsmscl	$⊢ φ \to G tsums F \subseteq B$
22	21	sselda	$⊢ (φ \land x \in (G tsums F)) \to x \in B$
23	21 7	sseldd	$⊢ φ \to X \in B$
24	23	adantr	$⊢ (φ \land x \in (G tsums F)) \to X \in B$
25		eqid	$⊢ -_{G} = -_{G}$
26	3	adantr	$⊢ (φ \land x \in (G tsums F)) \to G \in CMnd$
27	5	adantr	$⊢ (φ \land x \in (G tsums F)) \to A \in V$
28	6	adantr	$⊢ (φ \land x \in (G tsums F)) \to F : A ⟶ B$
29	7	adantr	$⊢ (φ \land x \in (G tsums F)) \to X \in (G tsums F)$
30		simpr	$⊢ (φ \land x \in (G tsums F)) \to x \in (G tsums F)$
31	1 25 26 8 27 28 28 29 30	tsmssub	$⊢ (φ \land x \in (G tsums F)) \to X -_{G} x \in (G tsums (F {-_{G}}_{f} F))$
32	28	ffvelrnda	$⊢ ((φ \land x \in (G tsums F)) \land k \in A) \to F (k) \in B$
33	28	feqmptd	$⊢ (φ \land x \in (G tsums F)) \to F = (k \in A ⟼ F (k))$
34	27 32 32 33 33	offval2	$⊢ (φ \land x \in (G tsums F)) \to F {-_{G}}_{f} F = (k \in A ⟼ F (k) -_{G} F (k))$
35	10	adantr	$⊢ ((φ \land x \in (G tsums F)) \land k \in A) \to G \in Grp$
36	1 11 25	grpsubid	$⊢ (G \in Grp \land F (k) \in B) \to F (k) -_{G} F (k) = 0_{G}$
37	35 32 36	syl2anc	$⊢ ((φ \land x \in (G tsums F)) \land k \in A) \to F (k) -_{G} F (k) = 0_{G}$
38	37	mpteq2dva	$⊢ (φ \land x \in (G tsums F)) \to (k \in A ⟼ F (k) -_{G} F (k)) = (k \in A ⟼ 0_{G})$
39	34 38	eqtrd	$⊢ (φ \land x \in (G tsums F)) \to F {-_{G}}_{f} F = (k \in A ⟼ 0_{G})$
40	39	oveq2d	$⊢ (φ \land x \in (G tsums F)) \to G tsums (F {-_{G}}_{f} F) = G tsums (k \in A ⟼ 0_{G})$
41	8 19	syl	$⊢ (φ \land x \in (G tsums F)) \to G \in TopSp$
42	1 11	grpidcl	$⊢ G \in Grp \to 0_{G} \in B$
43	10 42	syl	$⊢ (φ \land x \in (G tsums F)) \to 0_{G} \in B$
44	43	adantr	$⊢ ((φ \land x \in (G tsums F)) \land k \in A) \to 0_{G} \in B$
45	44	fmpttd	$⊢ (φ \land x \in (G tsums F)) \to (k \in A ⟼ 0_{G}) : A ⟶ B$
46		fconstmpt	$⊢ A \times \{0_{G}\} = (k \in A ⟼ 0_{G})$
47		fvexd	$⊢ φ \to 0_{G} \in V$
48	5 47	fczfsuppd	$⊢ φ \to {finSupp}_{0_{G}} ((A \times \{0_{G}\}))$
49	48	adantr	$⊢ (φ \land x \in (G tsums F)) \to {finSupp}_{0_{G}} ((A \times \{0_{G}\}))$
50	46 49	eqbrtrrid	$⊢ (φ \land x \in (G tsums F)) \to {finSupp}_{0_{G}} ((k \in A ⟼ 0_{G}))$
51	1 11 26 41 27 45 50 2	tsmsgsum	$⊢ (φ \land x \in (G tsums F)) \to G tsums (k \in A ⟼ 0_{G}) = cls (J) (\{\underset{k \in A}{\sum_{G}} 0_{G}\})$
52		cmnmnd	$⊢ G \in CMnd \to G \in Mnd$
53	26 52	syl	$⊢ (φ \land x \in (G tsums F)) \to G \in Mnd$
54	11	gsumz	$⊢ (G \in Mnd \land A \in V) \to \underset{k \in A}{\sum_{G}} 0_{G} = 0_{G}$
55	53 27 54	syl2anc	$⊢ (φ \land x \in (G tsums F)) \to \underset{k \in A}{\sum_{G}} 0_{G} = 0_{G}$
56	55	sneqd	$⊢ (φ \land x \in (G tsums F)) \to \{\underset{k \in A}{\sum_{G}} 0_{G}\} = \{0_{G}\}$
57	56	fveq2d	$⊢ (φ \land x \in (G tsums F)) \to cls (J) (\{\underset{k \in A}{\sum_{G}} 0_{G}\}) = cls (J) (\{0_{G}\})$
58	40 51 57	3eqtrd	$⊢ (φ \land x \in (G tsums F)) \to G tsums (F {-_{G}}_{f} F) = cls (J) (\{0_{G}\})$
59	31 58	eleqtrd	$⊢ (φ \land x \in (G tsums F)) \to X -_{G} x \in cls (J) (\{0_{G}\})$
60		isabl	$⊢ G \in Abel \leftrightarrow (G \in Grp \land G \in CMnd)$
61	10 26 60	sylanbrc	$⊢ (φ \land x \in (G tsums F)) \to G \in Abel$
62	1	subgss	$⊢ cls (J) (\{0_{G}\}) \in SubGrp (G) \to cls (J) (\{0_{G}\}) \subseteq B$
63	15 62	syl	$⊢ (φ \land x \in (G tsums F)) \to cls (J) (\{0_{G}\}) \subseteq B$
64	1 25 16	eqgabl	$⊢ (G \in Abel \land cls (J) (\{0_{G}\}) \subseteq B) \to (x (G ~_{QG} cls (J) (\{0_{G}\})) X \leftrightarrow (x \in B \land X \in B \land X -_{G} x \in cls (J) (\{0_{G}\})))$
65	61 63 64	syl2anc	$⊢ (φ \land x \in (G tsums F)) \to (x (G ~_{QG} cls (J) (\{0_{G}\})) X \leftrightarrow (x \in B \land X \in B \land X -_{G} x \in cls (J) (\{0_{G}\})))$
66	22 24 59 65	mpbir3and	$⊢ (φ \land x \in (G tsums F)) \to x (G ~_{QG} cls (J) (\{0_{G}\})) X$
67	18 66	ersym	$⊢ (φ \land x \in (G tsums F)) \to X (G ~_{QG} cls (J) (\{0_{G}\})) x$
68	16	releqg	$⊢ Rel (G ~_{QG} cls (J) (\{0_{G}\}))$
69		relelec	$⊢ Rel (G ~_{QG} cls (J) (\{0_{G}\})) \to (x \in [X] (G ~_{QG} cls (J) (\{0_{G}\})) \leftrightarrow X (G ~_{QG} cls (J) (\{0_{G}\})) x)$
70	68 69	ax-mp	$⊢ x \in [X] (G ~_{QG} cls (J) (\{0_{G}\})) \leftrightarrow X (G ~_{QG} cls (J) (\{0_{G}\})) x$
71	67 70	sylibr	$⊢ (φ \land x \in (G tsums F)) \to x \in [X] (G ~_{QG} cls (J) (\{0_{G}\}))$
72		eqid	$⊢ cls (J) (\{0_{G}\}) = cls (J) (\{0_{G}\})$
73	1 2 11 16 72	snclseqg	$⊢ (G \in TopGrp \land X \in B) \to [X] (G ~_{QG} cls (J) (\{0_{G}\})) = cls (J) (\{X\})$
74	8 24 73	syl2anc	$⊢ (φ \land x \in (G tsums F)) \to [X] (G ~_{QG} cls (J) (\{0_{G}\})) = cls (J) (\{X\})$
75	71 74	eleqtrd	$⊢ (φ \land x \in (G tsums F)) \to x \in cls (J) (\{X\})$
76	75	ex	$⊢ φ \to (x \in (G tsums F) \to x \in cls (J) (\{X\}))$
77	76	ssrdv	$⊢ φ \to G tsums F \subseteq cls (J) (\{X\})$
78	1 2 3 20 5 6 7	tsmscls	$⊢ φ \to cls (J) (\{X\}) \subseteq G tsums F$
79	77 78	eqssd	$⊢ φ \to G tsums F = cls (J) (\{X\})$

Metamath Proof Explorer

Theorem tgptsmscls

Proof