Theorem dpjid

Description: The key property of projections: the sum of all the projections of A is A . (Contributed by Mario Carneiro, 26-Apr-2016)

	Ref	Expression
Hypotheses	dpjfval.1	|- ( ph -> G dom DProd S )
	dpjfval.2	|- ( ph -> dom S = I )
	dpjfval.p	|- P = ( G dProj S )
	dpjid.3	|- ( ph -> A e. ( G DProd S ) )
Assertion	dpjid	|- ( ph -> A = ( G gsum ( x e. I |-> ( ( P ` x ) ` A ) ) ) )

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		dpjid.3	|- ( ph -> A e. ( G DProd S ) )
5		eqid	|- ( 0g ` G ) = ( 0g ` G )
6		eqid	|- { h e. X_ i e. I ( S ` i ) | h finSupp ( 0g ` G ) } = { h e. X_ i e. I ( S ` i ) | h finSupp ( 0g ` G ) }
7	1 2 3 4 5 6	dpjidcl	|- ( ph -> ( ( x e. I |-> ( ( P ` x ) ` A ) ) e. { h e. X_ i e. I ( S ` i ) | h finSupp ( 0g ` G ) } /\ A = ( G gsum ( x e. I |-> ( ( P ` x ) ` A ) ) ) ) )
8	7	simprd	|- ( ph -> A = ( G gsum ( x e. I |-> ( ( P ` x ) ` A ) ) ) )