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	⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
	dpjfval.2	⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
	dpjfval.p	⊢ 𝑃 = ( 𝐺 dProj 𝑆 )
	dpjid.3	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐺 DProd 𝑆 ) )
Assertion	dpjid	⊢ ( 𝜑 → 𝐴 = ( 𝐺 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		dpjfval.1	⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
2		dpjfval.2	⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
3		dpjfval.p	⊢ 𝑃 = ( 𝐺 dProj 𝑆 )
4		dpjid.3	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐺 DProd 𝑆 ) )
5		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
6		eqid	⊢ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } = { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) }
7	1 2 3 4 5 6	dpjidcl	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) ) ∈ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ∧ 𝐴 = ( 𝐺 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) ) ) ) )
8	7	simprd	⊢ ( 𝜑 → 𝐴 = ( 𝐺 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) ) ) )