gsumzsplit

Description: Split a group sum into two parts. (Contributed by Mario Carneiro, 25-Apr-2016) (Revised by AV, 5-Jun-2019)

	Ref	Expression
Hypotheses	gsumzsplit.b	$⊢ B = {Base}_{G}$
	gsumzsplit.0	$⊢ \underset{˙}{0} = 0_{G}$
	gsumzsplit.p	$⊢ \underset{˙}{+} = +_{G}$
	gsumzsplit.z	$⊢ Z = Cntz (G)$
	gsumzsplit.g	$⊢ φ \to G \in Mnd$
	gsumzsplit.a	$⊢ φ \to A \in V$
	gsumzsplit.f	$⊢ φ \to F : A ⟶ B$
	gsumzsplit.c	$⊢ φ \to ran F \subseteq Z (ran F)$
	gsumzsplit.w	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (F)$
	gsumzsplit.i	$⊢ φ \to C \cap D = \emptyset$
	gsumzsplit.u	$⊢ φ \to A = C \cup D$
Assertion	gsumzsplit	$⊢ φ \to \sum_{G} F = (\sum_{G}, ({F ↾}_{C})) \underset{˙}{+} (\sum_{G}, ({F ↾}_{D}))$

Proof

Step	Hyp	Ref	Expression
1		gsumzsplit.b	$⊢ B = {Base}_{G}$
2		gsumzsplit.0	$⊢ \underset{˙}{0} = 0_{G}$
3		gsumzsplit.p	$⊢ \underset{˙}{+} = +_{G}$
4		gsumzsplit.z	$⊢ Z = Cntz (G)$
5		gsumzsplit.g	$⊢ φ \to G \in Mnd$
6		gsumzsplit.a	$⊢ φ \to A \in V$
7		gsumzsplit.f	$⊢ φ \to F : A ⟶ B$
8		gsumzsplit.c	$⊢ φ \to ran F \subseteq Z (ran F)$
9		gsumzsplit.w	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (F)$
10		gsumzsplit.i	$⊢ φ \to C \cap D = \emptyset$
11		gsumzsplit.u	$⊢ φ \to A = C \cup D$
12	2	fvexi	$⊢ \underset{˙}{0} \in V$
13	12	a1i	$⊢ φ \to \underset{˙}{0} \in V$
14	7 6 13 9	fsuppmptif	$⊢ φ \to {finSupp}_{\underset{˙}{0}} ((k \in A ⟼ if (k \in C, F (k), \underset{˙}{0})))$
15	7 6 13 9	fsuppmptif	$⊢ φ \to {finSupp}_{\underset{˙}{0}} ((k \in A ⟼ if (k \in D, F (k), \underset{˙}{0})))$
16	1	submacs	$⊢ G \in Mnd \to SubMnd (G) \in ACS (B)$
17		acsmre	$⊢ SubMnd (G) \in ACS (B) \to SubMnd (G) \in Moore (B)$
18	5 16 17	3syl	$⊢ φ \to SubMnd (G) \in Moore (B)$
19	7	frnd	$⊢ φ \to ran F \subseteq B$
20		eqid	$⊢ mrCls (SubMnd (G)) = mrCls (SubMnd (G))$
21	20	mrccl	$⊢ (SubMnd (G) \in Moore (B) \land ran F \subseteq B) \to mrCls (SubMnd (G)) (ran F) \in SubMnd (G)$
22	18 19 21	syl2anc	$⊢ φ \to mrCls (SubMnd (G)) (ran F) \in SubMnd (G)$
23		eqid	$⊢ G ↾_{𝑠} mrCls (SubMnd (G)) (ran F) = G ↾_{𝑠} mrCls (SubMnd (G)) (ran F)$
24	4 20 23	cntzspan	$⊢ (G \in Mnd \land ran F \subseteq Z (ran F)) \to G ↾_{𝑠} mrCls (SubMnd (G)) (ran F) \in CMnd$
25	5 8 24	syl2anc	$⊢ φ \to G ↾_{𝑠} mrCls (SubMnd (G)) (ran F) \in CMnd$
26	23 4	submcmn2	$⊢ mrCls (SubMnd (G)) (ran F) \in SubMnd (G) \to (G ↾_{𝑠} mrCls (SubMnd (G)) (ran F) \in CMnd \leftrightarrow mrCls (SubMnd (G)) (ran F) \subseteq Z (mrCls (SubMnd (G)) (ran F)))$
27	22 26	syl	$⊢ φ \to (G ↾_{𝑠} mrCls (SubMnd (G)) (ran F) \in CMnd \leftrightarrow mrCls (SubMnd (G)) (ran F) \subseteq Z (mrCls (SubMnd (G)) (ran F)))$
28	25 27	mpbid	$⊢ φ \to mrCls (SubMnd (G)) (ran F) \subseteq Z (mrCls (SubMnd (G)) (ran F))$
29	18 20 19	mrcssidd	$⊢ φ \to ran F \subseteq mrCls (SubMnd (G)) (ran F)$
30	29	adantr	$⊢ (φ \land k \in A) \to ran F \subseteq mrCls (SubMnd (G)) (ran F)$
31	7	ffnd	$⊢ φ \to F Fn A$
32		fnfvelrn	$⊢ (F Fn A \land k \in A) \to F (k) \in ran F$
33	31 32	sylan	$⊢ (φ \land k \in A) \to F (k) \in ran F$
34	30 33	sseldd	$⊢ (φ \land k \in A) \to F (k) \in mrCls (SubMnd (G)) (ran F)$
35	2	subm0cl	$⊢ mrCls (SubMnd (G)) (ran F) \in SubMnd (G) \to \underset{˙}{0} \in mrCls (SubMnd (G)) (ran F)$
36	22 35	syl	$⊢ φ \to \underset{˙}{0} \in mrCls (SubMnd (G)) (ran F)$
37	36	adantr	$⊢ (φ \land k \in A) \to \underset{˙}{0} \in mrCls (SubMnd (G)) (ran F)$
38	34 37	ifcld	$⊢ (φ \land k \in A) \to if (k \in C, F (k), \underset{˙}{0}) \in mrCls (SubMnd (G)) (ran F)$
39	38	fmpttd	$⊢ φ \to (k \in A ⟼ if (k \in C, F (k), \underset{˙}{0})) : A ⟶ mrCls (SubMnd (G)) (ran F)$
40	34 37	ifcld	$⊢ (φ \land k \in A) \to if (k \in D, F (k), \underset{˙}{0}) \in mrCls (SubMnd (G)) (ran F)$
41	40	fmpttd	$⊢ φ \to (k \in A ⟼ if (k \in D, F (k), \underset{˙}{0})) : A ⟶ mrCls (SubMnd (G)) (ran F)$
42	1 2 3 4 5 6 14 15 22 28 39 41	gsumzadd	$⊢ φ \to \sum_{G} ((k \in A ⟼ if (k \in C, F (k), \underset{˙}{0})) {\underset{˙}{+}}_{f} (k \in A ⟼ if (k \in D, F (k), \underset{˙}{0}))) = (\underset{k \in A}{\sum_{G}}, if (k \in C, F (k), \underset{˙}{0})) \underset{˙}{+} (\underset{k \in A}{\sum_{G}}, if (k \in D, F (k), \underset{˙}{0}))$
43	7	feqmptd	$⊢ φ \to F = (k \in A ⟼ F (k))$
44		iftrue	$⊢ k \in C \to if (k \in C, F (k), \underset{˙}{0}) = F (k)$
45	44	adantl	$⊢ ((φ \land k \in A) \land k \in C) \to if (k \in C, F (k), \underset{˙}{0}) = F (k)$
46		noel	$⊢ \neg k \in \emptyset$
47		eleq2	$⊢ C \cap D = \emptyset \to (k \in (C \cap D) \leftrightarrow k \in \emptyset)$
48	46 47	mtbiri	$⊢ C \cap D = \emptyset \to \neg k \in (C \cap D)$
49	10 48	syl	$⊢ φ \to \neg k \in (C \cap D)$
50	49	adantr	$⊢ (φ \land k \in A) \to \neg k \in (C \cap D)$
51		elin	$⊢ k \in (C \cap D) \leftrightarrow (k \in C \land k \in D)$
52	50 51	sylnib	$⊢ (φ \land k \in A) \to \neg (k \in C \land k \in D)$
53		imnan	$⊢ (k \in C \to \neg k \in D) \leftrightarrow \neg (k \in C \land k \in D)$
54	52 53	sylibr	$⊢ (φ \land k \in A) \to (k \in C \to \neg k \in D)$
55	54	imp	$⊢ ((φ \land k \in A) \land k \in C) \to \neg k \in D$
56	55	iffalsed	$⊢ ((φ \land k \in A) \land k \in C) \to if (k \in D, F (k), \underset{˙}{0}) = \underset{˙}{0}$
57	45 56	oveq12d	$⊢ ((φ \land k \in A) \land k \in C) \to if (k \in C, F (k), \underset{˙}{0}) \underset{˙}{+} if (k \in D, F (k), \underset{˙}{0}) = F (k) \underset{˙}{+} \underset{˙}{0}$
58	7	ffvelrnda	$⊢ (φ \land k \in A) \to F (k) \in B$
59	1 3 2	mndrid	$⊢ (G \in Mnd \land F (k) \in B) \to F (k) \underset{˙}{+} \underset{˙}{0} = F (k)$
60	5 58 59	syl2an2r	$⊢ (φ \land k \in A) \to F (k) \underset{˙}{+} \underset{˙}{0} = F (k)$
61	60	adantr	$⊢ ((φ \land k \in A) \land k \in C) \to F (k) \underset{˙}{+} \underset{˙}{0} = F (k)$
62	57 61	eqtrd	$⊢ ((φ \land k \in A) \land k \in C) \to if (k \in C, F (k), \underset{˙}{0}) \underset{˙}{+} if (k \in D, F (k), \underset{˙}{0}) = F (k)$
63	54	con2d	$⊢ (φ \land k \in A) \to (k \in D \to \neg k \in C)$
64	63	imp	$⊢ ((φ \land k \in A) \land k \in D) \to \neg k \in C$
65	64	iffalsed	$⊢ ((φ \land k \in A) \land k \in D) \to if (k \in C, F (k), \underset{˙}{0}) = \underset{˙}{0}$
66		iftrue	$⊢ k \in D \to if (k \in D, F (k), \underset{˙}{0}) = F (k)$
67	66	adantl	$⊢ ((φ \land k \in A) \land k \in D) \to if (k \in D, F (k), \underset{˙}{0}) = F (k)$
68	65 67	oveq12d	$⊢ ((φ \land k \in A) \land k \in D) \to if (k \in C, F (k), \underset{˙}{0}) \underset{˙}{+} if (k \in D, F (k), \underset{˙}{0}) = \underset{˙}{0} \underset{˙}{+} F (k)$
69	1 3 2	mndlid	$⊢ (G \in Mnd \land F (k) \in B) \to \underset{˙}{0} \underset{˙}{+} F (k) = F (k)$
70	5 58 69	syl2an2r	$⊢ (φ \land k \in A) \to \underset{˙}{0} \underset{˙}{+} F (k) = F (k)$
71	70	adantr	$⊢ ((φ \land k \in A) \land k \in D) \to \underset{˙}{0} \underset{˙}{+} F (k) = F (k)$
72	68 71	eqtrd	$⊢ ((φ \land k \in A) \land k \in D) \to if (k \in C, F (k), \underset{˙}{0}) \underset{˙}{+} if (k \in D, F (k), \underset{˙}{0}) = F (k)$
73	11	eleq2d	$⊢ φ \to (k \in A \leftrightarrow k \in (C \cup D))$
74		elun	$⊢ k \in (C \cup D) \leftrightarrow (k \in C \lor k \in D)$
75	73 74	syl6bb	$⊢ φ \to (k \in A \leftrightarrow (k \in C \lor k \in D))$
76	75	biimpa	$⊢ (φ \land k \in A) \to (k \in C \lor k \in D)$
77	62 72 76	mpjaodan	$⊢ (φ \land k \in A) \to if (k \in C, F (k), \underset{˙}{0}) \underset{˙}{+} if (k \in D, F (k), \underset{˙}{0}) = F (k)$
78	77	mpteq2dva	$⊢ φ \to (k \in A ⟼ if (k \in C, F (k), \underset{˙}{0}) \underset{˙}{+} if (k \in D, F (k), \underset{˙}{0})) = (k \in A ⟼ F (k))$
79	43 78	eqtr4d	$⊢ φ \to F = (k \in A ⟼ if (k \in C, F (k), \underset{˙}{0}) \underset{˙}{+} if (k \in D, F (k), \underset{˙}{0}))$
80	1 2	mndidcl	$⊢ G \in Mnd \to \underset{˙}{0} \in B$
81	5 80	syl	$⊢ φ \to \underset{˙}{0} \in B$
82	81	adantr	$⊢ (φ \land k \in A) \to \underset{˙}{0} \in B$
83	58 82	ifcld	$⊢ (φ \land k \in A) \to if (k \in C, F (k), \underset{˙}{0}) \in B$
84	58 82	ifcld	$⊢ (φ \land k \in A) \to if (k \in D, F (k), \underset{˙}{0}) \in B$
85		eqidd	$⊢ φ \to (k \in A ⟼ if (k \in C, F (k), \underset{˙}{0})) = (k \in A ⟼ if (k \in C, F (k), \underset{˙}{0}))$
86		eqidd	$⊢ φ \to (k \in A ⟼ if (k \in D, F (k), \underset{˙}{0})) = (k \in A ⟼ if (k \in D, F (k), \underset{˙}{0}))$
87	6 83 84 85 86	offval2	$⊢ φ \to (k \in A ⟼ if (k \in C, F (k), \underset{˙}{0})) {\underset{˙}{+}}_{f} (k \in A ⟼ if (k \in D, F (k), \underset{˙}{0})) = (k \in A ⟼ if (k \in C, F (k), \underset{˙}{0}) \underset{˙}{+} if (k \in D, F (k), \underset{˙}{0}))$
88	79 87	eqtr4d	$⊢ φ \to F = (k \in A ⟼ if (k \in C, F (k), \underset{˙}{0})) {\underset{˙}{+}}_{f} (k \in A ⟼ if (k \in D, F (k), \underset{˙}{0}))$
89	88	oveq2d	$⊢ φ \to \sum_{G} F = \sum_{G} ((k \in A ⟼ if (k \in C, F (k), \underset{˙}{0})) {\underset{˙}{+}}_{f} (k \in A ⟼ if (k \in D, F (k), \underset{˙}{0})))$
90	43	reseq1d	$⊢ φ \to {F ↾}_{C} = {(k \in A ⟼ F (k)) ↾}_{C}$
91		ssun1	$⊢ C \subseteq C \cup D$
92	91 11	sseqtrrid	$⊢ φ \to C \subseteq A$
93	44	mpteq2ia	$⊢ (k \in C ⟼ if (k \in C, F (k), \underset{˙}{0})) = (k \in C ⟼ F (k))$
94		resmpt	$⊢ C \subseteq A \to {(k \in A ⟼ if (k \in C, F (k), \underset{˙}{0})) ↾}_{C} = (k \in C ⟼ if (k \in C, F (k), \underset{˙}{0}))$
95		resmpt	$⊢ C \subseteq A \to {(k \in A ⟼ F (k)) ↾}_{C} = (k \in C ⟼ F (k))$
96	93 94 95	3eqtr4a	$⊢ C \subseteq A \to {(k \in A ⟼ if (k \in C, F (k), \underset{˙}{0})) ↾}_{C} = {(k \in A ⟼ F (k)) ↾}_{C}$
97	92 96	syl	$⊢ φ \to {(k \in A ⟼ if (k \in C, F (k), \underset{˙}{0})) ↾}_{C} = {(k \in A ⟼ F (k)) ↾}_{C}$
98	90 97	eqtr4d	$⊢ φ \to {F ↾}_{C} = {(k \in A ⟼ if (k \in C, F (k), \underset{˙}{0})) ↾}_{C}$
99	98	oveq2d	$⊢ φ \to \sum_{G} ({F ↾}_{C}) = \sum_{G} ({(k \in A ⟼ if (k \in C, F (k), \underset{˙}{0})) ↾}_{C})$
100	83	fmpttd	$⊢ φ \to (k \in A ⟼ if (k \in C, F (k), \underset{˙}{0})) : A ⟶ B$
101	39	frnd	$⊢ φ \to ran (k \in A ⟼ if (k \in C, F (k), \underset{˙}{0})) \subseteq mrCls (SubMnd (G)) (ran F)$
102	4	cntzidss	$⊢ (mrCls (SubMnd (G)) (ran F) \subseteq Z (mrCls (SubMnd (G)) (ran F)) \land ran (k \in A ⟼ if (k \in C, F (k), \underset{˙}{0})) \subseteq mrCls (SubMnd (G)) (ran F)) \to ran (k \in A ⟼ if (k \in C, F (k), \underset{˙}{0})) \subseteq Z (ran (k \in A ⟼ if (k \in C, F (k), \underset{˙}{0})))$
103	28 101 102	syl2anc	$⊢ φ \to ran (k \in A ⟼ if (k \in C, F (k), \underset{˙}{0})) \subseteq Z (ran (k \in A ⟼ if (k \in C, F (k), \underset{˙}{0})))$
104		eldifn	$⊢ k \in (A ∖ C) \to \neg k \in C$
105	104	adantl	$⊢ (φ \land k \in (A ∖ C)) \to \neg k \in C$
106	105	iffalsed	$⊢ (φ \land k \in (A ∖ C)) \to if (k \in C, F (k), \underset{˙}{0}) = \underset{˙}{0}$
107	106 6	suppss2	$⊢ φ \to (k \in A ⟼ if (k \in C, F (k), \underset{˙}{0})) supp \underset{˙}{0} \subseteq C$
108	1 2 4 5 6 100 103 107 14	gsumzres	$⊢ φ \to \sum_{G} ({(k \in A ⟼ if (k \in C, F (k), \underset{˙}{0})) ↾}_{C}) = \underset{k \in A}{\sum_{G}} if (k \in C, F (k), \underset{˙}{0})$
109	99 108	eqtrd	$⊢ φ \to \sum_{G} ({F ↾}_{C}) = \underset{k \in A}{\sum_{G}} if (k \in C, F (k), \underset{˙}{0})$
110	43	reseq1d	$⊢ φ \to {F ↾}_{D} = {(k \in A ⟼ F (k)) ↾}_{D}$
111		ssun2	$⊢ D \subseteq C \cup D$
112	111 11	sseqtrrid	$⊢ φ \to D \subseteq A$
113	66	mpteq2ia	$⊢ (k \in D ⟼ if (k \in D, F (k), \underset{˙}{0})) = (k \in D ⟼ F (k))$
114		resmpt	$⊢ D \subseteq A \to {(k \in A ⟼ if (k \in D, F (k), \underset{˙}{0})) ↾}_{D} = (k \in D ⟼ if (k \in D, F (k), \underset{˙}{0}))$
115		resmpt	$⊢ D \subseteq A \to {(k \in A ⟼ F (k)) ↾}_{D} = (k \in D ⟼ F (k))$
116	113 114 115	3eqtr4a	$⊢ D \subseteq A \to {(k \in A ⟼ if (k \in D, F (k), \underset{˙}{0})) ↾}_{D} = {(k \in A ⟼ F (k)) ↾}_{D}$
117	112 116	syl	$⊢ φ \to {(k \in A ⟼ if (k \in D, F (k), \underset{˙}{0})) ↾}_{D} = {(k \in A ⟼ F (k)) ↾}_{D}$
118	110 117	eqtr4d	$⊢ φ \to {F ↾}_{D} = {(k \in A ⟼ if (k \in D, F (k), \underset{˙}{0})) ↾}_{D}$
119	118	oveq2d	$⊢ φ \to \sum_{G} ({F ↾}_{D}) = \sum_{G} ({(k \in A ⟼ if (k \in D, F (k), \underset{˙}{0})) ↾}_{D})$
120	84	fmpttd	$⊢ φ \to (k \in A ⟼ if (k \in D, F (k), \underset{˙}{0})) : A ⟶ B$
121	41	frnd	$⊢ φ \to ran (k \in A ⟼ if (k \in D, F (k), \underset{˙}{0})) \subseteq mrCls (SubMnd (G)) (ran F)$
122	4	cntzidss	$⊢ (mrCls (SubMnd (G)) (ran F) \subseteq Z (mrCls (SubMnd (G)) (ran F)) \land ran (k \in A ⟼ if (k \in D, F (k), \underset{˙}{0})) \subseteq mrCls (SubMnd (G)) (ran F)) \to ran (k \in A ⟼ if (k \in D, F (k), \underset{˙}{0})) \subseteq Z (ran (k \in A ⟼ if (k \in D, F (k), \underset{˙}{0})))$
123	28 121 122	syl2anc	$⊢ φ \to ran (k \in A ⟼ if (k \in D, F (k), \underset{˙}{0})) \subseteq Z (ran (k \in A ⟼ if (k \in D, F (k), \underset{˙}{0})))$
124		eldifn	$⊢ k \in (A ∖ D) \to \neg k \in D$
125	124	adantl	$⊢ (φ \land k \in (A ∖ D)) \to \neg k \in D$
126	125	iffalsed	$⊢ (φ \land k \in (A ∖ D)) \to if (k \in D, F (k), \underset{˙}{0}) = \underset{˙}{0}$
127	126 6	suppss2	$⊢ φ \to (k \in A ⟼ if (k \in D, F (k), \underset{˙}{0})) supp \underset{˙}{0} \subseteq D$
128	1 2 4 5 6 120 123 127 15	gsumzres	$⊢ φ \to \sum_{G} ({(k \in A ⟼ if (k \in D, F (k), \underset{˙}{0})) ↾}_{D}) = \underset{k \in A}{\sum_{G}} if (k \in D, F (k), \underset{˙}{0})$
129	119 128	eqtrd	$⊢ φ \to \sum_{G} ({F ↾}_{D}) = \underset{k \in A}{\sum_{G}} if (k \in D, F (k), \underset{˙}{0})$
130	109 129	oveq12d	$⊢ φ \to (\sum_{G}, ({F ↾}_{C})) \underset{˙}{+} (\sum_{G}, ({F ↾}_{D})) = (\underset{k \in A}{\sum_{G}}, if (k \in C, F (k), \underset{˙}{0})) \underset{˙}{+} (\underset{k \in A}{\sum_{G}}, if (k \in D, F (k), \underset{˙}{0}))$
131	42 89 130	3eqtr4d	$⊢ φ \to \sum_{G} F = (\sum_{G}, ({F ↾}_{C})) \underset{˙}{+} (\sum_{G}, ({F ↾}_{D}))$

Metamath Proof Explorer

Theorem gsumzsplit

Proof