Metamath Proof Explorer

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 ⊢ φ → G dom ⁡ DProd S
dpjfval.2 ⊢ φ → dom ⁡ S = I
dpjfval.p ⊢ P = G dProj S
dpjidcl.3 ⊢ φ → A ∈ G DProd S
dpjidcl.0 ⊢ 0 ˙ = 0 G
dpjidcl.w ⊢ W = h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 ˙⁡ h
dpjeq.c ⊢ φ → x ∈ I ⟼ C ∈ W
Assertion dpjeq ⊢ φ → A = ∑ G x ∈ I C ↔ ∀ x ∈ I P ⁡ x ⁡ A = C

Proof

Step Hyp Ref Expression
1 dpjfval.1 ⊢ φ → G dom ⁡ DProd S
2 dpjfval.2 ⊢ φ → dom ⁡ S = I
3 dpjfval.p ⊢ P = G dProj S
4 dpjidcl.3 ⊢ φ → A ∈ G DProd S
5 dpjidcl.0 ⊢ 0 ˙ = 0 G
6 dpjidcl.w ⊢ W = h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 ˙⁡ h
7 dpjeq.c ⊢ φ → x ∈ I ⟼ C ∈ W
8 1 2 3 4 5 6 dpjidcl ⊢ φ → x ∈ I ⟼ P ⁡ x ⁡ A ∈ W ∧ A = ∑ G x ∈ I P ⁡ x ⁡ A
9 8 simprd ⊢ φ → A = ∑ G x ∈ I P ⁡ x ⁡ A
10 9 eqeq1d ⊢ φ → A = ∑ G x ∈ I C ↔ ∑ G x ∈ I P ⁡ x ⁡ A = ∑ G x ∈ I C
11 8 simpld ⊢ φ → x ∈ I ⟼ P ⁡ x ⁡ A ∈ W
12 5 6 1 2 11 7 dprdf11 ⊢ φ → ∑ G x ∈ I P ⁡ x ⁡ A = ∑ G x ∈ I C ↔ x ∈ I ⟼ P ⁡ x ⁡ A = x ∈ I ⟼ C
13 fvex ⊢ P ⁡ x ⁡ A ∈ V
14 13 rgenw ⊢ ∀ x ∈ I P ⁡ x ⁡ A ∈ V
15 mpteqb ⊢ ∀ x ∈ I P ⁡ x ⁡ A ∈ V → x ∈ I ⟼ P ⁡ x ⁡ A = x ∈ I ⟼ C ↔ ∀ x ∈ I P ⁡ x ⁡ A = C
16 14 15 mp1i ⊢ φ → x ∈ I ⟼ P ⁡ x ⁡ A = x ∈ I ⟼ C ↔ ∀ x ∈ I P ⁡ x ⁡ A = C
17 10 12 16 3bitrd ⊢ φ → A = ∑ G x ∈ I C ↔ ∀ x ∈ I P ⁡ x ⁡ A = C