# Metamath Proof Explorer

## Theorem dpjidcl

Description: The key property of projections: the sum of all the projections of A is A . (Contributed by Mario Carneiro, 26-Apr-2016) (Revised by AV, 14-Jul-2019)

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}$
dpjidcl.3 ${⊢}{\phi }\to {A}\in \left({G}\mathrm{DProd}{S}\right)$
dpjidcl.0
dpjidcl.w
Assertion dpjidcl ${⊢}{\phi }\to \left(\left({x}\in {I}⟼{P}\left({x}\right)\left({A}\right)\right)\in {W}\wedge {A}=\underset{{x}\in {I}}{{\sum }_{{G}}}{P}\left({x}\right)\left({A}\right)\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 dpjidcl.3 ${⊢}{\phi }\to {A}\in \left({G}\mathrm{DProd}{S}\right)$
5 dpjidcl.0
6 dpjidcl.w
7 5 6 eldprd ${⊢}\mathrm{dom}{S}={I}\to \left({A}\in \left({G}\mathrm{DProd}{S}\right)↔\left({G}\mathrm{dom}\mathrm{DProd}{S}\wedge \exists {f}\in {W}\phantom{\rule{.4em}{0ex}}{A}={\sum }_{{G}}{f}\right)\right)$
8 2 7 syl ${⊢}{\phi }\to \left({A}\in \left({G}\mathrm{DProd}{S}\right)↔\left({G}\mathrm{dom}\mathrm{DProd}{S}\wedge \exists {f}\in {W}\phantom{\rule{.4em}{0ex}}{A}={\sum }_{{G}}{f}\right)\right)$
9 4 8 mpbid ${⊢}{\phi }\to \left({G}\mathrm{dom}\mathrm{DProd}{S}\wedge \exists {f}\in {W}\phantom{\rule{.4em}{0ex}}{A}={\sum }_{{G}}{f}\right)$
10 9 simprd ${⊢}{\phi }\to \exists {f}\in {W}\phantom{\rule{.4em}{0ex}}{A}={\sum }_{{G}}{f}$
11 1 adantr ${⊢}\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\to {G}\mathrm{dom}\mathrm{DProd}{S}$
12 2 adantr ${⊢}\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\to \mathrm{dom}{S}={I}$
13 1 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\wedge {x}\in {I}\right)\to {G}\mathrm{dom}\mathrm{DProd}{S}$
14 2 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\wedge {x}\in {I}\right)\to \mathrm{dom}{S}={I}$
15 simpr ${⊢}\left(\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\wedge {x}\in {I}\right)\to {x}\in {I}$
16 13 14 3 15 dpjf ${⊢}\left(\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\wedge {x}\in {I}\right)\to {P}\left({x}\right):{G}\mathrm{DProd}{S}⟶{S}\left({x}\right)$
17 4 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\wedge {x}\in {I}\right)\to {A}\in \left({G}\mathrm{DProd}{S}\right)$
18 16 17 ffvelrnd ${⊢}\left(\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\wedge {x}\in {I}\right)\to {P}\left({x}\right)\left({A}\right)\in {S}\left({x}\right)$
19 1 2 dprddomcld ${⊢}{\phi }\to {I}\in \mathrm{V}$
20 19 mptexd ${⊢}{\phi }\to \left({x}\in {I}⟼{P}\left({x}\right)\left({A}\right)\right)\in \mathrm{V}$
21 20 adantr ${⊢}\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\to \left({x}\in {I}⟼{P}\left({x}\right)\left({A}\right)\right)\in \mathrm{V}$
22 funmpt ${⊢}\mathrm{Fun}\left({x}\in {I}⟼{P}\left({x}\right)\left({A}\right)\right)$
23 22 a1i ${⊢}\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\to \mathrm{Fun}\left({x}\in {I}⟼{P}\left({x}\right)\left({A}\right)\right)$
24 simprl ${⊢}\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\to {f}\in {W}$
25 6 11 12 24 dprdffsupp
26 eldifi
27 eqid ${⊢}{proj}_{1}\left({G}\right)={proj}_{1}\left({G}\right)$
28 13 14 3 27 15 dpjval ${⊢}\left(\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\wedge {x}\in {I}\right)\to {P}\left({x}\right)={S}\left({x}\right){proj}_{1}\left({G}\right)\left({G}\mathrm{DProd}\left({{S}↾}_{\left({I}\setminus \left\{{x}\right\}\right)}\right)\right)$
29 28 fveq1d ${⊢}\left(\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\wedge {x}\in {I}\right)\to {P}\left({x}\right)\left({A}\right)=\left({S}\left({x}\right){proj}_{1}\left({G}\right)\left({G}\mathrm{DProd}\left({{S}↾}_{\left({I}\setminus \left\{{x}\right\}\right)}\right)\right)\right)\left({A}\right)$
30 26 29 sylan2
31 simplrr
32 eqid ${⊢}{\mathrm{Base}}_{{G}}={\mathrm{Base}}_{{G}}$
33 eqid ${⊢}\mathrm{Cntz}\left({G}\right)=\mathrm{Cntz}\left({G}\right)$
34 dprdgrp ${⊢}{G}\mathrm{dom}\mathrm{DProd}{S}\to {G}\in \mathrm{Grp}$
35 grpmnd ${⊢}{G}\in \mathrm{Grp}\to {G}\in \mathrm{Mnd}$
36 11 34 35 3syl ${⊢}\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\to {G}\in \mathrm{Mnd}$
39 6 11 12 24 32 dprdff ${⊢}\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\to {f}:{I}⟶{\mathrm{Base}}_{{G}}$
41 24 adantr ${⊢}\left(\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\wedge {x}\in {I}\right)\to {f}\in {W}$
42 6 13 14 41 33 dprdfcntz ${⊢}\left(\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\wedge {x}\in {I}\right)\to \mathrm{ran}{f}\subseteq \mathrm{Cntz}\left({G}\right)\left(\mathrm{ran}{f}\right)$
43 26 42 sylan2
44 snssi
46 45 difss2d
47 suppssdm
48 47 39 fssdm
50 ssconb
51 46 49 50 syl2anc
52 45 51 mpbid
54 32 5 33 37 38 40 43 52 53 gsumzres
55 31 54 eqtr4d
56 eqid
57 difss ${⊢}{I}\setminus \left\{{x}\right\}\subseteq {I}$
58 57 a1i ${⊢}\left(\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\wedge {x}\in {I}\right)\to {I}\setminus \left\{{x}\right\}\subseteq {I}$
59 13 14 58 dprdres ${⊢}\left(\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\wedge {x}\in {I}\right)\to \left({G}\mathrm{dom}\mathrm{DProd}\left({{S}↾}_{\left({I}\setminus \left\{{x}\right\}\right)}\right)\wedge {G}\mathrm{DProd}\left({{S}↾}_{\left({I}\setminus \left\{{x}\right\}\right)}\right)\subseteq {G}\mathrm{DProd}{S}\right)$
60 59 simpld ${⊢}\left(\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\wedge {x}\in {I}\right)\to {G}\mathrm{dom}\mathrm{DProd}\left({{S}↾}_{\left({I}\setminus \left\{{x}\right\}\right)}\right)$
61 13 14 dprdf2 ${⊢}\left(\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\wedge {x}\in {I}\right)\to {S}:{I}⟶\mathrm{SubGrp}\left({G}\right)$
62 fssres ${⊢}\left({S}:{I}⟶\mathrm{SubGrp}\left({G}\right)\wedge {I}\setminus \left\{{x}\right\}\subseteq {I}\right)\to \left({{S}↾}_{\left({I}\setminus \left\{{x}\right\}\right)}\right):{I}\setminus \left\{{x}\right\}⟶\mathrm{SubGrp}\left({G}\right)$
63 61 57 62 sylancl ${⊢}\left(\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\wedge {x}\in {I}\right)\to \left({{S}↾}_{\left({I}\setminus \left\{{x}\right\}\right)}\right):{I}\setminus \left\{{x}\right\}⟶\mathrm{SubGrp}\left({G}\right)$
64 63 fdmd ${⊢}\left(\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\wedge {x}\in {I}\right)\to \mathrm{dom}\left({{S}↾}_{\left({I}\setminus \left\{{x}\right\}\right)}\right)={I}\setminus \left\{{x}\right\}$
65 39 adantr ${⊢}\left(\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\wedge {x}\in {I}\right)\to {f}:{I}⟶{\mathrm{Base}}_{{G}}$
66 65 feqmptd ${⊢}\left(\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\wedge {x}\in {I}\right)\to {f}=\left({k}\in {I}⟼{f}\left({k}\right)\right)$
67 66 reseq1d ${⊢}\left(\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\wedge {x}\in {I}\right)\to {{f}↾}_{\left({I}\setminus \left\{{x}\right\}\right)}={\left({k}\in {I}⟼{f}\left({k}\right)\right)↾}_{\left({I}\setminus \left\{{x}\right\}\right)}$
68 resmpt ${⊢}{I}\setminus \left\{{x}\right\}\subseteq {I}\to {\left({k}\in {I}⟼{f}\left({k}\right)\right)↾}_{\left({I}\setminus \left\{{x}\right\}\right)}=\left({k}\in \left({I}\setminus \left\{{x}\right\}\right)⟼{f}\left({k}\right)\right)$
69 57 68 ax-mp ${⊢}{\left({k}\in {I}⟼{f}\left({k}\right)\right)↾}_{\left({I}\setminus \left\{{x}\right\}\right)}=\left({k}\in \left({I}\setminus \left\{{x}\right\}\right)⟼{f}\left({k}\right)\right)$
70 67 69 syl6eq ${⊢}\left(\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\wedge {x}\in {I}\right)\to {{f}↾}_{\left({I}\setminus \left\{{x}\right\}\right)}=\left({k}\in \left({I}\setminus \left\{{x}\right\}\right)⟼{f}\left({k}\right)\right)$
71 eldifi ${⊢}{k}\in \left({I}\setminus \left\{{x}\right\}\right)\to {k}\in {I}$
72 6 13 14 41 dprdfcl ${⊢}\left(\left(\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\wedge {x}\in {I}\right)\wedge {k}\in {I}\right)\to {f}\left({k}\right)\in {S}\left({k}\right)$
73 71 72 sylan2 ${⊢}\left(\left(\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\wedge {x}\in {I}\right)\wedge {k}\in \left({I}\setminus \left\{{x}\right\}\right)\right)\to {f}\left({k}\right)\in {S}\left({k}\right)$
74 fvres ${⊢}{k}\in \left({I}\setminus \left\{{x}\right\}\right)\to \left({{S}↾}_{\left({I}\setminus \left\{{x}\right\}\right)}\right)\left({k}\right)={S}\left({k}\right)$
75 74 adantl ${⊢}\left(\left(\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\wedge {x}\in {I}\right)\wedge {k}\in \left({I}\setminus \left\{{x}\right\}\right)\right)\to \left({{S}↾}_{\left({I}\setminus \left\{{x}\right\}\right)}\right)\left({k}\right)={S}\left({k}\right)$
76 73 75 eleqtrrd ${⊢}\left(\left(\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\wedge {x}\in {I}\right)\wedge {k}\in \left({I}\setminus \left\{{x}\right\}\right)\right)\to {f}\left({k}\right)\in \left({{S}↾}_{\left({I}\setminus \left\{{x}\right\}\right)}\right)\left({k}\right)$
77 difexg ${⊢}{I}\in \mathrm{V}\to {I}\setminus \left\{{x}\right\}\in \mathrm{V}$
78 19 77 syl ${⊢}{\phi }\to {I}\setminus \left\{{x}\right\}\in \mathrm{V}$
79 78 mptexd ${⊢}{\phi }\to \left({k}\in \left({I}\setminus \left\{{x}\right\}\right)⟼{f}\left({k}\right)\right)\in \mathrm{V}$
80 79 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\wedge {x}\in {I}\right)\to \left({k}\in \left({I}\setminus \left\{{x}\right\}\right)⟼{f}\left({k}\right)\right)\in \mathrm{V}$
81 funmpt ${⊢}\mathrm{Fun}\left({k}\in \left({I}\setminus \left\{{x}\right\}\right)⟼{f}\left({k}\right)\right)$
82 81 a1i ${⊢}\left(\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\wedge {x}\in {I}\right)\to \mathrm{Fun}\left({k}\in \left({I}\setminus \left\{{x}\right\}\right)⟼{f}\left({k}\right)\right)$
84 ssdif
85 57 84 ax-mp
86 85 sseli
87 ssidd
88 19 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\wedge {x}\in {I}\right)\to {I}\in \mathrm{V}$
89 5 fvexi
90 89 a1i
91 65 87 88 90 suppssr
92 86 91 sylan2
93 78 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\wedge {x}\in {I}\right)\to {I}\setminus \left\{{x}\right\}\in \mathrm{V}$
94 92 93 suppss2
95 fsuppsssupp
96 80 82 83 94 95 syl22anc
97 56 60 64 76 96 dprdwd
98 70 97 eqeltrd
99 5 56 60 64 98 eldprdi ${⊢}\left(\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\wedge {x}\in {I}\right)\to {\sum }_{{G}}\left({{f}↾}_{\left({I}\setminus \left\{{x}\right\}\right)}\right)\in \left({G}\mathrm{DProd}\left({{S}↾}_{\left({I}\setminus \left\{{x}\right\}\right)}\right)\right)$
100 26 99 sylan2
101 55 100 eqeltrd
102 eqid ${⊢}{+}_{{G}}={+}_{{G}}$
103 eqid ${⊢}\mathrm{LSSum}\left({G}\right)=\mathrm{LSSum}\left({G}\right)$
104 61 15 ffvelrnd ${⊢}\left(\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\wedge {x}\in {I}\right)\to {S}\left({x}\right)\in \mathrm{SubGrp}\left({G}\right)$
105 dprdsubg ${⊢}{G}\mathrm{dom}\mathrm{DProd}\left({{S}↾}_{\left({I}\setminus \left\{{x}\right\}\right)}\right)\to {G}\mathrm{DProd}\left({{S}↾}_{\left({I}\setminus \left\{{x}\right\}\right)}\right)\in \mathrm{SubGrp}\left({G}\right)$
106 60 105 syl ${⊢}\left(\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\wedge {x}\in {I}\right)\to {G}\mathrm{DProd}\left({{S}↾}_{\left({I}\setminus \left\{{x}\right\}\right)}\right)\in \mathrm{SubGrp}\left({G}\right)$
107 13 14 15 5 dpjdisj
108 13 14 15 33 dpjcntz ${⊢}\left(\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\wedge {x}\in {I}\right)\to {S}\left({x}\right)\subseteq \mathrm{Cntz}\left({G}\right)\left({G}\mathrm{DProd}\left({{S}↾}_{\left({I}\setminus \left\{{x}\right\}\right)}\right)\right)$
109 102 103 5 33 104 106 107 108 27 pj1rid
110 26 109 sylanl2
111 101 110 mpdan
112 30 111 eqtrd
113 19 adantr ${⊢}\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\to {I}\in \mathrm{V}$
114 112 113 suppss2
115 fsuppsssupp
116 21 23 25 114 115 syl22anc
117 6 11 12 18 116 dprdwd ${⊢}\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\to \left({x}\in {I}⟼{P}\left({x}\right)\left({A}\right)\right)\in {W}$
118 simprr ${⊢}\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\to {A}={\sum }_{{G}}{f}$
119 39 feqmptd ${⊢}\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\to {f}=\left({x}\in {I}⟼{f}\left({x}\right)\right)$
120 simplrr ${⊢}\left(\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\wedge {x}\in {I}\right)\to {A}={\sum }_{{G}}{f}$
121 13 34 35 3syl ${⊢}\left(\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\wedge {x}\in {I}\right)\to {G}\in \mathrm{Mnd}$
122 6 13 14 41 dprdffsupp
123 disjdif ${⊢}\left\{{x}\right\}\cap \left({I}\setminus \left\{{x}\right\}\right)=\varnothing$
124 123 a1i ${⊢}\left(\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\wedge {x}\in {I}\right)\to \left\{{x}\right\}\cap \left({I}\setminus \left\{{x}\right\}\right)=\varnothing$
125 undif2 ${⊢}\left\{{x}\right\}\cup \left({I}\setminus \left\{{x}\right\}\right)=\left\{{x}\right\}\cup {I}$
126 15 snssd ${⊢}\left(\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\wedge {x}\in {I}\right)\to \left\{{x}\right\}\subseteq {I}$
127 ssequn1 ${⊢}\left\{{x}\right\}\subseteq {I}↔\left\{{x}\right\}\cup {I}={I}$
128 126 127 sylib ${⊢}\left(\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\wedge {x}\in {I}\right)\to \left\{{x}\right\}\cup {I}={I}$
129 125 128 syl5req ${⊢}\left(\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\wedge {x}\in {I}\right)\to {I}=\left\{{x}\right\}\cup \left({I}\setminus \left\{{x}\right\}\right)$
130 32 5 102 33 121 88 65 42 122 124 129 gsumzsplit ${⊢}\left(\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\wedge {x}\in {I}\right)\to {\sum }_{{G}}{f}=\left({\sum }_{{G}},\left({{f}↾}_{\left\{{x}\right\}}\right)\right){+}_{{G}}\left({\sum }_{{G}},\left({{f}↾}_{\left({I}\setminus \left\{{x}\right\}\right)}\right)\right)$
131 65 126 feqresmpt ${⊢}\left(\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\wedge {x}\in {I}\right)\to {{f}↾}_{\left\{{x}\right\}}=\left({k}\in \left\{{x}\right\}⟼{f}\left({k}\right)\right)$
132 131 oveq2d ${⊢}\left(\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\wedge {x}\in {I}\right)\to {\sum }_{{G}}\left({{f}↾}_{\left\{{x}\right\}}\right)=\underset{{k}\in \left\{{x}\right\}}{{\sum }_{{G}}}{f}\left({k}\right)$
133 65 15 ffvelrnd ${⊢}\left(\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\wedge {x}\in {I}\right)\to {f}\left({x}\right)\in {\mathrm{Base}}_{{G}}$
134 fveq2 ${⊢}{k}={x}\to {f}\left({k}\right)={f}\left({x}\right)$
135 32 134 gsumsn ${⊢}\left({G}\in \mathrm{Mnd}\wedge {x}\in {I}\wedge {f}\left({x}\right)\in {\mathrm{Base}}_{{G}}\right)\to \underset{{k}\in \left\{{x}\right\}}{{\sum }_{{G}}}{f}\left({k}\right)={f}\left({x}\right)$
136 121 15 133 135 syl3anc ${⊢}\left(\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\wedge {x}\in {I}\right)\to \underset{{k}\in \left\{{x}\right\}}{{\sum }_{{G}}}{f}\left({k}\right)={f}\left({x}\right)$
137 132 136 eqtrd ${⊢}\left(\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\wedge {x}\in {I}\right)\to {\sum }_{{G}}\left({{f}↾}_{\left\{{x}\right\}}\right)={f}\left({x}\right)$
138 137 oveq1d ${⊢}\left(\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\wedge {x}\in {I}\right)\to \left({\sum }_{{G}},\left({{f}↾}_{\left\{{x}\right\}}\right)\right){+}_{{G}}\left({\sum }_{{G}},\left({{f}↾}_{\left({I}\setminus \left\{{x}\right\}\right)}\right)\right)={f}\left({x}\right){+}_{{G}}\left({\sum }_{{G}},\left({{f}↾}_{\left({I}\setminus \left\{{x}\right\}\right)}\right)\right)$
139 120 130 138 3eqtrd ${⊢}\left(\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\wedge {x}\in {I}\right)\to {A}={f}\left({x}\right){+}_{{G}}\left({\sum }_{{G}},\left({{f}↾}_{\left({I}\setminus \left\{{x}\right\}\right)}\right)\right)$
140 13 14 15 103 dpjlsm ${⊢}\left(\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\wedge {x}\in {I}\right)\to {G}\mathrm{DProd}{S}={S}\left({x}\right)\mathrm{LSSum}\left({G}\right)\left({G}\mathrm{DProd}\left({{S}↾}_{\left({I}\setminus \left\{{x}\right\}\right)}\right)\right)$
141 17 140 eleqtrd ${⊢}\left(\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\wedge {x}\in {I}\right)\to {A}\in \left({S}\left({x}\right)\mathrm{LSSum}\left({G}\right)\left({G}\mathrm{DProd}\left({{S}↾}_{\left({I}\setminus \left\{{x}\right\}\right)}\right)\right)\right)$
142 6 11 12 24 dprdfcl ${⊢}\left(\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\wedge {x}\in {I}\right)\to {f}\left({x}\right)\in {S}\left({x}\right)$
143 102 103 5 33 104 106 107 108 27 141 142 99 pj1eq ${⊢}\left(\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\wedge {x}\in {I}\right)\to \left({A}={f}\left({x}\right){+}_{{G}}\left({\sum }_{{G}},\left({{f}↾}_{\left({I}\setminus \left\{{x}\right\}\right)}\right)\right)↔\left(\left({S}\left({x}\right){proj}_{1}\left({G}\right)\left({G}\mathrm{DProd}\left({{S}↾}_{\left({I}\setminus \left\{{x}\right\}\right)}\right)\right)\right)\left({A}\right)={f}\left({x}\right)\wedge \left(\left({G}\mathrm{DProd}\left({{S}↾}_{\left({I}\setminus \left\{{x}\right\}\right)}\right)\right){proj}_{1}\left({G}\right){S}\left({x}\right)\right)\left({A}\right)={\sum }_{{G}}\left({{f}↾}_{\left({I}\setminus \left\{{x}\right\}\right)}\right)\right)\right)$
144 139 143 mpbid ${⊢}\left(\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\wedge {x}\in {I}\right)\to \left(\left({S}\left({x}\right){proj}_{1}\left({G}\right)\left({G}\mathrm{DProd}\left({{S}↾}_{\left({I}\setminus \left\{{x}\right\}\right)}\right)\right)\right)\left({A}\right)={f}\left({x}\right)\wedge \left(\left({G}\mathrm{DProd}\left({{S}↾}_{\left({I}\setminus \left\{{x}\right\}\right)}\right)\right){proj}_{1}\left({G}\right){S}\left({x}\right)\right)\left({A}\right)={\sum }_{{G}}\left({{f}↾}_{\left({I}\setminus \left\{{x}\right\}\right)}\right)\right)$
145 144 simpld ${⊢}\left(\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\wedge {x}\in {I}\right)\to \left({S}\left({x}\right){proj}_{1}\left({G}\right)\left({G}\mathrm{DProd}\left({{S}↾}_{\left({I}\setminus \left\{{x}\right\}\right)}\right)\right)\right)\left({A}\right)={f}\left({x}\right)$
146 29 145 eqtrd ${⊢}\left(\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\wedge {x}\in {I}\right)\to {P}\left({x}\right)\left({A}\right)={f}\left({x}\right)$
147 146 mpteq2dva ${⊢}\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\to \left({x}\in {I}⟼{P}\left({x}\right)\left({A}\right)\right)=\left({x}\in {I}⟼{f}\left({x}\right)\right)$
148 119 147 eqtr4d ${⊢}\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\to {f}=\left({x}\in {I}⟼{P}\left({x}\right)\left({A}\right)\right)$
149 148 oveq2d ${⊢}\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\to {\sum }_{{G}}{f}=\underset{{x}\in {I}}{{\sum }_{{G}}}{P}\left({x}\right)\left({A}\right)$
150 118 149 eqtrd ${⊢}\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\to {A}=\underset{{x}\in {I}}{{\sum }_{{G}}}{P}\left({x}\right)\left({A}\right)$
151 117 150 jca ${⊢}\left({\phi }\wedge \left({f}\in {W}\wedge {A}={\sum }_{{G}}{f}\right)\right)\to \left(\left({x}\in {I}⟼{P}\left({x}\right)\left({A}\right)\right)\in {W}\wedge {A}=\underset{{x}\in {I}}{{\sum }_{{G}}}{P}\left({x}\right)\left({A}\right)\right)$
152 10 151 rexlimddv ${⊢}{\phi }\to \left(\left({x}\in {I}⟼{P}\left({x}\right)\left({A}\right)\right)\in {W}\wedge {A}=\underset{{x}\in {I}}{{\sum }_{{G}}}{P}\left({x}\right)\left({A}\right)\right)$