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	⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
	dpjfval.2	⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
	dpjfval.p	⊢ 𝑃 = ( 𝐺 dProj 𝑆 )
	dpjidcl.3	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐺 DProd 𝑆 ) )
	dpjidcl.0	⊢ 0 = ( 0g ‘ 𝐺 )
	dpjidcl.w	⊢ 𝑊 = { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp 0 }
	dpjeq.c	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ 𝐶 ) ∈ 𝑊 )
Assertion	dpjeq	⊢ ( 𝜑 → ( 𝐴 = ( 𝐺 Σg ( 𝑥 ∈ 𝐼 ↦ 𝐶 ) ) ↔ ∀ 𝑥 ∈ 𝐼 ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) = 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		dpjfval.1	⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
2		dpjfval.2	⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
3		dpjfval.p	⊢ 𝑃 = ( 𝐺 dProj 𝑆 )
4		dpjidcl.3	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐺 DProd 𝑆 ) )
5		dpjidcl.0	⊢ 0 = ( 0g ‘ 𝐺 )
6		dpjidcl.w	⊢ 𝑊 = { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp 0 }
7		dpjeq.c	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ 𝐶 ) ∈ 𝑊 )
8	1 2 3 4 5 6	dpjidcl	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) ) ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) ) ) ) )
9	8	simprd	⊢ ( 𝜑 → 𝐴 = ( 𝐺 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) ) ) )
10	9	eqeq1d	⊢ ( 𝜑 → ( 𝐴 = ( 𝐺 Σg ( 𝑥 ∈ 𝐼 ↦ 𝐶 ) ) ↔ ( 𝐺 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) ) ) = ( 𝐺 Σg ( 𝑥 ∈ 𝐼 ↦ 𝐶 ) ) ) )
11	8	simpld	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) ) ∈ 𝑊 )
12	5 6 1 2 11 7	dprdf11	⊢ ( 𝜑 → ( ( 𝐺 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) ) ) = ( 𝐺 Σg ( 𝑥 ∈ 𝐼 ↦ 𝐶 ) ) ↔ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) ) = ( 𝑥 ∈ 𝐼 ↦ 𝐶 ) ) )
13		fvex	⊢ ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) ∈ V
14	13	rgenw	⊢ ∀ 𝑥 ∈ 𝐼 ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) ∈ V
15		mpteqb	⊢ ( ∀ 𝑥 ∈ 𝐼 ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) ∈ V → ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) ) = ( 𝑥 ∈ 𝐼 ↦ 𝐶 ) ↔ ∀ 𝑥 ∈ 𝐼 ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) = 𝐶 ) )
16	14 15	mp1i	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) ) = ( 𝑥 ∈ 𝐼 ↦ 𝐶 ) ↔ ∀ 𝑥 ∈ 𝐼 ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) = 𝐶 ) )
17	10 12 16	3bitrd	⊢ ( 𝜑 → ( 𝐴 = ( 𝐺 Σg ( 𝑥 ∈ 𝐼 ↦ 𝐶 ) ) ↔ ∀ 𝑥 ∈ 𝐼 ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) = 𝐶 ) )