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	34	grpmndd	$⊢ φ \to G \in Mnd$
52		eqid	$⊢ (F \cup H) supp \underset{˙}{0} = (F \cup H) supp \underset{˙}{0}$
53	2 3 4 5 50	dprdfcntz	$⊢ φ \to ran F \subseteq Cntz (G) (ran F)$
54	2 3 4 6 50	dprdfcntz	$⊢ φ \to ran H \subseteq Cntz (G) (ran H)$
55	2 3 4 49 50	dprdfcntz	$⊢ φ \to ran (F {\underset{˙}{+}}_{f} H) \subseteq Cntz (G) (ran (F {\underset{˙}{+}}_{f} H))$
56	51	adantr	$⊢ (φ \land (x \subseteq I \land k \in (I ∖ x))) \to G \in Mnd$
57		vex	$⊢ x \in V$
58	57	a1i	$⊢ (φ \land (x \subseteq I \land k \in (I ∖ x))) \to x \in V$
59		eldifi	$⊢ k \in (I ∖ x) \to k \in I$
60	59	adantl	$⊢ (x \subseteq I \land k \in (I ∖ x)) \to k \in I$
61		ffvelrn	$⊢ (F : I ⟶ {Base}_{G} \land k \in I) \to F (k) \in {Base}_{G}$
62	12 60 61	syl2an	$⊢ (φ \land (x \subseteq I \land k \in (I ∖ x))) \to F (k) \in {Base}_{G}$
63	62	snssd	$⊢ (φ \land (x \subseteq I \land k \in (I ∖ x))) \to \{F (k)\} \subseteq {Base}_{G}$
64	11 50	cntzsubm	$⊢ (G \in Mnd \land \{F (k)\} \subseteq {Base}_{G}) \to Cntz (G) (\{F (k)\}) \in SubMnd (G)$
65	56 63 64	syl2anc	$⊢ (φ \land (x \subseteq I \land k \in (I ∖ x))) \to Cntz (G) (\{F (k)\}) \in SubMnd (G)$
66	14	adantr	$⊢ (φ \land (x \subseteq I \land k \in (I ∖ x))) \to H : I ⟶ {Base}_{G}$
67	66	ffnd	$⊢ (φ \land (x \subseteq I \land k \in (I ∖ x))) \to H Fn I$
68		simprl	$⊢ (φ \land (x \subseteq I \land k \in (I ∖ x))) \to x \subseteq I$
69		fnssres	$⊢ (H Fn I \land x \subseteq I) \to ({H ↾}_{x}) Fn x$
70	67 68 69	syl2anc	$⊢ (φ \land (x \subseteq I \land k \in (I ∖ x))) \to ({H ↾}_{x}) Fn x$
71		fvres	$⊢ y \in x \to ({H ↾}_{x}) (y) = H (y)$
72	71	adantl	$⊢ ((φ \land (x \subseteq I \land k \in (I ∖ x))) \land y \in x) \to ({H ↾}_{x}) (y) = H (y)$
73	3	ad2antrr	$⊢ ((φ \land (x \subseteq I \land k \in (I ∖ x))) \land y \in x) \to G dom DProd S$
74	4	ad2antrr	$⊢ ((φ \land (x \subseteq I \land k \in (I ∖ x))) \land y \in x) \to dom S = I$
75	73 74	dprdf2	$⊢ ((φ \land (x \subseteq I \land k \in (I ∖ x))) \land y \in x) \to S : I ⟶ SubGrp (G)$
76	60	ad2antlr	$⊢ ((φ \land (x \subseteq I \land k \in (I ∖ x))) \land y \in x) \to k \in I$
77	75 76	ffvelrnd	$⊢ ((φ \land (x \subseteq I \land k \in (I ∖ x))) \land y \in x) \to S (k) \in SubGrp (G)$
78	11	subgss	$⊢ S (k) \in SubGrp (G) \to S (k) \subseteq {Base}_{G}$
79	77 78	syl	$⊢ ((φ \land (x \subseteq I \land k \in (I ∖ x))) \land y \in x) \to S (k) \subseteq {Base}_{G}$
80	5	ad2antrr	$⊢ ((φ \land (x \subseteq I \land k \in (I ∖ x))) \land y \in x) \to F \in W$
81	2 73 74 80	dprdfcl	$⊢ (((φ \land (x \subseteq I \land k \in (I ∖ x))) \land y \in x) \land k \in I) \to F (k) \in S (k)$
82	76 81	mpdan	$⊢ ((φ \land (x \subseteq I \land k \in (I ∖ x))) \land y \in x) \to F (k) \in S (k)$
83	82	snssd	$⊢ ((φ \land (x \subseteq I \land k \in (I ∖ x))) \land y \in x) \to \{F (k)\} \subseteq S (k)$
84	11 50	cntz2ss	$⊢ (S (k) \subseteq {Base}_{G} \land \{F (k)\} \subseteq S (k)) \to Cntz (G) (S (k)) \subseteq Cntz (G) (\{F (k)\})$
85	79 83 84	syl2anc	$⊢ ((φ \land (x \subseteq I \land k \in (I ∖ x))) \land y \in x) \to Cntz (G) (S (k)) \subseteq Cntz (G) (\{F (k)\})$
86	68	sselda	$⊢ ((φ \land (x \subseteq I \land k \in (I ∖ x))) \land y \in x) \to y \in I$
87		simpr	$⊢ ((φ \land (x \subseteq I \land k \in (I ∖ x))) \land y \in x) \to y \in x$
88		simplrr	$⊢ ((φ \land (x \subseteq I \land k \in (I ∖ x))) \land y \in x) \to k \in (I ∖ x)$
89	88	eldifbd	$⊢ ((φ \land (x \subseteq I \land k \in (I ∖ x))) \land y \in x) \to \neg k \in x$
90		nelne2	$⊢ (y \in x \land \neg k \in x) \to y \neq k$
91	87 89 90	syl2anc	$⊢ ((φ \land (x \subseteq I \land k \in (I ∖ x))) \land y \in x) \to y \neq k$
92	73 74 86 76 91 50	dprdcntz	$⊢ ((φ \land (x \subseteq I \land k \in (I ∖ x))) \land y \in x) \to S (y) \subseteq Cntz (G) (S (k))$
93	6	ad2antrr	$⊢ ((φ \land (x \subseteq I \land k \in (I ∖ x))) \land y \in x) \to H \in W$
94	2 73 74 93	dprdfcl	$⊢ (((φ \land (x \subseteq I \land k \in (I ∖ x))) \land y \in x) \land y \in I) \to H (y) \in S (y)$
95	86 94	mpdan	$⊢ ((φ \land (x \subseteq I \land k \in (I ∖ x))) \land y \in x) \to H (y) \in S (y)$
96	92 95	sseldd	$⊢ ((φ \land (x \subseteq I \land k \in (I ∖ x))) \land y \in x) \to H (y) \in Cntz (G) (S (k))$
97	85 96	sseldd	$⊢ ((φ \land (x \subseteq I \land k \in (I ∖ x))) \land y \in x) \to H (y) \in Cntz (G) (\{F (k)\})$
98	72 97	eqeltrd	$⊢ ((φ \land (x \subseteq I \land k \in (I ∖ x))) \land y \in x) \to ({H ↾}_{x}) (y) \in Cntz (G) (\{F (k)\})$
99	98	ralrimiva	$⊢ (φ \land (x \subseteq I \land k \in (I ∖ x))) \to \forall y \in x ({H ↾}_{x}) (y) \in Cntz (G) (\{F (k)\})$
100		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)\}))$
101	70 99 100	sylanbrc	$⊢ (φ \land (x \subseteq I \land k \in (I ∖ x))) \to ({H ↾}_{x}) : x ⟶ Cntz (G) (\{F (k)\})$
102		resss	$⊢ {H ↾}_{x} \subseteq H$
103	102	rnssi	$⊢ ran ({H ↾}_{x}) \subseteq ran H$
104	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}))$
105	54 103 104	sylancl	$⊢ φ \to ran ({H ↾}_{x}) \subseteq Cntz (G) (ran ({H ↾}_{x}))$
106	105	adantr	$⊢ (φ \land (x \subseteq I \land k \in (I ∖ x))) \to ran ({H ↾}_{x}) \subseteq Cntz (G) (ran ({H ↾}_{x}))$
107	22 27	fsuppres	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (({H ↾}_{x}))$
108	107	adantr	$⊢ (φ \land (x \subseteq I \land k \in (I ∖ x))) \to {finSupp}_{\underset{˙}{0}} (({H ↾}_{x}))$
109	1 50 56 58 65 101 106 108	gsumzsubmcl	$⊢ (φ \land (x \subseteq I \land k \in (I ∖ x))) \to \sum_{G} ({H ↾}_{x}) \in Cntz (G) (\{F (k)\})$
110	109	snssd	$⊢ (φ \land (x \subseteq I \land k \in (I ∖ x))) \to \{\sum_{G} ({H ↾}_{x})\} \subseteq Cntz (G) (\{F (k)\})$
111	66 68	fssresd	$⊢ (φ \land (x \subseteq I \land k \in (I ∖ x))) \to ({H ↾}_{x}) : x ⟶ {Base}_{G}$
112	11 1 50 56 58 111 106 108	gsumzcl	$⊢ (φ \land (x \subseteq I \land k \in (I ∖ x))) \to \sum_{G} ({H ↾}_{x}) \in {Base}_{G}$
113	112	snssd	$⊢ (φ \land (x \subseteq I \land k \in (I ∖ x))) \to \{\sum_{G} ({H ↾}_{x})\} \subseteq {Base}_{G}$
114	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})\}))$
115	113 63 114	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})\}))$
116	110 115	mpbid	$⊢ (φ \land (x \subseteq I \land k \in (I ∖ x))) \to \{F (k)\} \subseteq Cntz (G) (\{\sum_{G} ({H ↾}_{x})\})$
117		fvex	$⊢ F (k) \in V$
118	117	snss	$⊢ F (k) \in Cntz (G) (\{\sum_{G} ({H ↾}_{x})\}) \leftrightarrow \{F (k)\} \subseteq Cntz (G) (\{\sum_{G} ({H ↾}_{x})\})$
119	116 118	sylibr	$⊢ (φ \land (x \subseteq I \land k \in (I ∖ x))) \to F (k) \in Cntz (G) (\{\sum_{G} ({H ↾}_{x})\})$
120	11 1 7 50 51 8 21 22 52 12 14 53 54 55 119	gsumzaddlem	$⊢ φ \to \sum_{G} (F {\underset{˙}{+}}_{f} H) = (\sum_{G}, F) \underset{˙}{+} (\sum_{G}, H)$
121	49 120	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