dprdfadd

Description: Take the sum of group sums over two families of elements of disjoint subgroups. (Contributed by Mario Carneiro, 25-Apr-2016) (Revised by AV, 14-Jul-2019)

	Ref	Expression
Hypotheses	eldprdi.0	$⊢ \underset{˙}{0} = 0_{G}$
	eldprdi.w	$⊢ W = \{h \in \underset{i \in I}{⨉} S (i) \| {finSupp}_{\underset{˙}{0}} (h)\}$
	eldprdi.1	$⊢ φ \to G dom DProd S$
	eldprdi.2	$⊢ φ \to dom S = I$
	eldprdi.3	$⊢ φ \to F \in W$
	dprdfadd.4	$⊢ φ \to H \in W$
	dprdfadd.b	$⊢ \underset{˙}{+} = +_{G}$
Assertion	dprdfadd	$⊢ φ \to (F {\underset{˙}{+}}_{f} H \in W \land \sum_{G} (F {\underset{˙}{+}}_{f} H) = (\sum_{G}, F) \underset{˙}{+} (\sum_{G}, H))$

Proof

Step	Hyp	Ref	Expression
1		eldprdi.0	$⊢ \underset{˙}{0} = 0_{G}$
2		eldprdi.w	$⊢ W = \{h \in \underset{i \in I}{⨉} S (i) \| {finSupp}_{\underset{˙}{0}} (h)\}$
3		eldprdi.1	$⊢ φ \to G dom DProd S$
4		eldprdi.2	$⊢ φ \to dom S = I$
5		eldprdi.3	$⊢ φ \to F \in W$
6		dprdfadd.4	$⊢ φ \to H \in W$
7		dprdfadd.b	$⊢ \underset{˙}{+} = +_{G}$
8	3 4	dprddomcld	$⊢ φ \to I \in V$
9	2 3 4 5	dprdfcl	$⊢ (φ \land x \in I) \to F (x) \in S (x)$
10	2 3 4 6	dprdfcl	$⊢ (φ \land x \in I) \to H (x) \in S (x)$
11		eqid	$⊢ {Base}_{G} = {Base}_{G}$
12	2 3 4 5 11	dprdff	$⊢ φ \to F : I ⟶ {Base}_{G}$
13	12	feqmptd	$⊢ φ \to F = (x \in I ⟼ F (x))$
14	2 3 4 6 11	dprdff	$⊢ φ \to H : I ⟶ {Base}_{G}$
15	14	feqmptd	$⊢ φ \to H = (x \in I ⟼ H (x))$
16	8 9 10 13 15	offval2	$⊢ φ \to F {\underset{˙}{+}}_{f} H = (x \in I ⟼ F (x) \underset{˙}{+} H (x))$
17	3 4	dprdf2	$⊢ φ \to S : I ⟶ SubGrp (G)$
18	17	ffvelrnda	$⊢ (φ \land x \in I) \to S (x) \in SubGrp (G)$
19	7	subgcl	$⊢ (S (x) \in SubGrp (G) \land F (x) \in S (x) \land H (x) \in S (x)) \to F (x) \underset{˙}{+} H (x) \in S (x)$
20	18 9 10 19	syl3anc	$⊢ (φ \land x \in I) \to F (x) \underset{˙}{+} H (x) \in S (x)$
21	2 3 4 5	dprdffsupp	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (F)$
22	2 3 4 6	dprdffsupp	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (H)$
23	21 22	fsuppunfi	$⊢ φ \to {supp}_{\underset{˙}{0}} (F) \cup {supp}_{\underset{˙}{0}} (H) \in Fin$
24		ssun1	$⊢ F supp \underset{˙}{0} \subseteq {supp}_{\underset{˙}{0}} (F) \cup {supp}_{\underset{˙}{0}} (H)$
25	24	a1i	$⊢ φ \to F supp \underset{˙}{0} \subseteq {supp}_{\underset{˙}{0}} (F) \cup {supp}_{\underset{˙}{0}} (H)$
26	1	fvexi	$⊢ \underset{˙}{0} \in V$
27	26	a1i	$⊢ φ \to \underset{˙}{0} \in V$
28	12 25 8 27	suppssr	$⊢ (φ \land x \in (I ∖ ({supp}_{\underset{˙}{0}} (F) \cup {supp}_{\underset{˙}{0}} (H)))) \to F (x) = \underset{˙}{0}$
29		ssun2	$⊢ H supp \underset{˙}{0} \subseteq {supp}_{\underset{˙}{0}} (F) \cup {supp}_{\underset{˙}{0}} (H)$
30	29	a1i	$⊢ φ \to H supp \underset{˙}{0} \subseteq {supp}_{\underset{˙}{0}} (F) \cup {supp}_{\underset{˙}{0}} (H)$
31	14 30 8 27	suppssr	$⊢ (φ \land x \in (I ∖ ({supp}_{\underset{˙}{0}} (F) \cup {supp}_{\underset{˙}{0}} (H)))) \to H (x) = \underset{˙}{0}$
32	28 31	oveq12d	$⊢ (φ \land x \in (I ∖ ({supp}_{\underset{˙}{0}} (F) \cup {supp}_{\underset{˙}{0}} (H)))) \to F (x) \underset{˙}{+} H (x) = \underset{˙}{0} \underset{˙}{+} \underset{˙}{0}$
33		dprdgrp	$⊢ G dom DProd S \to G \in Grp$
34	3 33	syl	$⊢ φ \to G \in Grp$
35	11 1	grpidcl	$⊢ G \in Grp \to \underset{˙}{0} \in {Base}_{G}$
36	11 7 1	grplid	$⊢ (G \in Grp \land \underset{˙}{0} \in {Base}_{G}) \to \underset{˙}{0} \underset{˙}{+} \underset{˙}{0} = \underset{˙}{0}$
37	34 35 36	syl2anc2	$⊢ φ \to \underset{˙}{0} \underset{˙}{+} \underset{˙}{0} = \underset{˙}{0}$
38	37	adantr	$⊢ (φ \land x \in (I ∖ ({supp}_{\underset{˙}{0}} (F) \cup {supp}_{\underset{˙}{0}} (H)))) \to \underset{˙}{0} \underset{˙}{+} \underset{˙}{0} = \underset{˙}{0}$
39	32 38	eqtrd	$⊢ (φ \land x \in (I ∖ ({supp}_{\underset{˙}{0}} (F) \cup {supp}_{\underset{˙}{0}} (H)))) \to F (x) \underset{˙}{+} H (x) = \underset{˙}{0}$
40	39 8	suppss2	$⊢ φ \to (x \in I ⟼ F (x) \underset{˙}{+} H (x)) supp \underset{˙}{0} \subseteq {supp}_{\underset{˙}{0}} (F) \cup {supp}_{\underset{˙}{0}} (H)$
41	23 40	ssfid	$⊢ φ \to (x \in I ⟼ F (x) \underset{˙}{+} H (x)) supp \underset{˙}{0} \in Fin$
42		funmpt	$⊢ Fun (x \in I ⟼ F (x) \underset{˙}{+} H (x))$
43	42	a1i	$⊢ φ \to Fun (x \in I ⟼ F (x) \underset{˙}{+} H (x))$
44	8	mptexd	$⊢ φ \to (x \in I ⟼ F (x) \underset{˙}{+} H (x)) \in V$
45		funisfsupp	$⊢ (Fun (x \in I ⟼ F (x) \underset{˙}{+} H (x)) \land (x \in I ⟼ F (x) \underset{˙}{+} H (x)) \in V \land \underset{˙}{0} \in V) \to ({finSupp}_{\underset{˙}{0}} ((x \in I ⟼ F (x) \underset{˙}{+} H (x))) \leftrightarrow (x \in I ⟼ F (x) \underset{˙}{+} H (x)) supp \underset{˙}{0} \in Fin)$
46	43 44 27 45	syl3anc	$⊢ φ \to ({finSupp}_{\underset{˙}{0}} ((x \in I ⟼ F (x) \underset{˙}{+} H (x))) \leftrightarrow (x \in I ⟼ F (x) \underset{˙}{+} H (x)) supp \underset{˙}{0} \in Fin)$
47	41 46	mpbird	$⊢ φ \to {finSupp}_{\underset{˙}{0}} ((x \in I ⟼ F (x) \underset{˙}{+} H (x)))$
48	2 3 4 20 47	dprdwd	$⊢ φ \to (x \in I ⟼ F (x) \underset{˙}{+} H (x)) \in W$
49	16 48	eqeltrd	$⊢ φ \to F {\underset{˙}{+}}_{f} H \in W$
50		eqid	$⊢ Cntz (G) = Cntz (G)$
51		grpmnd	$⊢ G \in Grp \to G \in Mnd$
52	34 51	syl	$⊢ φ \to G \in Mnd$
53		eqid	$⊢ (F \cup H) supp \underset{˙}{0} = (F \cup H) supp \underset{˙}{0}$
54	2 3 4 5 50	dprdfcntz	$⊢ φ \to ran F \subseteq Cntz (G) (ran F)$
55	2 3 4 6 50	dprdfcntz	$⊢ φ \to ran H \subseteq Cntz (G) (ran H)$
56	2 3 4 49 50	dprdfcntz	$⊢ φ \to ran (F {\underset{˙}{+}}_{f} H) \subseteq Cntz (G) (ran (F {\underset{˙}{+}}_{f} H))$
57	52	adantr	$⊢ (φ \land (x \subseteq I \land k \in (I ∖ x))) \to G \in Mnd$
58		vex	$⊢ x \in V$
59	58	a1i	$⊢ (φ \land (x \subseteq I \land k \in (I ∖ x))) \to x \in V$
60		eldifi	$⊢ k \in (I ∖ x) \to k \in I$
61	60	adantl	$⊢ (x \subseteq I \land k \in (I ∖ x)) \to k \in I$
62		ffvelrn	$⊢ (F : I ⟶ {Base}_{G} \land k \in I) \to F (k) \in {Base}_{G}$
63	12 61 62	syl2an	$⊢ (φ \land (x \subseteq I \land k \in (I ∖ x))) \to F (k) \in {Base}_{G}$
64	63	snssd	$⊢ (φ \land (x \subseteq I \land k \in (I ∖ x))) \to \{F (k)\} \subseteq {Base}_{G}$
65	11 50	cntzsubm	$⊢ (G \in Mnd \land \{F (k)\} \subseteq {Base}_{G}) \to Cntz (G) (\{F (k)\}) \in SubMnd (G)$
66	57 64 65	syl2anc	$⊢ (φ \land (x \subseteq I \land k \in (I ∖ x))) \to Cntz (G) (\{F (k)\}) \in SubMnd (G)$
67	14	adantr	$⊢ (φ \land (x \subseteq I \land k \in (I ∖ x))) \to H : I ⟶ {Base}_{G}$
68	67	ffnd	$⊢ (φ \land (x \subseteq I \land k \in (I ∖ x))) \to H Fn I$
69		simprl	$⊢ (φ \land (x \subseteq I \land k \in (I ∖ x))) \to x \subseteq I$
70		fnssres	$⊢ (H Fn I \land x \subseteq I) \to ({H ↾}_{x}) Fn x$
71	68 69 70	syl2anc	$⊢ (φ \land (x \subseteq I \land k \in (I ∖ x))) \to ({H ↾}_{x}) Fn x$
72		fvres	$⊢ y \in x \to ({H ↾}_{x}) (y) = H (y)$
73	72	adantl	$⊢ ((φ \land (x \subseteq I \land k \in (I ∖ x))) \land y \in x) \to ({H ↾}_{x}) (y) = H (y)$
74	3	ad2antrr	$⊢ ((φ \land (x \subseteq I \land k \in (I ∖ x))) \land y \in x) \to G dom DProd S$
75	4	ad2antrr	$⊢ ((φ \land (x \subseteq I \land k \in (I ∖ x))) \land y \in x) \to dom S = I$
76	74 75	dprdf2	$⊢ ((φ \land (x \subseteq I \land k \in (I ∖ x))) \land y \in x) \to S : I ⟶ SubGrp (G)$
77	61	ad2antlr	$⊢ ((φ \land (x \subseteq I \land k \in (I ∖ x))) \land y \in x) \to k \in I$
78	76 77	ffvelrnd	$⊢ ((φ \land (x \subseteq I \land k \in (I ∖ x))) \land y \in x) \to S (k) \in SubGrp (G)$
79	11	subgss	$⊢ S (k) \in SubGrp (G) \to S (k) \subseteq {Base}_{G}$
80	78 79	syl	$⊢ ((φ \land (x \subseteq I \land k \in (I ∖ x))) \land y \in x) \to S (k) \subseteq {Base}_{G}$
81	5	ad2antrr	$⊢ ((φ \land (x \subseteq I \land k \in (I ∖ x))) \land y \in x) \to F \in W$
82	2 74 75 81	dprdfcl	$⊢ (((φ \land (x \subseteq I \land k \in (I ∖ x))) \land y \in x) \land k \in I) \to F (k) \in S (k)$
83	77 82	mpdan	$⊢ ((φ \land (x \subseteq I \land k \in (I ∖ x))) \land y \in x) \to F (k) \in S (k)$
84	83	snssd	$⊢ ((φ \land (x \subseteq I \land k \in (I ∖ x))) \land y \in x) \to \{F (k)\} \subseteq S (k)$
85	11 50	cntz2ss	$⊢ (S (k) \subseteq {Base}_{G} \land \{F (k)\} \subseteq S (k)) \to Cntz (G) (S (k)) \subseteq Cntz (G) (\{F (k)\})$
86	80 84 85	syl2anc	$⊢ ((φ \land (x \subseteq I \land k \in (I ∖ x))) \land y \in x) \to Cntz (G) (S (k)) \subseteq Cntz (G) (\{F (k)\})$
87	69	sselda	$⊢ ((φ \land (x \subseteq I \land k \in (I ∖ x))) \land y \in x) \to y \in I$
88		simpr	$⊢ ((φ \land (x \subseteq I \land k \in (I ∖ x))) \land y \in x) \to y \in x$
89		simplrr	$⊢ ((φ \land (x \subseteq I \land k \in (I ∖ x))) \land y \in x) \to k \in (I ∖ x)$
90	89	eldifbd	$⊢ ((φ \land (x \subseteq I \land k \in (I ∖ x))) \land y \in x) \to \neg k \in x$
91		nelne2	$⊢ (y \in x \land \neg k \in x) \to y \neq k$
92	88 90 91	syl2anc	$⊢ ((φ \land (x \subseteq I \land k \in (I ∖ x))) \land y \in x) \to y \neq k$
93	74 75 87 77 92 50	dprdcntz	$⊢ ((φ \land (x \subseteq I \land k \in (I ∖ x))) \land y \in x) \to S (y) \subseteq Cntz (G) (S (k))$
94	6	ad2antrr	$⊢ ((φ \land (x \subseteq I \land k \in (I ∖ x))) \land y \in x) \to H \in W$
95	2 74 75 94	dprdfcl	$⊢ (((φ \land (x \subseteq I \land k \in (I ∖ x))) \land y \in x) \land y \in I) \to H (y) \in S (y)$
96	87 95	mpdan	$⊢ ((φ \land (x \subseteq I \land k \in (I ∖ x))) \land y \in x) \to H (y) \in S (y)$
97	93 96	sseldd	$⊢ ((φ \land (x \subseteq I \land k \in (I ∖ x))) \land y \in x) \to H (y) \in Cntz (G) (S (k))$
98	86 97	sseldd	$⊢ ((φ \land (x \subseteq I \land k \in (I ∖ x))) \land y \in x) \to H (y) \in Cntz (G) (\{F (k)\})$
99	73 98	eqeltrd	$⊢ ((φ \land (x \subseteq I \land k \in (I ∖ x))) \land y \in x) \to ({H ↾}_{x}) (y) \in Cntz (G) (\{F (k)\})$
100	99	ralrimiva	$⊢ (φ \land (x \subseteq I \land k \in (I ∖ x))) \to \forall y \in x ({H ↾}_{x}) (y) \in Cntz (G) (\{F (k)\})$
101		ffnfv	$⊢ ({H ↾}_{x}) : x ⟶ Cntz (G) (\{F (k)\}) \leftrightarrow (({H ↾}_{x}) Fn x \land \forall y \in x ({H ↾}_{x}) (y) \in Cntz (G) (\{F (k)\}))$
102	71 100 101	sylanbrc	$⊢ (φ \land (x \subseteq I \land k \in (I ∖ x))) \to ({H ↾}_{x}) : x ⟶ Cntz (G) (\{F (k)\})$
103		resss	$⊢ {H ↾}_{x} \subseteq H$
104	103	rnssi	$⊢ ran ({H ↾}_{x}) \subseteq ran H$
105	50	cntzidss	$⊢ (ran H \subseteq Cntz (G) (ran H) \land ran ({H ↾}_{x}) \subseteq ran H) \to ran ({H ↾}_{x}) \subseteq Cntz (G) (ran ({H ↾}_{x}))$
106	55 104 105	sylancl	$⊢ φ \to ran ({H ↾}_{x}) \subseteq Cntz (G) (ran ({H ↾}_{x}))$
107	106	adantr	$⊢ (φ \land (x \subseteq I \land k \in (I ∖ x))) \to ran ({H ↾}_{x}) \subseteq Cntz (G) (ran ({H ↾}_{x}))$
108	22 27	fsuppres	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (({H ↾}_{x}))$
109	108	adantr	$⊢ (φ \land (x \subseteq I \land k \in (I ∖ x))) \to {finSupp}_{\underset{˙}{0}} (({H ↾}_{x}))$
110	1 50 57 59 66 102 107 109	gsumzsubmcl	$⊢ (φ \land (x \subseteq I \land k \in (I ∖ x))) \to \sum_{G} ({H ↾}_{x}) \in Cntz (G) (\{F (k)\})$
111	110	snssd	$⊢ (φ \land (x \subseteq I \land k \in (I ∖ x))) \to \{\sum_{G} ({H ↾}_{x})\} \subseteq Cntz (G) (\{F (k)\})$
112	67 69	fssresd	$⊢ (φ \land (x \subseteq I \land k \in (I ∖ x))) \to ({H ↾}_{x}) : x ⟶ {Base}_{G}$
113	11 1 50 57 59 112 107 109	gsumzcl	$⊢ (φ \land (x \subseteq I \land k \in (I ∖ x))) \to \sum_{G} ({H ↾}_{x}) \in {Base}_{G}$
114	113	snssd	$⊢ (φ \land (x \subseteq I \land k \in (I ∖ x))) \to \{\sum_{G} ({H ↾}_{x})\} \subseteq {Base}_{G}$
115	11 50	cntzrec	$⊢ (\{\sum_{G} ({H ↾}_{x})\} \subseteq {Base}_{G} \land \{F (k)\} \subseteq {Base}_{G}) \to (\{\sum_{G} ({H ↾}_{x})\} \subseteq Cntz (G) (\{F (k)\}) \leftrightarrow \{F (k)\} \subseteq Cntz (G) (\{\sum_{G} ({H ↾}_{x})\}))$
116	114 64 115	syl2anc	$⊢ (φ \land (x \subseteq I \land k \in (I ∖ x))) \to (\{\sum_{G} ({H ↾}_{x})\} \subseteq Cntz (G) (\{F (k)\}) \leftrightarrow \{F (k)\} \subseteq Cntz (G) (\{\sum_{G} ({H ↾}_{x})\}))$
117	111 116	mpbid	$⊢ (φ \land (x \subseteq I \land k \in (I ∖ x))) \to \{F (k)\} \subseteq Cntz (G) (\{\sum_{G} ({H ↾}_{x})\})$
118		fvex	$⊢ F (k) \in V$
119	118	snss	$⊢ F (k) \in Cntz (G) (\{\sum_{G} ({H ↾}_{x})\}) \leftrightarrow \{F (k)\} \subseteq Cntz (G) (\{\sum_{G} ({H ↾}_{x})\})$
120	117 119	sylibr	$⊢ (φ \land (x \subseteq I \land k \in (I ∖ x))) \to F (k) \in Cntz (G) (\{\sum_{G} ({H ↾}_{x})\})$
121	11 1 7 50 52 8 21 22 53 12 14 54 55 56 120	gsumzaddlem	$⊢ φ \to \sum_{G} (F {\underset{˙}{+}}_{f} H) = (\sum_{G}, F) \underset{˙}{+} (\sum_{G}, H)$
122	49 121	jca	$⊢ φ \to (F {\underset{˙}{+}}_{f} H \in W \land \sum_{G} (F {\underset{˙}{+}}_{f} H) = (\sum_{G}, F) \underset{˙}{+} (\sum_{G}, H))$

Metamath Proof Explorer

Theorem dprdfadd

Proof