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	$$⊢\phi \to G\mathrm{dom}\mathrm{DProd}S$$
	dpjfval.2	$$⊢\phi \to \mathrm{dom}S=I$$
	dpjfval.p	$$⊢P=G\mathrm{dProj}S$$
	dpjid.3	$$⊢\phi \to A\in \left(G\mathrm{DProd}S\right)$$
Assertion	dpjid	$$⊢\phi \to A=\underset{x\in I}{{\sum }_G}P\left(x\right)\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		dpjfval.1	$$⊢\phi \to G\mathrm{dom}\mathrm{DProd}S$$
2		dpjfval.2	$$⊢\phi \to \mathrm{dom}S=I$$
3		dpjfval.p	$$⊢P=G\mathrm{dProj}S$$
4		dpjid.3	$$⊢\phi \to A\in \left(G\mathrm{DProd}S\right)$$
5		eqid	$$⊢0_G=0_G$$
6		eqid	$$⊢\left\{h\in \underset{i\in I}{⨉}S\left(i\right)|{finSupp}_{0_G}\left(h\right)\right\}=\left\{h\in \underset{i\in I}{⨉}S\left(i\right)|{finSupp}_{0_G}\left(h\right)\right\}$$
7	1 2 3 4 5 6	dpjidcl	$$⊢\phi \to \left(\left(x\in I⟼P\left(x\right)\left(A\right)\right)\in \left\{h\in \underset{i\in I}{⨉}S\left(i\right)|{finSupp}_{0_G}\left(h\right)\right\}\wedge A=\underset{x\in I}{{\sum }_G}P\left(x\right)\left(A\right)\right)$$
8	7	simprd	$$⊢\phi \to A=\underset{x\in I}{{\sum }_G}P\left(x\right)\left(A\right)$$