This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) ) )