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 
|- ( ph -> G dom DProd S )
dpjfval.2 
|- ( ph -> dom S = I )
dpjfval.p 
|- P = ( G dProj S )
dpjidcl.3 
|- ( ph -> A e. ( G DProd S ) )
dpjidcl.0 
|- .0. = ( 0g ` G )
dpjidcl.w 
|- W = { h e. X_ i e. I ( S ` i ) | h finSupp .0. }
Assertion dpjidcl 
|- ( ph -> ( ( x e. I |-> ( ( P ` x ) ` A ) ) e. W /\ A = ( G gsum ( x e. I |-> ( ( P ` x ) ` A ) ) ) ) )

Proof

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