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 19 difexd 
 |-  ( ph -> ( I \ { x } ) e. _V )
78 77 mptexd 
 |-  ( ph -> ( k e. ( I \ { x } ) |-> ( f ` k ) ) e. _V )
79 78 ad2antrr 
 |-  ( ( ( ph /\ ( f e. W /\ A = ( G gsum f ) ) ) /\ x e. I ) -> ( k e. ( I \ { x } ) |-> ( f ` k ) ) e. _V )
80 funmpt 
 |-  Fun ( k e. ( I \ { x } ) |-> ( f ` k ) )
81 80 a1i 
 |-  ( ( ( ph /\ ( f e. W /\ A = ( G gsum f ) ) ) /\ x e. I ) -> Fun ( k e. ( I \ { x } ) |-> ( f ` k ) ) )
82 25 adantr 
 |-  ( ( ( ph /\ ( f e. W /\ A = ( G gsum f ) ) ) /\ x e. I ) -> f finSupp .0. )
83 ssdif 
 |-  ( ( I \ { x } ) C_ I -> ( ( I \ { x } ) \ ( f supp .0. ) ) C_ ( I \ ( f supp .0. ) ) )
84 57 83 ax-mp 
 |-  ( ( I \ { x } ) \ ( f supp .0. ) ) C_ ( I \ ( f supp .0. ) )
85 84 sseli 
 |-  ( k e. ( ( I \ { x } ) \ ( f supp .0. ) ) -> k e. ( I \ ( f supp .0. ) ) )
86 ssidd 
 |-  ( ( ( ph /\ ( f e. W /\ A = ( G gsum f ) ) ) /\ x e. I ) -> ( f supp .0. ) C_ ( f supp .0. ) )
87 19 ad2antrr 
 |-  ( ( ( ph /\ ( f e. W /\ A = ( G gsum f ) ) ) /\ x e. I ) -> I e. _V )
88 5 fvexi 
 |-  .0. e. _V
89 88 a1i 
 |-  ( ( ( ph /\ ( f e. W /\ A = ( G gsum f ) ) ) /\ x e. I ) -> .0. e. _V )
90 65 86 87 89 suppssr 
 |-  ( ( ( ( ph /\ ( f e. W /\ A = ( G gsum f ) ) ) /\ x e. I ) /\ k e. ( I \ ( f supp .0. ) ) ) -> ( f ` k ) = .0. )
91 85 90 sylan2 
 |-  ( ( ( ( ph /\ ( f e. W /\ A = ( G gsum f ) ) ) /\ x e. I ) /\ k e. ( ( I \ { x } ) \ ( f supp .0. ) ) ) -> ( f ` k ) = .0. )
92 77 ad2antrr 
 |-  ( ( ( ph /\ ( f e. W /\ A = ( G gsum f ) ) ) /\ x e. I ) -> ( I \ { x } ) e. _V )
93 91 92 suppss2 
 |-  ( ( ( ph /\ ( f e. W /\ A = ( G gsum f ) ) ) /\ x e. I ) -> ( ( k e. ( I \ { x } ) |-> ( f ` k ) ) supp .0. ) C_ ( f supp .0. ) )
94 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. )
95 79 81 82 93 94 syl22anc 
 |-  ( ( ( ph /\ ( f e. W /\ A = ( G gsum f ) ) ) /\ x e. I ) -> ( k e. ( I \ { x } ) |-> ( f ` k ) ) finSupp .0. )
96 56 60 64 76 95 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. } )
97 70 96 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. } )
98 5 56 60 64 97 eldprdi 
 |-  ( ( ( ph /\ ( f e. W /\ A = ( G gsum f ) ) ) /\ x e. I ) -> ( G gsum ( f |` ( I \ { x } ) ) ) e. ( G DProd ( S |` ( I \ { x } ) ) ) )
