Theorem 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	|- ( ph -> G dom DProd S )
	dpjfval.2	|- ( ph -> dom S = I )
	dpjfval.p	|- P = ( G dProj S )
	dpjidcl.3	|- ( ph -> A e. ( G DProd S ) )
	dpjidcl.0	|- .0. = ( 0g ` G )
	dpjidcl.w	|- W = { h e. X_ i e. I ( S ` i ) | h finSupp .0. }
	dpjeq.c	|- ( ph -> ( x e. I |-> C ) e. W )
Assertion	dpjeq	|- ( ph -> ( A = ( G gsum ( x e. I |-> C ) ) <-> A. x e. I ( ( P ` x ) ` A ) = C ) )

Proof

Step	Hyp	Ref	Expression
1		dpjfval.1	|- ( ph -> G dom DProd S )
2		dpjfval.2	|- ( ph -> dom S = I )
3		dpjfval.p	|- P = ( G dProj S )
4		dpjidcl.3	|- ( ph -> A e. ( G DProd S ) )
5		dpjidcl.0	|- .0. = ( 0g ` G )
6		dpjidcl.w	|- W = { h e. X_ i e. I ( S ` i ) | h finSupp .0. }
7		dpjeq.c	|- ( ph -> ( x e. I |-> C ) e. W )
8	1 2 3 4 5 6	dpjidcl	|- ( ph -> ( ( x e. I |-> ( ( P ` x ) ` A ) ) e. W /\ A = ( G gsum ( x e. I |-> ( ( P ` x ) ` A ) ) ) ) )
9	8	simprd	|- ( ph -> A = ( G gsum ( x e. I |-> ( ( P ` x ) ` A ) ) ) )
10	9	eqeq1d	|- ( ph -> ( A = ( G gsum ( x e. I |-> C ) ) <-> ( G gsum ( x e. I |-> ( ( P ` x ) ` A ) ) ) = ( G gsum ( x e. I |-> C ) ) ) )
11	8	simpld	|- ( ph -> ( x e. I |-> ( ( P ` x ) ` A ) ) e. W )
12	5 6 1 2 11 7	dprdf11	|- ( ph -> ( ( G gsum ( x e. I |-> ( ( P ` x ) ` A ) ) ) = ( G gsum ( x e. I |-> C ) ) <-> ( x e. I |-> ( ( P ` x ) ` A ) ) = ( x e. I |-> C ) ) )
13		fvex	|- ( ( P ` x ) ` A ) e. _V
14	13	rgenw	|- A. x e. I ( ( P ` x ) ` A ) e. _V
15		mpteqb	|- ( A. x e. I ( ( P ` x ) ` A ) e. _V -> ( ( x e. I |-> ( ( P ` x ) ` A ) ) = ( x e. I |-> C ) <-> A. x e. I ( ( P ` x ) ` A ) = C ) )
16	14 15	mp1i	|- ( ph -> ( ( x e. I |-> ( ( P ` x ) ` A ) ) = ( x e. I |-> C ) <-> A. x e. I ( ( P ` x ) ` A ) = C ) )
17	10 12 16	3bitrd	|- ( ph -> ( A = ( G gsum ( x e. I |-> C ) ) <-> A. x e. I ( ( P ` x ) ` A ) = C ) )