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	46	funresd	$⊢ φ \to Fun ({H ↾}_{x})$
48	47	adantr	$⊢ (φ \land (x \subseteq A \land k \in (A ∖ x))) \to Fun ({H ↾}_{x})$
49	8	fsuppimpd	$⊢ φ \to H supp \underset{˙}{0} \in Fin$
50	49	adantr	$⊢ (φ \land (x \subseteq A \land k \in (A ∖ x))) \to H supp \underset{˙}{0} \in Fin$
51	12 6	fexd	$⊢ φ \to H \in V$
52	2	fvexi	$⊢ \underset{˙}{0} \in V$
53		ressuppss	$⊢ (H \in V \land \underset{˙}{0} \in V) \to ({H ↾}_{x}) supp \underset{˙}{0} \subseteq H supp \underset{˙}{0}$
54	51 52 53	sylancl	$⊢ φ \to ({H ↾}_{x}) supp \underset{˙}{0} \subseteq H supp \underset{˙}{0}$
55	54	adantr	$⊢ (φ \land (x \subseteq A \land k \in (A ∖ x))) \to ({H ↾}_{x}) supp \underset{˙}{0} \subseteq H supp \underset{˙}{0}$
56	50 55	ssfid	$⊢ (φ \land (x \subseteq A \land k \in (A ∖ x))) \to ({H ↾}_{x}) supp \underset{˙}{0} \in Fin$
57		resfunexg	$⊢ (Fun H \land x \in V) \to {H ↾}_{x} \in V$
58	46 35 57	sylancl	$⊢ φ \to {H ↾}_{x} \in V$
59		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))$
60	58 52 59	sylancl	$⊢ φ \to ({finSupp}_{\underset{˙}{0}} (({H ↾}_{x})) \leftrightarrow (Fun ({H ↾}_{x}) \land ({H ↾}_{x}) supp \underset{˙}{0} \in Fin))$
61	60	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))$
62	48 56 61	mpbir2and	$⊢ (φ \land (x \subseteq A \land k \in (A ∖ x))) \to {finSupp}_{\underset{˙}{0}} (({H ↾}_{x}))$
63	2 4 34 36 37 40 45 62	gsumzsubmcl	$⊢ (φ \land (x \subseteq A \land k \in (A ∖ x))) \to \sum_{G} ({H ↾}_{x}) \in S$
64	63	snssd	$⊢ (φ \land (x \subseteq A \land k \in (A ∖ x))) \to \{\sum_{G} ({H ↾}_{x})\} \subseteq S$
65	1 4	cntz2ss	$⊢ (S \subseteq B \land \{\sum_{G} ({H ↾}_{x})\} \subseteq S) \to Z (S) \subseteq Z (\{\sum_{G} ({H ↾}_{x})\})$
66	33 64 65	syl2anc	$⊢ (φ \land (x \subseteq A \land k \in (A ∖ x))) \to Z (S) \subseteq Z (\{\sum_{G} ({H ↾}_{x})\})$
67	32 66	sstrd	$⊢ (φ \land (x \subseteq A \land k \in (A ∖ x))) \to S \subseteq Z (\{\sum_{G} ({H ↾}_{x})\})$
68		eldifi	$⊢ k \in (A ∖ x) \to k \in A$
69	68	adantl	$⊢ (x \subseteq A \land k \in (A ∖ x)) \to k \in A$
70		ffvelcdm	$⊢ (F : A ⟶ S \land k \in A) \to F (k) \in S$
71	11 69 70	syl2an	$⊢ (φ \land (x \subseteq A \land k \in (A ∖ x))) \to F (k) \in S$
72	67 71	sseldd	$⊢ (φ \land (x \subseteq A \land k \in (A ∖ x))) \to F (k) \in Z (\{\sum_{G} ({H ↾}_{x})\})$
73	1 2 3 4 5 6 7 8 13 16 17 20 23 31 72	gsumzaddlem	$⊢ φ \to \sum_{G} (F {\underset{˙}{+}}_{f} H) = (\sum_{G}, F) \underset{˙}{+} (\sum_{G}, H)$

Metamath Proof Explorer

Theorem gsumzadd

Proof