dprdf11

Description: Two group sums over a direct product that give the same value are equal as functions. (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$
	dprdf11.4	$⊢ φ \to H \in W$
Assertion	dprdf11	$⊢ φ \to (\sum_{G} F = \sum_{G} H \leftrightarrow F = 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		dprdf11.4	$⊢ φ \to H \in W$
7		eqid	$⊢ {Base}_{G} = {Base}_{G}$
8	2 3 4 5 7	dprdff	$⊢ φ \to F : I ⟶ {Base}_{G}$
9	8	ffnd	$⊢ φ \to F Fn I$
10	2 3 4 6 7	dprdff	$⊢ φ \to H : I ⟶ {Base}_{G}$
11	10	ffnd	$⊢ φ \to H Fn I$
12		eqfnfv	$⊢ (F Fn I \land H Fn I) \to (F = H \leftrightarrow \forall x \in I F (x) = H (x))$
13	9 11 12	syl2anc	$⊢ φ \to (F = H \leftrightarrow \forall x \in I F (x) = H (x))$
14		eqid	$⊢ -_{G} = -_{G}$
15	1 2 3 4 5 6 14	dprdfsub	$⊢ φ \to (F {-_{G}}_{f} H \in W \land \sum_{G} (F {-_{G}}_{f} H) = (\sum_{G}, F) -_{G} (\sum_{G}, H))$
16	15	simpld	$⊢ φ \to F {-_{G}}_{f} H \in W$
17	1 2 3 4 16	dprdfeq0	$⊢ φ \to (\sum_{G} (F {-_{G}}_{f} H) = \underset{˙}{0} \leftrightarrow F {-_{G}}_{f} H = (x \in I ⟼ \underset{˙}{0}))$
18	15	simprd	$⊢ φ \to \sum_{G} (F {-_{G}}_{f} H) = (\sum_{G}, F) -_{G} (\sum_{G}, H)$
19	18	eqeq1d	$⊢ φ \to (\sum_{G} (F {-_{G}}_{f} H) = \underset{˙}{0} \leftrightarrow (\sum_{G}, F) -_{G} (\sum_{G}, H) = \underset{˙}{0})$
20	3 4	dprddomcld	$⊢ φ \to I \in V$
21		fvexd	$⊢ (φ \land x \in I) \to F (x) \in V$
22		fvexd	$⊢ (φ \land x \in I) \to H (x) \in V$
23	8	feqmptd	$⊢ φ \to F = (x \in I ⟼ F (x))$
24	10	feqmptd	$⊢ φ \to H = (x \in I ⟼ H (x))$
25	20 21 22 23 24	offval2	$⊢ φ \to F {-_{G}}_{f} H = (x \in I ⟼ F (x) -_{G} H (x))$
26	25	eqeq1d	$⊢ φ \to (F {-_{G}}_{f} H = (x \in I ⟼ \underset{˙}{0}) \leftrightarrow (x \in I ⟼ F (x) -_{G} H (x)) = (x \in I ⟼ \underset{˙}{0}))$
27		ovex	$⊢ F (x) -_{G} H (x) \in V$
28	27	rgenw	$⊢ \forall x \in I F (x) -_{G} H (x) \in V$
29		mpteqb	$⊢ \forall x \in I F (x) -_{G} H (x) \in V \to ((x \in I ⟼ F (x) -_{G} H (x)) = (x \in I ⟼ \underset{˙}{0}) \leftrightarrow \forall x \in I F (x) -_{G} H (x) = \underset{˙}{0})$
30	28 29	ax-mp	$⊢ (x \in I ⟼ F (x) -_{G} H (x)) = (x \in I ⟼ \underset{˙}{0}) \leftrightarrow \forall x \in I F (x) -_{G} H (x) = \underset{˙}{0}$
31		dprdgrp	$⊢ G dom DProd S \to G \in Grp$
32	3 31	syl	$⊢ φ \to G \in Grp$
33	32	adantr	$⊢ (φ \land x \in I) \to G \in Grp$
34	8	ffvelcdmda	$⊢ (φ \land x \in I) \to F (x) \in {Base}_{G}$
35	10	ffvelcdmda	$⊢ (φ \land x \in I) \to H (x) \in {Base}_{G}$
36	7 1 14	grpsubeq0	$⊢ (G \in Grp \land F (x) \in {Base}_{G} \land H (x) \in {Base}_{G}) \to (F (x) -_{G} H (x) = \underset{˙}{0} \leftrightarrow F (x) = H (x))$
37	33 34 35 36	syl3anc	$⊢ (φ \land x \in I) \to (F (x) -_{G} H (x) = \underset{˙}{0} \leftrightarrow F (x) = H (x))$
38	37	ralbidva	$⊢ φ \to (\forall x \in I F (x) -_{G} H (x) = \underset{˙}{0} \leftrightarrow \forall x \in I F (x) = H (x))$
39	30 38	bitrid	$⊢ φ \to ((x \in I ⟼ F (x) -_{G} H (x)) = (x \in I ⟼ \underset{˙}{0}) \leftrightarrow \forall x \in I F (x) = H (x))$
40	26 39	bitrd	$⊢ φ \to (F {-_{G}}_{f} H = (x \in I ⟼ \underset{˙}{0}) \leftrightarrow \forall x \in I F (x) = H (x))$
41	17 19 40	3bitr3d	$⊢ φ \to ((\sum_{G}, F) -_{G} (\sum_{G}, H) = \underset{˙}{0} \leftrightarrow \forall x \in I F (x) = H (x))$
42	7	dprdssv	$⊢ G DProd S \subseteq {Base}_{G}$
43	1 2 3 4 5	eldprdi	$⊢ φ \to \sum_{G} F \in (G DProd S)$
44	42 43	sselid	$⊢ φ \to \sum_{G} F \in {Base}_{G}$
45	1 2 3 4 6	eldprdi	$⊢ φ \to \sum_{G} H \in (G DProd S)$
46	42 45	sselid	$⊢ φ \to \sum_{G} H \in {Base}_{G}$
47	7 1 14	grpsubeq0	$⊢ (G \in Grp \land \sum_{G} F \in {Base}_{G} \land \sum_{G} H \in {Base}_{G}) \to ((\sum_{G}, F) -_{G} (\sum_{G}, H) = \underset{˙}{0} \leftrightarrow \sum_{G} F = \sum_{G} H)$
48	32 44 46 47	syl3anc	$⊢ φ \to ((\sum_{G}, F) -_{G} (\sum_{G}, H) = \underset{˙}{0} \leftrightarrow \sum_{G} F = \sum_{G} H)$
49	13 41 48	3bitr2rd	$⊢ φ \to (\sum_{G} F = \sum_{G} H \leftrightarrow F = H)$

Metamath Proof Explorer

Theorem dprdf11

Proof