gsumzadd

Description: The sum of two group sums. (Contributed by Mario Carneiro, 25-Apr-2016) (Revised by AV, 5-Jun-2019)

	Ref	Expression
Hypotheses	gsumzadd.b	$⊢ B = {Base}_{G}$
	gsumzadd.0	$⊢ \underset{˙}{0} = 0_{G}$
	gsumzadd.p	$⊢ \underset{˙}{+} = +_{G}$
	gsumzadd.z	$⊢ Z = Cntz (G)$
	gsumzadd.g	$⊢ φ \to G \in Mnd$
	gsumzadd.a	$⊢ φ \to A \in V$
	gsumzadd.fn	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (F)$
	gsumzadd.hn	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (H)$
	gsumzadd.s	$⊢ φ \to S \in SubMnd (G)$
	gsumzadd.c	$⊢ φ \to S \subseteq Z (S)$
	gsumzadd.f	$⊢ φ \to F : A ⟶ S$
	gsumzadd.h	$⊢ φ \to H : A ⟶ S$
Assertion	gsumzadd	$⊢ φ \to \sum_{G} (F {\underset{˙}{+}}_{f} H) = (\sum_{G}, F) \underset{˙}{+} (\sum_{G}, H)$

Proof

Step	Hyp	Ref	Expression
1		gsumzadd.b	$⊢ B = {Base}_{G}$
2		gsumzadd.0	$⊢ \underset{˙}{0} = 0_{G}$
3		gsumzadd.p	$⊢ \underset{˙}{+} = +_{G}$
4		gsumzadd.z	$⊢ Z = Cntz (G)$
5		gsumzadd.g	$⊢ φ \to G \in Mnd$
6		gsumzadd.a	$⊢ φ \to A \in V$
7		gsumzadd.fn	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (F)$
8		gsumzadd.hn	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (H)$
9		gsumzadd.s	$⊢ φ \to S \in SubMnd (G)$
10		gsumzadd.c	$⊢ φ \to S \subseteq Z (S)$
11		gsumzadd.f	$⊢ φ \to F : A ⟶ S$
12		gsumzadd.h	$⊢ φ \to H : A ⟶ S$
13		eqid	$⊢ (F \cup H) supp \underset{˙}{0} = (F \cup H) supp \underset{˙}{0}$
14	1	submss	$⊢ S \in SubMnd (G) \to S \subseteq B$
15	9 14	syl	$⊢ φ \to S \subseteq B$
16	11 15	fssd	$⊢ φ \to F : A ⟶ B$
17	12 15	fssd	$⊢ φ \to H : A ⟶ B$
18	11	frnd	$⊢ φ \to ran F \subseteq S$
19	4	cntzidss	$⊢ (S \subseteq Z (S) \land ran F \subseteq S) \to ran F \subseteq Z (ran F)$
20	10 18 19	syl2anc	$⊢ φ \to ran F \subseteq Z (ran F)$
21	12	frnd	$⊢ φ \to ran H \subseteq S$
22	4	cntzidss	$⊢ (S \subseteq Z (S) \land ran H \subseteq S) \to ran H \subseteq Z (ran H)$
23	10 21 22	syl2anc	$⊢ φ \to ran H \subseteq Z (ran H)$
24	3	submcl	$⊢ (S \in SubMnd (G) \land x \in S \land y \in S) \to x \underset{˙}{+} y \in S$
25	24	3expb	$⊢ (S \in SubMnd (G) \land (x \in S \land y \in S)) \to x \underset{˙}{+} y \in S$
26	9 25	sylan	$⊢ (φ \land (x \in S \land y \in S)) \to x \underset{˙}{+} y \in S$
27		inidm	$⊢ A \cap A = A$
28	26 11 12 6 6 27	off	$⊢ φ \to (F {\underset{˙}{+}}_{f} H) : A ⟶ S$
29	28	frnd	$⊢ φ \to ran (F {\underset{˙}{+}}_{f} H) \subseteq S$
30	4	cntzidss	$⊢ (S \subseteq Z (S) \land ran (F {\underset{˙}{+}}_{f} H) \subseteq S) \to ran (F {\underset{˙}{+}}_{f} H) \subseteq Z (ran (F {\underset{˙}{+}}_{f} H))$
31	10 29 30	syl2anc	$⊢ φ \to ran (F {\underset{˙}{+}}_{f} H) \subseteq Z (ran (F {\underset{˙}{+}}_{f} H))$
32	10	adantr	$⊢ (φ \land (x \subseteq A \land k \in (A ∖ x))) \to S \subseteq Z (S)$
33	15	adantr	$⊢ (φ \land (x \subseteq A \land k \in (A ∖ x))) \to S \subseteq B$
34	5	adantr	$⊢ (φ \land (x \subseteq A \land k \in (A ∖ x))) \to G \in Mnd$
35		vex	$⊢ x \in V$
36	35	a1i	$⊢ (φ \land (x \subseteq A \land k \in (A ∖ x))) \to x \in V$
37	9	adantr	$⊢ (φ \land (x \subseteq A \land k \in (A ∖ x))) \to S \in SubMnd (G)$
38		simpl	$⊢ (x \subseteq A \land k \in (A ∖ x)) \to x \subseteq A$
39		fssres	$⊢ (H : A ⟶ S \land x \subseteq A) \to ({H ↾}_{x}) : x ⟶ S$
40	12 38 39	syl2an	$⊢ (φ \land (x \subseteq A \land k \in (A ∖ x))) \to ({H ↾}_{x}) : x ⟶ S$
41	23	adantr	$⊢ (φ \land (x \subseteq A \land k \in (A ∖ x))) \to ran H \subseteq Z (ran H)$
42		resss	$⊢ {H ↾}_{x} \subseteq H$
43	42	rnssi	$⊢ ran ({H ↾}_{x}) \subseteq ran H$
44	4	cntzidss	$⊢ (ran H \subseteq Z (ran H) \land ran ({H ↾}_{x}) \subseteq ran H) \to ran ({H ↾}_{x}) \subseteq Z (ran ({H ↾}_{x}))$
45	41 43 44	sylancl	$⊢ (φ \land (x \subseteq A \land k \in (A ∖ x))) \to ran ({H ↾}_{x}) \subseteq Z (ran ({H ↾}_{x}))$
46	12	ffund	$⊢ φ \to Fun H$
47		funres	$⊢ Fun H \to Fun ({H ↾}_{x})$
48	46 47	syl	$⊢ φ \to Fun ({H ↾}_{x})$
49	48	adantr	$⊢ (φ \land (x \subseteq A \land k \in (A ∖ x))) \to Fun ({H ↾}_{x})$
50	8	fsuppimpd	$⊢ φ \to H supp \underset{˙}{0} \in Fin$
51	50	adantr	$⊢ (φ \land (x \subseteq A \land k \in (A ∖ x))) \to H supp \underset{˙}{0} \in Fin$
52		fex	$⊢ (H : A ⟶ S \land A \in V) \to H \in V$
53	12 6 52	syl2anc	$⊢ φ \to H \in V$
54	2	fvexi	$⊢ \underset{˙}{0} \in V$
55		ressuppss	$⊢ (H \in V \land \underset{˙}{0} \in V) \to ({H ↾}_{x}) supp \underset{˙}{0} \subseteq H supp \underset{˙}{0}$
56	53 54 55	sylancl	$⊢ φ \to ({H ↾}_{x}) supp \underset{˙}{0} \subseteq H supp \underset{˙}{0}$
57	56	adantr	$⊢ (φ \land (x \subseteq A \land k \in (A ∖ x))) \to ({H ↾}_{x}) supp \underset{˙}{0} \subseteq H supp \underset{˙}{0}$
58	51 57	ssfid	$⊢ (φ \land (x \subseteq A \land k \in (A ∖ x))) \to ({H ↾}_{x}) supp \underset{˙}{0} \in Fin$
59		resfunexg	$⊢ (Fun H \land x \in V) \to {H ↾}_{x} \in V$
60	46 35 59	sylancl	$⊢ φ \to {H ↾}_{x} \in V$
61		isfsupp	$⊢ ({H ↾}_{x} \in V \land \underset{˙}{0} \in V) \to ({finSupp}_{\underset{˙}{0}} (({H ↾}_{x})) \leftrightarrow (Fun ({H ↾}_{x}) \land ({H ↾}_{x}) supp \underset{˙}{0} \in Fin))$
62	60 54 61	sylancl	$⊢ φ \to ({finSupp}_{\underset{˙}{0}} (({H ↾}_{x})) \leftrightarrow (Fun ({H ↾}_{x}) \land ({H ↾}_{x}) supp \underset{˙}{0} \in Fin))$
63	62	adantr	$⊢ (φ \land (x \subseteq A \land k \in (A ∖ x))) \to ({finSupp}_{\underset{˙}{0}} (({H ↾}_{x})) \leftrightarrow (Fun ({H ↾}_{x}) \land ({H ↾}_{x}) supp \underset{˙}{0} \in Fin))$
64	49 58 63	mpbir2and	$⊢ (φ \land (x \subseteq A \land k \in (A ∖ x))) \to {finSupp}_{\underset{˙}{0}} (({H ↾}_{x}))$
65	2 4 34 36 37 40 45 64	gsumzsubmcl	$⊢ (φ \land (x \subseteq A \land k \in (A ∖ x))) \to \sum_{G} ({H ↾}_{x}) \in S$
66	65	snssd	$⊢ (φ \land (x \subseteq A \land k \in (A ∖ x))) \to \{\sum_{G} ({H ↾}_{x})\} \subseteq S$
67	1 4	cntz2ss	$⊢ (S \subseteq B \land \{\sum_{G} ({H ↾}_{x})\} \subseteq S) \to Z (S) \subseteq Z (\{\sum_{G} ({H ↾}_{x})\})$
68	33 66 67	syl2anc	$⊢ (φ \land (x \subseteq A \land k \in (A ∖ x))) \to Z (S) \subseteq Z (\{\sum_{G} ({H ↾}_{x})\})$
69	32 68	sstrd	$⊢ (φ \land (x \subseteq A \land k \in (A ∖ x))) \to S \subseteq Z (\{\sum_{G} ({H ↾}_{x})\})$
70		eldifi	$⊢ k \in (A ∖ x) \to k \in A$
71	70	adantl	$⊢ (x \subseteq A \land k \in (A ∖ x)) \to k \in A$
72		ffvelrn	$⊢ (F : A ⟶ S \land k \in A) \to F (k) \in S$
73	11 71 72	syl2an	$⊢ (φ \land (x \subseteq A \land k \in (A ∖ x))) \to F (k) \in S$
74	69 73	sseldd	$⊢ (φ \land (x \subseteq A \land k \in (A ∖ x))) \to F (k) \in Z (\{\sum_{G} ({H ↾}_{x})\})$
75	1 2 3 4 5 6 7 8 13 16 17 20 23 31 74	gsumzaddlem	$⊢ φ \to \sum_{G} (F {\underset{˙}{+}}_{f} H) = (\sum_{G}, F) \underset{˙}{+} (\sum_{G}, H)$

Metamath Proof Explorer

Theorem gsumzadd

Proof