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 ⊢ φ → G dom ⁡ DProd S
dpjfval.2 ⊢ φ → dom ⁡ S = I
dpjfval.p ⊢ P = G dProj S
dpjid.3 ⊢ φ → A ∈ G DProd S
Assertion dpjid ⊢ φ → A = ∑ G x ∈ I P ⁡ x ⁡ A

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 dpjid.3 ⊢ φ → A ∈ G DProd S
5 eqid ⊢ 0 G = 0 G
6 eqid ⊢ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 G⁡ h = h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 G⁡ h
7 1 2 3 4 5 6 dpjidcl ⊢ φ → x ∈ I ⟼ P ⁡ x ⁡ A ∈ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 G⁡ h ∧ A = ∑ G x ∈ I P ⁡ x ⁡ A
8 7 simprd ⊢ φ → A = ∑ G x ∈ I P ⁡ x ⁡ A