99 26 98 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 } ) ) ) )
100 55 99 eqeltrd 
 |-  ( ( ( ph /\ ( f e. W /\ A = ( G gsum f ) ) ) /\ x e. ( I \ ( f supp .0. ) ) ) -> A e. ( G DProd ( S |` ( I \ { x } ) ) ) )
101 eqid 
 |-  ( +g ` G ) = ( +g ` G )
102 eqid 
 |-  ( LSSum ` G ) = ( LSSum ` G )
103 61 15 ffvelrnd 
 |-  ( ( ( ph /\ ( f e. W /\ A = ( G gsum f ) ) ) /\ x e. I ) -> ( S ` x ) e. ( SubGrp ` G ) )
104 dprdsubg 
 |-  ( G dom DProd ( S |` ( I \ { x } ) ) -> ( G DProd ( S |` ( I \ { x } ) ) ) e. ( SubGrp ` G ) )
105 60 104 syl 
 |-  ( ( ( ph /\ ( f e. W /\ A = ( G gsum f ) ) ) /\ x e. I ) -> ( G DProd ( S |` ( I \ { x } ) ) ) e. ( SubGrp ` G ) )
106 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. } )
107 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 } ) ) ) ) )
108 101 102 5 33 103 105 106 107 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. )
109 26 108 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. )
110 100 109 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. )
111 30 110 eqtrd 
 |-  ( ( ( ph /\ ( f e. W /\ A = ( G gsum f ) ) ) /\ x e. ( I \ ( f supp .0. ) ) ) -> ( ( P ` x ) ` A ) = .0. )
112 19 adantr 
 |-  ( ( ph /\ ( f e. W /\ A = ( G gsum f ) ) ) -> I e. _V )
113 111 112 suppss2 
 |-  ( ( ph /\ ( f e. W /\ A = ( G gsum f ) ) ) -> ( ( x e. I |-> ( ( P ` x ) ` A ) ) supp .0. ) C_ ( f supp .0. ) )
114 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. )
115 21 23 25 113 114 syl22anc 
 |-  ( ( ph /\ ( f e. W /\ A = ( G gsum f ) ) ) -> ( x e. I |-> ( ( P ` x ) ` A ) ) finSupp .0. )
116 6 11 12 18 115 dprdwd 
 |-  ( ( ph /\ ( f e. W /\ A = ( G gsum f ) ) ) -> ( x e. I |-> ( ( P ` x ) ` A ) ) e. W )
117 simprr 
 |-  ( ( ph /\ ( f e. W /\ A = ( G gsum f ) ) ) -> A = ( G gsum f ) )
118 39 feqmptd 
 |-  ( ( ph /\ ( f e. W /\ A = ( G gsum f ) ) ) -> f = ( x e. I |-> ( f ` x ) ) )
119 simplrr 
 |-  ( ( ( ph /\ ( f e. W /\ A = ( G gsum f ) ) ) /\ x e. I ) -> A = ( G gsum f ) )
120 13 34 35 3syl 
 |-  ( ( ( ph /\ ( f e. W /\ A = ( G gsum f ) ) ) /\ x e. I ) -> G e. Mnd )
121 6 13 14 41 dprdffsupp 
 |-  ( ( ( ph /\ ( f e. W /\ A = ( G gsum f ) ) ) /\ x e. I ) -> f finSupp .0. )
122 disjdif 
 |-  ( { x } i^i ( I \ { x } ) ) = (/)
123 122 a1i 
 |-  ( ( ( ph /\ ( f e. W /\ A = ( G gsum f ) ) ) /\ x e. I ) -> ( { x } i^i ( I \ { x } ) ) = (/) )
124 undif2 
 |-  ( { x } u. ( I \ { x } ) ) = ( { x } u. I )
125 15 snssd 
 |-  ( ( ( ph /\ ( f e. W /\ A = ( G gsum f ) ) ) /\ x e. I ) -> { x } C_ I )
126 ssequn1 
 |-  ( { x } C_ I <-> ( { x } u. I ) = I )
127 125 126 sylib 
 |-  ( ( ( ph /\ ( f e. W /\ A = ( G gsum f ) ) ) /\ x e. I ) -> ( { x } u. I ) = I )
128 124 127 eqtr2id 
 |-  ( ( ( ph /\ ( f e. W /\ A = ( G gsum f ) ) ) /\ x e. I ) -> I = ( { x } u. ( I \ { x } ) ) )
129 32 5 101 33 120 87 65 42 121 123 128 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 } ) ) ) ) )
130 65 125 feqresmpt 
 |-  ( ( ( ph /\ ( f e. W /\ A = ( G gsum f ) ) ) /\ x e. I ) -> ( f |` { x } ) = ( k e. { x } |-> ( f ` k ) ) )
131 130 oveq2d 
 |-  ( ( ( ph /\ ( f e. W /\ A = ( G gsum f ) ) ) /\ x e. I ) -> ( G gsum ( f |` { x } ) ) = ( G gsum ( k e. { x } |-> ( f ` k ) ) ) )
132 65 15 ffvelrnd 
 |-  ( ( ( ph /\ ( f e. W /\ A = ( G gsum f ) ) ) /\ x e. I ) -> ( f ` x ) e. ( Base ` G ) )
133 fveq2 
 |-  ( k = x -> ( f ` k ) = ( f ` x ) )
134 32 133 gsumsn 
 |-  ( ( G e. Mnd /\ x e. I /\ ( f ` x ) e. ( Base ` G ) ) -> ( G gsum ( k e. { x } |-> ( f ` k ) ) ) = ( f ` x ) )
135 120 15 132 134 syl3anc 
 |-  ( ( ( ph /\ ( f e. W /\ A = ( G gsum f ) ) ) /\ x e. I ) -> ( G gsum ( k e. { x } |-> ( f ` k ) ) ) = ( f ` x ) )
136 131 135 eqtrd 
 |-  ( ( ( ph /\ ( f e. W /\ A = ( G gsum f ) ) ) /\ x e. I ) -> ( G gsum ( f |` { x } ) ) = ( f ` x ) )
137 136 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 } ) ) ) ) )
138 119 129 137 3eqtrd 
 |-  ( ( ( ph /\ ( f e. W /\ A = ( G gsum f ) ) ) /\ x e. I ) -> A = ( ( f ` x ) ( +g ` G ) ( G gsum ( f |` ( I \ { x } ) ) ) ) )
