dpjeq

Description: Decompose a group sum into projections. (Contributed by Mario Carneiro, 26-Apr-2016) (Revised by AV, 14-Jul-2019)

	Ref	Expression
Hypotheses	dpjfval.1	$⊢ φ \to G dom DProd S$
	dpjfval.2	$⊢ φ \to dom S = I$
	dpjfval.p	$⊢ P = G dProj S$
	dpjidcl.3	$⊢ φ \to A \in (G DProd S)$
	dpjidcl.0	$⊢ \underset{˙}{0} = 0_{G}$
	dpjidcl.w	$⊢ W = \{h \in \underset{i \in I}{⨉} S (i) \| {finSupp}_{\underset{˙}{0}} (h)\}$
	dpjeq.c	$⊢ φ \to (x \in I ⟼ C) \in W$
Assertion	dpjeq	$⊢ φ \to (A = \underset{x \in I}{\sum_{G}} C \leftrightarrow \forall x \in I P (x) (A) = C)$

Step	Hyp	Ref	Expression
1		dpjfval.1	$⊢ φ \to G dom DProd S$
2		dpjfval.2	$⊢ φ \to dom S = I$
3		dpjfval.p	$⊢ P = G dProj S$
4		dpjidcl.3	$⊢ φ \to A \in (G DProd S)$
5		dpjidcl.0	$⊢ \underset{˙}{0} = 0_{G}$
6		dpjidcl.w	$⊢ W = \{h \in \underset{i \in I}{⨉} S (i) \| {finSupp}_{\underset{˙}{0}} (h)\}$
7		dpjeq.c	$⊢ φ \to (x \in I ⟼ C) \in W$
8	1 2 3 4 5 6	dpjidcl	$⊢ φ \to ((x \in I ⟼ P (x) (A)) \in W \land A = \underset{x \in I}{\sum_{G}} P (x) (A))$
9	8	simprd	$⊢ φ \to A = \underset{x \in I}{\sum_{G}} P (x) (A)$
10	9	eqeq1d	$⊢ φ \to (A = \underset{x \in I}{\sum_{G}} C \leftrightarrow \underset{x \in I}{\sum_{G}} P (x) (A) = \underset{x \in I}{\sum_{G}} C)$
11	8	simpld	$⊢ φ \to (x \in I ⟼ P (x) (A)) \in W$
12	5 6 1 2 11 7	dprdf11	$⊢ φ \to (\underset{x \in I}{\sum_{G}} P (x) (A) = \underset{x \in I}{\sum_{G}} C \leftrightarrow (x \in I ⟼ P (x) (A)) = (x \in I ⟼ C))$
13		fvex	$⊢ P (x) (A) \in V$
14	13	rgenw	$⊢ \forall x \in I P (x) (A) \in V$
15		mpteqb	$⊢ \forall x \in I P (x) (A) \in V \to ((x \in I ⟼ P (x) (A)) = (x \in I ⟼ C) \leftrightarrow \forall x \in I P (x) (A) = C)$
16	14 15	mp1i	$⊢ φ \to ((x \in I ⟼ P (x) (A)) = (x \in I ⟼ C) \leftrightarrow \forall x \in I P (x) (A) = C)$
17	10 12 16	3bitrd	$⊢ φ \to (A = \underset{x \in I}{\sum_{G}} C \leftrightarrow \forall x \in I P (x) (A) = C)$

Metamath Proof Explorer