tsmssplit

Description: Split a topological group sum into two parts. (Contributed by Mario Carneiro, 19-Sep-2015) (Proof shortened by AV, 24-Jul-2019)

	Ref	Expression
Hypotheses	tsmssplit.b	$⊢ B = {Base}_{G}$
	tsmssplit.p	$⊢ \underset{˙}{+} = +_{G}$
	tsmssplit.1	$⊢ φ \to G \in CMnd$
	tsmssplit.2	$⊢ φ \to G \in TopMnd$
	tsmssplit.a	$⊢ φ \to A \in V$
	tsmssplit.f	$⊢ φ \to F : A ⟶ B$
	tsmssplit.x	$⊢ φ \to X \in (G tsums ({F ↾}_{C}))$
	tsmssplit.y	$⊢ φ \to Y \in (G tsums ({F ↾}_{D}))$
	tsmssplit.i	$⊢ φ \to C \cap D = \emptyset$
	tsmssplit.u	$⊢ φ \to A = C \cup D$
Assertion	tsmssplit	$⊢ φ \to X \underset{˙}{+} Y \in (G tsums F)$

Proof

Step	Hyp	Ref	Expression
1		tsmssplit.b	$⊢ B = {Base}_{G}$
2		tsmssplit.p	$⊢ \underset{˙}{+} = +_{G}$
3		tsmssplit.1	$⊢ φ \to G \in CMnd$
4		tsmssplit.2	$⊢ φ \to G \in TopMnd$
5		tsmssplit.a	$⊢ φ \to A \in V$
6		tsmssplit.f	$⊢ φ \to F : A ⟶ B$
7		tsmssplit.x	$⊢ φ \to X \in (G tsums ({F ↾}_{C}))$
8		tsmssplit.y	$⊢ φ \to Y \in (G tsums ({F ↾}_{D}))$
9		tsmssplit.i	$⊢ φ \to C \cap D = \emptyset$
10		tsmssplit.u	$⊢ φ \to A = C \cup D$
11	6	ffvelcdmda	$⊢ (φ \land k \in A) \to F (k) \in B$
12		cmnmnd	$⊢ G \in CMnd \to G \in Mnd$
13	3 12	syl	$⊢ φ \to G \in Mnd$
14		eqid	$⊢ 0_{G} = 0_{G}$
15	1 14	mndidcl	$⊢ G \in Mnd \to 0_{G} \in B$
16	13 15	syl	$⊢ φ \to 0_{G} \in B$
17	16	adantr	$⊢ (φ \land k \in A) \to 0_{G} \in B$
18	11 17	ifcld	$⊢ (φ \land k \in A) \to if (k \in C, F (k), 0_{G}) \in B$
19	18	fmpttd	$⊢ φ \to (k \in A ⟼ if (k \in C, F (k), 0_{G})) : A ⟶ B$
20	11 17	ifcld	$⊢ (φ \land k \in A) \to if (k \in D, F (k), 0_{G}) \in B$
21	20	fmpttd	$⊢ φ \to (k \in A ⟼ if (k \in D, F (k), 0_{G})) : A ⟶ B$
22	6	feqmptd	$⊢ φ \to F = (k \in A ⟼ F (k))$
23	22	reseq1d	$⊢ φ \to {F ↾}_{C} = {(k \in A ⟼ F (k)) ↾}_{C}$
24		ssun1	$⊢ C \subseteq C \cup D$
25	24 10	sseqtrrid	$⊢ φ \to C \subseteq A$
26		iftrue	$⊢ k \in C \to if (k \in C, F (k), 0_{G}) = F (k)$
27	26	mpteq2ia	$⊢ (k \in C ⟼ if (k \in C, F (k), 0_{G})) = (k \in C ⟼ F (k))$
28		resmpt	$⊢ C \subseteq A \to {(k \in A ⟼ if (k \in C, F (k), 0_{G})) ↾}_{C} = (k \in C ⟼ if (k \in C, F (k), 0_{G}))$
29		resmpt	$⊢ C \subseteq A \to {(k \in A ⟼ F (k)) ↾}_{C} = (k \in C ⟼ F (k))$
30	27 28 29	3eqtr4a	$⊢ C \subseteq A \to {(k \in A ⟼ if (k \in C, F (k), 0_{G})) ↾}_{C} = {(k \in A ⟼ F (k)) ↾}_{C}$
31	25 30	syl	$⊢ φ \to {(k \in A ⟼ if (k \in C, F (k), 0_{G})) ↾}_{C} = {(k \in A ⟼ F (k)) ↾}_{C}$
32	23 31	eqtr4d	$⊢ φ \to {F ↾}_{C} = {(k \in A ⟼ if (k \in C, F (k), 0_{G})) ↾}_{C}$
33	32	oveq2d	$⊢ φ \to G tsums ({F ↾}_{C}) = G tsums ({(k \in A ⟼ if (k \in C, F (k), 0_{G})) ↾}_{C})$
34		tmdtps	$⊢ G \in TopMnd \to G \in TopSp$
35	4 34	syl	$⊢ φ \to G \in TopSp$
36		eldifn	$⊢ k \in (A ∖ C) \to \neg k \in C$
37	36	adantl	$⊢ (φ \land k \in (A ∖ C)) \to \neg k \in C$
38	37	iffalsed	$⊢ (φ \land k \in (A ∖ C)) \to if (k \in C, F (k), 0_{G}) = 0_{G}$
39	38 5	suppss2	$⊢ φ \to (k \in A ⟼ if (k \in C, F (k), 0_{G})) supp 0_{G} \subseteq C$
40	1 14 3 35 5 19 39	tsmsres	$⊢ φ \to G tsums ({(k \in A ⟼ if (k \in C, F (k), 0_{G})) ↾}_{C}) = G tsums (k \in A ⟼ if (k \in C, F (k), 0_{G}))$
41	33 40	eqtrd	$⊢ φ \to G tsums ({F ↾}_{C}) = G tsums (k \in A ⟼ if (k \in C, F (k), 0_{G}))$
42	7 41	eleqtrd	$⊢ φ \to X \in (G tsums (k \in A ⟼ if (k \in C, F (k), 0_{G})))$
43	22	reseq1d	$⊢ φ \to {F ↾}_{D} = {(k \in A ⟼ F (k)) ↾}_{D}$
44		ssun2	$⊢ D \subseteq C \cup D$
45	44 10	sseqtrrid	$⊢ φ \to D \subseteq A$
46		iftrue	$⊢ k \in D \to if (k \in D, F (k), 0_{G}) = F (k)$
47	46	mpteq2ia	$⊢ (k \in D ⟼ if (k \in D, F (k), 0_{G})) = (k \in D ⟼ F (k))$
48		resmpt	$⊢ D \subseteq A \to {(k \in A ⟼ if (k \in D, F (k), 0_{G})) ↾}_{D} = (k \in D ⟼ if (k \in D, F (k), 0_{G}))$
49		resmpt	$⊢ D \subseteq A \to {(k \in A ⟼ F (k)) ↾}_{D} = (k \in D ⟼ F (k))$
50	47 48 49	3eqtr4a	$⊢ D \subseteq A \to {(k \in A ⟼ if (k \in D, F (k), 0_{G})) ↾}_{D} = {(k \in A ⟼ F (k)) ↾}_{D}$
51	45 50	syl	$⊢ φ \to {(k \in A ⟼ if (k \in D, F (k), 0_{G})) ↾}_{D} = {(k \in A ⟼ F (k)) ↾}_{D}$
52	43 51	eqtr4d	$⊢ φ \to {F ↾}_{D} = {(k \in A ⟼ if (k \in D, F (k), 0_{G})) ↾}_{D}$
53	52	oveq2d	$⊢ φ \to G tsums ({F ↾}_{D}) = G tsums ({(k \in A ⟼ if (k \in D, F (k), 0_{G})) ↾}_{D})$
54		eldifn	$⊢ k \in (A ∖ D) \to \neg k \in D$
55	54	adantl	$⊢ (φ \land k \in (A ∖ D)) \to \neg k \in D$
56	55	iffalsed	$⊢ (φ \land k \in (A ∖ D)) \to if (k \in D, F (k), 0_{G}) = 0_{G}$
57	56 5	suppss2	$⊢ φ \to (k \in A ⟼ if (k \in D, F (k), 0_{G})) supp 0_{G} \subseteq D$
58	1 14 3 35 5 21 57	tsmsres	$⊢ φ \to G tsums ({(k \in A ⟼ if (k \in D, F (k), 0_{G})) ↾}_{D}) = G tsums (k \in A ⟼ if (k \in D, F (k), 0_{G}))$
59	53 58	eqtrd	$⊢ φ \to G tsums ({F ↾}_{D}) = G tsums (k \in A ⟼ if (k \in D, F (k), 0_{G}))$
60	8 59	eleqtrd	$⊢ φ \to Y \in (G tsums (k \in A ⟼ if (k \in D, F (k), 0_{G})))$
61	1 2 3 4 5 19 21 42 60	tsmsadd	$⊢ φ \to X \underset{˙}{+} Y \in (G tsums ((k \in A ⟼ if (k \in C, F (k), 0_{G})) {\underset{˙}{+}}_{f} (k \in A ⟼ if (k \in D, F (k), 0_{G}))))$
62	26	adantl	$⊢ ((φ \land k \in A) \land k \in C) \to if (k \in C, F (k), 0_{G}) = F (k)$
63		noel	$⊢ \neg k \in \emptyset$
64		eleq2	$⊢ C \cap D = \emptyset \to (k \in (C \cap D) \leftrightarrow k \in \emptyset)$
65	63 64	mtbiri	$⊢ C \cap D = \emptyset \to \neg k \in (C \cap D)$
66	9 65	syl	$⊢ φ \to \neg k \in (C \cap D)$
67	66	adantr	$⊢ (φ \land k \in A) \to \neg k \in (C \cap D)$
68		elin	$⊢ k \in (C \cap D) \leftrightarrow (k \in C \land k \in D)$
69	67 68	sylnib	$⊢ (φ \land k \in A) \to \neg (k \in C \land k \in D)$
70		imnan	$⊢ (k \in C \to \neg k \in D) \leftrightarrow \neg (k \in C \land k \in D)$
71	69 70	sylibr	$⊢ (φ \land k \in A) \to (k \in C \to \neg k \in D)$
72	71	imp	$⊢ ((φ \land k \in A) \land k \in C) \to \neg k \in D$
73	72	iffalsed	$⊢ ((φ \land k \in A) \land k \in C) \to if (k \in D, F (k), 0_{G}) = 0_{G}$
74	62 73	oveq12d	$⊢ ((φ \land k \in A) \land k \in C) \to if (k \in C, F (k), 0_{G}) \underset{˙}{+} if (k \in D, F (k), 0_{G}) = F (k) \underset{˙}{+} 0_{G}$
75	1 2 14	mndrid	$⊢ (G \in Mnd \land F (k) \in B) \to F (k) \underset{˙}{+} 0_{G} = F (k)$
76	13 11 75	syl2an2r	$⊢ (φ \land k \in A) \to F (k) \underset{˙}{+} 0_{G} = F (k)$
77	76	adantr	$⊢ ((φ \land k \in A) \land k \in C) \to F (k) \underset{˙}{+} 0_{G} = F (k)$
78	74 77	eqtrd	$⊢ ((φ \land k \in A) \land k \in C) \to if (k \in C, F (k), 0_{G}) \underset{˙}{+} if (k \in D, F (k), 0_{G}) = F (k)$
79	71	con2d	$⊢ (φ \land k \in A) \to (k \in D \to \neg k \in C)$
80	79	imp	$⊢ ((φ \land k \in A) \land k \in D) \to \neg k \in C$
81	80	iffalsed	$⊢ ((φ \land k \in A) \land k \in D) \to if (k \in C, F (k), 0_{G}) = 0_{G}$
82	46	adantl	$⊢ ((φ \land k \in A) \land k \in D) \to if (k \in D, F (k), 0_{G}) = F (k)$
83	81 82	oveq12d	$⊢ ((φ \land k \in A) \land k \in D) \to if (k \in C, F (k), 0_{G}) \underset{˙}{+} if (k \in D, F (k), 0_{G}) = 0_{G} \underset{˙}{+} F (k)$
84	1 2 14	mndlid	$⊢ (G \in Mnd \land F (k) \in B) \to 0_{G} \underset{˙}{+} F (k) = F (k)$
85	13 11 84	syl2an2r	$⊢ (φ \land k \in A) \to 0_{G} \underset{˙}{+} F (k) = F (k)$
86	85	adantr	$⊢ ((φ \land k \in A) \land k \in D) \to 0_{G} \underset{˙}{+} F (k) = F (k)$
87	83 86	eqtrd	$⊢ ((φ \land k \in A) \land k \in D) \to if (k \in C, F (k), 0_{G}) \underset{˙}{+} if (k \in D, F (k), 0_{G}) = F (k)$
88	10	eleq2d	$⊢ φ \to (k \in A \leftrightarrow k \in (C \cup D))$
89		elun	$⊢ k \in (C \cup D) \leftrightarrow (k \in C \lor k \in D)$
90	88 89	bitrdi	$⊢ φ \to (k \in A \leftrightarrow (k \in C \lor k \in D))$
91	90	biimpa	$⊢ (φ \land k \in A) \to (k \in C \lor k \in D)$
92	78 87 91	mpjaodan	$⊢ (φ \land k \in A) \to if (k \in C, F (k), 0_{G}) \underset{˙}{+} if (k \in D, F (k), 0_{G}) = F (k)$
93	92	mpteq2dva	$⊢ φ \to (k \in A ⟼ if (k \in C, F (k), 0_{G}) \underset{˙}{+} if (k \in D, F (k), 0_{G})) = (k \in A ⟼ F (k))$
94	22 93	eqtr4d	$⊢ φ \to F = (k \in A ⟼ if (k \in C, F (k), 0_{G}) \underset{˙}{+} if (k \in D, F (k), 0_{G}))$
95		eqidd	$⊢ φ \to (k \in A ⟼ if (k \in C, F (k), 0_{G})) = (k \in A ⟼ if (k \in C, F (k), 0_{G}))$
96		eqidd	$⊢ φ \to (k \in A ⟼ if (k \in D, F (k), 0_{G})) = (k \in A ⟼ if (k \in D, F (k), 0_{G}))$
97	5 18 20 95 96	offval2	$⊢ φ \to (k \in A ⟼ if (k \in C, F (k), 0_{G})) {\underset{˙}{+}}_{f} (k \in A ⟼ if (k \in D, F (k), 0_{G})) = (k \in A ⟼ if (k \in C, F (k), 0_{G}) \underset{˙}{+} if (k \in D, F (k), 0_{G}))$
98	94 97	eqtr4d	$⊢ φ \to F = (k \in A ⟼ if (k \in C, F (k), 0_{G})) {\underset{˙}{+}}_{f} (k \in A ⟼ if (k \in D, F (k), 0_{G}))$
99	98	oveq2d	$⊢ φ \to G tsums F = G tsums ((k \in A ⟼ if (k \in C, F (k), 0_{G})) {\underset{˙}{+}}_{f} (k \in A ⟼ if (k \in D, F (k), 0_{G})))$
100	61 99	eleqtrrd	$⊢ φ \to X \underset{˙}{+} Y \in (G tsums F)$

Metamath Proof Explorer

Theorem tsmssplit

Proof