139 13 14 15 102 dpjlsm 
 |-  ( ( ( ph /\ ( f e. W /\ A = ( G gsum f ) ) ) /\ x e. I ) -> ( G DProd S ) = ( ( S ` x ) ( LSSum ` G ) ( G DProd ( S |` ( I \ { x } ) ) ) ) )
140 17 139 eleqtrd 
 |-  ( ( ( ph /\ ( f e. W /\ A = ( G gsum f ) ) ) /\ x e. I ) -> A e. ( ( S ` x ) ( LSSum ` G ) ( G DProd ( S |` ( I \ { x } ) ) ) ) )
141 6 11 12 24 dprdfcl 
 |-  ( ( ( ph /\ ( f e. W /\ A = ( G gsum f ) ) ) /\ x e. I ) -> ( f ` x ) e. ( S ` x ) )
142 101 102 5 33 103 105 106 107 27 140 141 98 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 } ) ) ) ) ) )
143 138 142 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 } ) ) ) ) )
144 143 simpld 
 |-  ( ( ( ph /\ ( f e. W /\ A = ( G gsum f ) ) ) /\ x e. I ) -> ( ( ( S ` x ) ( proj1 ` G ) ( G DProd ( S |` ( I \ { x } ) ) ) ) ` A ) = ( f ` x ) )
145 29 144 eqtrd 
 |-  ( ( ( ph /\ ( f e. W /\ A = ( G gsum f ) ) ) /\ x e. I ) -> ( ( P ` x ) ` A ) = ( f ` x ) )
146 145 mpteq2dva 
 |-  ( ( ph /\ ( f e. W /\ A = ( G gsum f ) ) ) -> ( x e. I |-> ( ( P ` x ) ` A ) ) = ( x e. I |-> ( f ` x ) ) )
147 118 146 eqtr4d 
 |-  ( ( ph /\ ( f e. W /\ A = ( G gsum f ) ) ) -> f = ( x e. I |-> ( ( P ` x ) ` A ) ) )
148 147 oveq2d 
 |-  ( ( ph /\ ( f e. W /\ A = ( G gsum f ) ) ) -> ( G gsum f ) = ( G gsum ( x e. I |-> ( ( P ` x ) ` A ) ) ) )
149 117 148 eqtrd 
 |-  ( ( ph /\ ( f e. W /\ A = ( G gsum f ) ) ) -> A = ( G gsum ( x e. I |-> ( ( P ` x ) ` A ) ) ) )
150 116 149 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 ) ) ) ) )
151 10 150 rexlimddv 
 |-  ( ph -> ( ( x e. I |-> ( ( P ` x ) ` A ) ) e. W /\ A = ( G gsum ( x e. I |-> ( ( P ` x ) ` A ) ) ) ) )