Metamath Proof Explorer

Theorem gsumhashmul

Description: Express a group sum by grouping by nonzero values. (Contributed by Thierry Arnoux, 22-Jun-2024)

Ref Expression
Hypotheses gsumhashmul.b 
|- B = ( Base ` G )
gsumhashmul.z 
|- .0. = ( 0g ` G )
gsumhashmul.x 
|- .x. = ( .g ` G )
gsumhashmul.g 
|- ( ph -> G e. CMnd )
gsumhashmul.f 
|- ( ph -> F : A --> B )
gsumhashmul.1 
|- ( ph -> F finSupp .0. )
Assertion gsumhashmul 
|- ( ph -> ( G gsum F ) = ( G gsum ( x e. ( ran F \ { .0. } ) |-> ( ( # ` ( `' F " { x } ) ) .x. x ) ) ) )

Proof

Step Hyp Ref Expression
1 gsumhashmul.b 
 |-  B = ( Base ` G )
2 gsumhashmul.z 
 |-  .0. = ( 0g ` G )
3 gsumhashmul.x 
 |-  .x. = ( .g ` G )
4 gsumhashmul.g 
 |-  ( ph -> G e. CMnd )
5 gsumhashmul.f 
 |-  ( ph -> F : A --> B )
6 gsumhashmul.1 
 |-  ( ph -> F finSupp .0. )
7 suppssdm 
 |-  ( F supp .0. ) C_ dom F
8 7 5 fssdm 
 |-  ( ph -> ( F supp .0. ) C_ A )
9 5 8 feqresmpt 
 |-  ( ph -> ( F |` ( F supp .0. ) ) = ( x e. ( F supp .0. ) |-> ( F ` x ) ) )
10 9 oveq2d 
 |-  ( ph -> ( G gsum ( F |` ( F supp .0. ) ) ) = ( G gsum ( x e. ( F supp .0. ) |-> ( F ` x ) ) ) )
11 relfsupp 
 |-  Rel finSupp
12 11 brrelex1i 
 |-  ( F finSupp .0. -> F e. _V )
13 6 12 syl 
 |-  ( ph -> F e. _V )
14 5 ffnd 
 |-  ( ph -> F Fn A )
15 13 14 fndmexd 
 |-  ( ph -> A e. _V )
16 ssidd 
 |-  ( ph -> ( F supp .0. ) C_ ( F supp .0. ) )
17 1 2 4 15 5 16 6 gsumres 
 |-  ( ph -> ( G gsum ( F |` ( F supp .0. ) ) ) = ( G gsum F ) )
18 nfcv 
 |-  F/_ x ( F ` ( 1st ` z ) )
19 fveq2 
 |-  ( x = ( 1st ` z ) -> ( F ` x ) = ( F ` ( 1st ` z ) ) )
20 6 fsuppimpd 
 |-  ( ph -> ( F supp .0. ) e. Fin )
21 ssidd 
 |-  ( ph -> B C_ B )
22 5 adantr 
 |-  ( ( ph /\ x e. ( F supp .0. ) ) -> F : A --> B )
23 8 sselda 
 |-  ( ( ph /\ x e. ( F supp .0. ) ) -> x e. A )
24 22 23 ffvelcdmd 
 |-  ( ( ph /\ x e. ( F supp .0. ) ) -> ( F ` x ) e. B )
25 5 ffund 
 |-  ( ph -> Fun F )
26 funrel 
 |-  ( Fun F -> Rel F )
27 reldif 
 |-  ( Rel F -> Rel ( F \ ( _V X. { .0. } ) ) )
28 25 26 27 3syl 
 |-  ( ph -> Rel ( F \ ( _V X. { .0. } ) ) )
29 1stdm 
 |-  ( ( Rel ( F \ ( _V X. { .0. } ) ) /\ z e. ( F \ ( _V X. { .0. } ) ) ) -> ( 1st ` z ) e. dom ( F \ ( _V X. { .0. } ) ) )
30 28 29 sylan 
 |-  ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) -> ( 1st ` z ) e. dom ( F \ ( _V X. { .0. } ) ) )
31 2 fvexi 
 |-  .0. e. _V
32 31 a1i 
 |-  ( ph -> .0. e. _V )
33 fressupp 
 |-  ( ( Fun F /\ F e. _V /\ .0. e. _V ) -> ( F |` ( F supp .0. ) ) = ( F \ ( _V X. { .0. } ) ) )
34 25 13 32 33 syl3anc 
 |-  ( ph -> ( F |` ( F supp .0. ) ) = ( F \ ( _V X. { .0. } ) ) )
35 34 dmeqd 
 |-  ( ph -> dom ( F |` ( F supp .0. ) ) = dom ( F \ ( _V X. { .0. } ) ) )
36 7 a1i 
 |-  ( ph -> ( F supp .0. ) C_ dom F )
37 ssdmres 
 |-  ( ( F supp .0. ) C_ dom F <-> dom ( F |` ( F supp .0. ) ) = ( F supp .0. ) )
38 36 37 sylib 
 |-  ( ph -> dom ( F |` ( F supp .0. ) ) = ( F supp .0. ) )
39 35 38 eqtr3d 
 |-  ( ph -> dom ( F \ ( _V X. { .0. } ) ) = ( F supp .0. ) )
40 39 adantr 
 |-  ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) -> dom ( F \ ( _V X. { .0. } ) ) = ( F supp .0. ) )
41 30 40 eleqtrd 
 |-  ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) -> ( 1st ` z ) e. ( F supp .0. ) )
42 25 funresd 
 |-  ( ph -> Fun ( F |` ( F supp .0. ) ) )
43 42 adantr 
 |-  ( ( ph /\ x e. ( F supp .0. ) ) -> Fun ( F |` ( F supp .0. ) ) )
44 38 eleq2d 
 |-  ( ph -> ( x e. dom ( F |` ( F supp .0. ) ) <-> x e. ( F supp .0. ) ) )
45 44 biimpar 
 |-  ( ( ph /\ x e. ( F supp .0. ) ) -> x e. dom ( F |` ( F supp .0. ) ) )
46 simpr 
 |-  ( ( ph /\ x e. ( F supp .0. ) ) -> x e. ( F supp .0. ) )
47 46 fvresd 
 |-  ( ( ph /\ x e. ( F supp .0. ) ) -> ( ( F |` ( F supp .0. ) ) ` x ) = ( F ` x ) )
48 funopfvb 
 |-  ( ( Fun ( F |` ( F supp .0. ) ) /\ x e. dom ( F |` ( F supp .0. ) ) ) -> ( ( ( F |` ( F supp .0. ) ) ` x ) = ( F ` x ) <-> <. x , ( F ` x ) >. e. ( F |` ( F supp .0. ) ) ) )
49 48 biimpa 
 |-  ( ( ( Fun ( F |` ( F supp .0. ) ) /\ x e. dom ( F |` ( F supp .0. ) ) ) /\ ( ( F |` ( F supp .0. ) ) ` x ) = ( F ` x ) ) -> <. x , ( F ` x ) >. e. ( F |` ( F supp .0. ) ) )
50 43 45 47 49 syl21anc 
 |-  ( ( ph /\ x e. ( F supp .0. ) ) -> <. x , ( F ` x ) >. e. ( F |` ( F supp .0. ) ) )
51 34 adantr 
 |-  ( ( ph /\ x e. ( F supp .0. ) ) -> ( F |` ( F supp .0. ) ) = ( F \ ( _V X. { .0. } ) ) )
52 50 51 eleqtrd 
 |-  ( ( ph /\ x e. ( F supp .0. ) ) -> <. x , ( F ` x ) >. e. ( F \ ( _V X. { .0. } ) ) )
53 eqeq2 
 |-  ( v = <. x , ( F ` x ) >. -> ( z = v <-> z = <. x , ( F ` x ) >. ) )
54 53 bibi2d 
 |-  ( v = <. x , ( F ` x ) >. -> ( ( x = ( 1st ` z ) <-> z = v ) <-> ( x = ( 1st ` z ) <-> z = <. x , ( F ` x ) >. ) ) )
55 54 ralbidv 
 |-  ( v = <. x , ( F ` x ) >. -> ( A. z e. ( F \ ( _V X. { .0. } ) ) ( x = ( 1st ` z ) <-> z = v ) <-> A. z e. ( F \ ( _V X. { .0. } ) ) ( x = ( 1st ` z ) <-> z = <. x , ( F ` x ) >. ) ) )
56 55 adantl 
 |-  ( ( ( ph /\ x e. ( F supp .0. ) ) /\ v = <. x , ( F ` x ) >. ) -> ( A. z e. ( F \ ( _V X. { .0. } ) ) ( x = ( 1st ` z ) <-> z = v ) <-> A. z e. ( F \ ( _V X. { .0. } ) ) ( x = ( 1st ` z ) <-> z = <. x , ( F ` x ) >. ) ) )
57 fvexd 
 |-  ( ( ( ( ph /\ x e. ( F supp .0. ) ) /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ x = ( 1st ` z ) ) -> ( 2nd ` z ) e. _V )
58 28 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( F supp .0. ) ) /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ x = ( 1st ` z ) ) -> Rel ( F \ ( _V X. { .0. } ) ) )
59 simplr 
 |-  ( ( ( ( ph /\ x e. ( F supp .0. ) ) /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ x = ( 1st ` z ) ) -> z e. ( F \ ( _V X. { .0. } ) ) )
60 1st2nd 
 |-  ( ( Rel ( F \ ( _V X. { .0. } ) ) /\ z e. ( F \ ( _V X. { .0. } ) ) ) -> z = <. ( 1st ` z ) , ( 2nd ` z ) >. )
61 58 59 60 syl2anc 
 |-  ( ( ( ( ph /\ x e. ( F supp .0. ) ) /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ x = ( 1st ` z ) ) -> z = <. ( 1st ` z ) , ( 2nd ` z ) >. )
62 opeq1 
 |-  ( x = ( 1st ` z ) -> <. x , ( 2nd ` z ) >. = <. ( 1st ` z ) , ( 2nd ` z ) >. )
63 62 adantl 
 |-  ( ( ( ( ph /\ x e. ( F supp .0. ) ) /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ x = ( 1st ` z ) ) -> <. x , ( 2nd ` z ) >. = <. ( 1st ` z ) , ( 2nd ` z ) >. )
64 61 63 eqtr4d 
 |-  ( ( ( ( ph /\ x e. ( F supp .0. ) ) /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ x = ( 1st ` z ) ) -> z = <. x , ( 2nd ` z ) >. )
65 difssd 
 |-  ( ( ph /\ x e. ( F supp .0. ) ) -> ( F \ ( _V X. { .0. } ) ) C_ F )
66 65 sselda 
 |-  ( ( ( ph /\ x e. ( F supp .0. ) ) /\ z e. ( F \ ( _V X. { .0. } ) ) ) -> z e. F )
67 66 adantr 
 |-  ( ( ( ( ph /\ x e. ( F supp .0. ) ) /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ x = ( 1st ` z ) ) -> z e. F )
68 64 67 eqeltrrd 
 |-  ( ( ( ( ph /\ x e. ( F supp .0. ) ) /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ x = ( 1st ` z ) ) -> <. x , ( 2nd ` z ) >. e. F )
69 64 68 jca 
 |-  ( ( ( ( ph /\ x e. ( F supp .0. ) ) /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ x = ( 1st ` z ) ) -> ( z = <. x , ( 2nd ` z ) >. /\ <. x , ( 2nd ` z ) >. e. F ) )
70 opeq2 
 |-  ( y = ( 2nd ` z ) -> <. x , y >. = <. x , ( 2nd ` z ) >. )
71 70 eqeq2d 
 |-  ( y = ( 2nd ` z ) -> ( z = <. x , y >. <-> z = <. x , ( 2nd ` z ) >. ) )
72 70 eleq1d 
 |-  ( y = ( 2nd ` z ) -> ( <. x , y >. e. F <-> <. x , ( 2nd ` z ) >. e. F ) )
73 71 72 anbi12d 
 |-  ( y = ( 2nd ` z ) -> ( ( z = <. x , y >. /\ <. x , y >. e. F ) <-> ( z = <. x , ( 2nd ` z ) >. /\ <. x , ( 2nd ` z ) >. e. F ) ) )
74 57 69 73 spcedv 
 |-  ( ( ( ( ph /\ x e. ( F supp .0. ) ) /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ x = ( 1st ` z ) ) -> E. y ( z = <. x , y >. /\ <. x , y >. e. F ) )
75 vex 
 |-  x e. _V
76 75 elsnres 
 |-  ( z e. ( F |` { x } ) <-> E. y ( z = <. x , y >. /\ <. x , y >. e. F ) )
77 74 76 sylibr 
 |-  ( ( ( ( ph /\ x e. ( F supp .0. ) ) /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ x = ( 1st ` z ) ) -> z e. ( F |` { x } ) )
78 14 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( F supp .0. ) ) /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ x = ( 1st ` z ) ) -> F Fn A )
79 23 ad2antrr 
 |-  ( ( ( ( ph /\ x e. ( F supp .0. ) ) /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ x = ( 1st ` z ) ) -> x e. A )
80 fnressn 
 |-  ( ( F Fn A /\ x e. A ) -> ( F |` { x } ) = { <. x , ( F ` x ) >. } )
81 78 79 80 syl2anc 
 |-  ( ( ( ( ph /\ x e. ( F supp .0. ) ) /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ x = ( 1st ` z ) ) -> ( F |` { x } ) = { <. x , ( F ` x ) >. } )
82 77 81 eleqtrd 
 |-  ( ( ( ( ph /\ x e. ( F supp .0. ) ) /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ x = ( 1st ` z ) ) -> z e. { <. x , ( F ` x ) >. } )
83 elsni 
 |-  ( z e. { <. x , ( F ` x ) >. } -> z = <. x , ( F ` x ) >. )
84 82 83 syl 
 |-  ( ( ( ( ph /\ x e. ( F supp .0. ) ) /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ x = ( 1st ` z ) ) -> z = <. x , ( F ` x ) >. )
85 simpr 
 |-  ( ( ( ( ph /\ x e. ( F supp .0. ) ) /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ z = <. x , ( F ` x ) >. ) -> z = <. x , ( F ` x ) >. )
86 85 fveq2d 
 |-  ( ( ( ( ph /\ x e. ( F supp .0. ) ) /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ z = <. x , ( F ` x ) >. ) -> ( 1st ` z ) = ( 1st ` <. x , ( F ` x ) >. ) )
87 fvex 
 |-  ( F ` x ) e. _V
88 75 87 op1st 
 |-  ( 1st ` <. x , ( F ` x ) >. ) = x
89 86 88 eqtr2di 
 |-  ( ( ( ( ph /\ x e. ( F supp .0. ) ) /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ z = <. x , ( F ` x ) >. ) -> x = ( 1st ` z ) )
90 84 89 impbida 
 |-  ( ( ( ph /\ x e. ( F supp .0. ) ) /\ z e. ( F \ ( _V X. { .0. } ) ) ) -> ( x = ( 1st ` z ) <-> z = <. x , ( F ` x ) >. ) )
91 90 ralrimiva 
 |-  ( ( ph /\ x e. ( F supp .0. ) ) -> A. z e. ( F \ ( _V X. { .0. } ) ) ( x = ( 1st ` z ) <-> z = <. x , ( F ` x ) >. ) )
92 52 56 91 rspcedvd 
 |-  ( ( ph /\ x e. ( F supp .0. ) ) -> E. v e. ( F \ ( _V X. { .0. } ) ) A. z e. ( F \ ( _V X. { .0. } ) ) ( x = ( 1st ` z ) <-> z = v ) )
93 reu6 
 |-  ( E! z e. ( F \ ( _V X. { .0. } ) ) x = ( 1st ` z ) <-> E. v e. ( F \ ( _V X. { .0. } ) ) A. z e. ( F \ ( _V X. { .0. } ) ) ( x = ( 1st ` z ) <-> z = v ) )
94 92 93 sylibr 
 |-  ( ( ph /\ x e. ( F supp .0. ) ) -> E! z e. ( F \ ( _V X. { .0. } ) ) x = ( 1st ` z ) )
95 18 1 2 19 4 20 21 24 41 94 gsummptf1o 
 |-  ( ph -> ( G gsum ( x e. ( F supp .0. ) |-> ( F ` x ) ) ) = ( G gsum ( z e. ( F \ ( _V X. { .0. } ) ) |-> ( F ` ( 1st ` z ) ) ) ) )
96 10 17 95 3eqtr3d 
 |-  ( ph -> ( G gsum F ) = ( G gsum ( z e. ( F \ ( _V X. { .0. } ) ) |-> ( F ` ( 1st ` z ) ) ) ) )
97 simpr 
 |-  ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) -> z e. ( F \ ( _V X. { .0. } ) ) )
98 97 eldifad 
 |-  ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) -> z e. F )
99 funfv1st2nd 
 |-  ( ( Fun F /\ z e. F ) -> ( F ` ( 1st ` z ) ) = ( 2nd ` z ) )
100 25 98 99 syl2an2r 
 |-  ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) -> ( F ` ( 1st ` z ) ) = ( 2nd ` z ) )
101 100 mpteq2dva 
 |-  ( ph -> ( z e. ( F \ ( _V X. { .0. } ) ) |-> ( F ` ( 1st ` z ) ) ) = ( z e. ( F \ ( _V X. { .0. } ) ) |-> ( 2nd ` z ) ) )
102 101 oveq2d 
 |-  ( ph -> ( G gsum ( z e. ( F \ ( _V X. { .0. } ) ) |-> ( F ` ( 1st ` z ) ) ) ) = ( G gsum ( z e. ( F \ ( _V X. { .0. } ) ) |-> ( 2nd ` z ) ) ) )
103 96 102 eqtrd 
 |-  ( ph -> ( G gsum F ) = ( G gsum ( z e. ( F \ ( _V X. { .0. } ) ) |-> ( 2nd ` z ) ) ) )
104 nfcv 
 |-  F/_ z ( 1st ` t )
105 fvex 
 |-  ( 2nd ` t ) e. _V
106 fvex 
 |-  ( 1st ` t ) e. _V
107 105 106 op2ndd 
 |-  ( z = <. ( 2nd ` t ) , ( 1st ` t ) >. -> ( 2nd ` z ) = ( 1st ` t ) )
108 resfnfinfin 
 |-  ( ( F Fn A /\ ( F supp .0. ) e. Fin ) -> ( F |` ( F supp .0. ) ) e. Fin )
109 14 20 108 syl2anc 
 |-  ( ph -> ( F |` ( F supp .0. ) ) e. Fin )
110 34 109 eqeltrrd 
 |-  ( ph -> ( F \ ( _V X. { .0. } ) ) e. Fin )
111 34 rneqd 
 |-  ( ph -> ran ( F |` ( F supp .0. ) ) = ran ( F \ ( _V X. { .0. } ) ) )
112 rnresss 
 |-  ran ( F |` ( F supp .0. ) ) C_ ran F
113 5 frnd 
 |-  ( ph -> ran F C_ B )
114 112 113 sstrid 
 |-  ( ph -> ran ( F |` ( F supp .0. ) ) C_ B )
115 111 114 eqsstrrd 
 |-  ( ph -> ran ( F \ ( _V X. { .0. } ) ) C_ B )
116 2ndrn 
 |-  ( ( Rel ( F \ ( _V X. { .0. } ) ) /\ z e. ( F \ ( _V X. { .0. } ) ) ) -> ( 2nd ` z ) e. ran ( F \ ( _V X. { .0. } ) ) )
117 28 116 sylan 
 |-  ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) -> ( 2nd ` z ) e. ran ( F \ ( _V X. { .0. } ) ) )
118 relcnv 
 |-  Rel `' F
119 reldif 
 |-  ( Rel `' F -> Rel ( `' F \ ( { .0. } X. _V ) ) )
120 118 119 mp1i 
 |-  ( ph -> Rel ( `' F \ ( { .0. } X. _V ) ) )
121 1st2nd 
 |-  ( ( Rel ( `' F \ ( { .0. } X. _V ) ) /\ t e. ( `' F \ ( { .0. } X. _V ) ) ) -> t = <. ( 1st ` t ) , ( 2nd ` t ) >. )
122 120 121 sylan 
 |-  ( ( ph /\ t e. ( `' F \ ( { .0. } X. _V ) ) ) -> t = <. ( 1st ` t ) , ( 2nd ` t ) >. )
123 cnvdif 
 |-  `' ( F \ ( _V X. { .0. } ) ) = ( `' F \ `' ( _V X. { .0. } ) )
124 cnvxp 
 |-  `' ( _V X. { .0. } ) = ( { .0. } X. _V )
125 124 difeq2i 
 |-  ( `' F \ `' ( _V X. { .0. } ) ) = ( `' F \ ( { .0. } X. _V ) )
126 123 125 eqtri 
 |-  `' ( F \ ( _V X. { .0. } ) ) = ( `' F \ ( { .0. } X. _V ) )
127 126 eqimss2i 
 |-  ( `' F \ ( { .0. } X. _V ) ) C_ `' ( F \ ( _V X. { .0. } ) )
128 127 a1i 
 |-  ( ph -> ( `' F \ ( { .0. } X. _V ) ) C_ `' ( F \ ( _V X. { .0. } ) ) )
129 128 sselda 
 |-  ( ( ph /\ t e. ( `' F \ ( { .0. } X. _V ) ) ) -> t e. `' ( F \ ( _V X. { .0. } ) ) )
130 122 129 eqeltrrd 
 |-  ( ( ph /\ t e. ( `' F \ ( { .0. } X. _V ) ) ) -> <. ( 1st ` t ) , ( 2nd ` t ) >. e. `' ( F \ ( _V X. { .0. } ) ) )
131 106 105 opelcnv 
 |-  ( <. ( 1st ` t ) , ( 2nd ` t ) >. e. `' ( F \ ( _V X. { .0. } ) ) <-> <. ( 2nd ` t ) , ( 1st ` t ) >. e. ( F \ ( _V X. { .0. } ) ) )
132 130 131 sylib 
 |-  ( ( ph /\ t e. ( `' F \ ( { .0. } X. _V ) ) ) -> <. ( 2nd ` t ) , ( 1st ` t ) >. e. ( F \ ( _V X. { .0. } ) ) )
133 28 adantr 
 |-  ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) -> Rel ( F \ ( _V X. { .0. } ) ) )
134 eqidd 
 |-  ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) -> U. `' { z } = U. `' { z } )
135 cnvf1olem 
 |-  ( ( Rel ( F \ ( _V X. { .0. } ) ) /\ ( z e. ( F \ ( _V X. { .0. } ) ) /\ U. `' { z } = U. `' { z } ) ) -> ( U. `' { z } e. `' ( F \ ( _V X. { .0. } ) ) /\ z = U. `' { U. `' { z } } ) )
136 135 simpld 
 |-  ( ( Rel ( F \ ( _V X. { .0. } ) ) /\ ( z e. ( F \ ( _V X. { .0. } ) ) /\ U. `' { z } = U. `' { z } ) ) -> U. `' { z } e. `' ( F \ ( _V X. { .0. } ) ) )
137 133 97 134 136 syl12anc 
 |-  ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) -> U. `' { z } e. `' ( F \ ( _V X. { .0. } ) ) )
138 137 126 eleqtrdi 
 |-  ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) -> U. `' { z } e. ( `' F \ ( { .0. } X. _V ) ) )
139 eqeq2 
 |-  ( u = U. `' { z } -> ( t = u <-> t = U. `' { z } ) )
140 139 bibi2d 
 |-  ( u = U. `' { z } -> ( ( z = <. ( 2nd ` t ) , ( 1st ` t ) >. <-> t = u ) <-> ( z = <. ( 2nd ` t ) , ( 1st ` t ) >. <-> t = U. `' { z } ) ) )
141 140 ralbidv 
 |-  ( u = U. `' { z } -> ( A. t e. ( `' F \ ( { .0. } X. _V ) ) ( z = <. ( 2nd ` t ) , ( 1st ` t ) >. <-> t = u ) <-> A. t e. ( `' F \ ( { .0. } X. _V ) ) ( z = <. ( 2nd ` t ) , ( 1st ` t ) >. <-> t = U. `' { z } ) ) )
142 141 adantl 
 |-  ( ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ u = U. `' { z } ) -> ( A. t e. ( `' F \ ( { .0. } X. _V ) ) ( z = <. ( 2nd ` t ) , ( 1st ` t ) >. <-> t = u ) <-> A. t e. ( `' F \ ( { .0. } X. _V ) ) ( z = <. ( 2nd ` t ) , ( 1st ` t ) >. <-> t = U. `' { z } ) ) )
143 118 119 mp1i 
 |-  ( ( ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ t e. ( `' F \ ( { .0. } X. _V ) ) ) /\ z = <. ( 2nd ` t ) , ( 1st ` t ) >. ) -> Rel ( `' F \ ( { .0. } X. _V ) ) )
144 simplr 
 |-  ( ( ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ t e. ( `' F \ ( { .0. } X. _V ) ) ) /\ z = <. ( 2nd ` t ) , ( 1st ` t ) >. ) -> t e. ( `' F \ ( { .0. } X. _V ) ) )
145 simpr 
 |-  ( ( ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ t e. ( `' F \ ( { .0. } X. _V ) ) ) /\ z = <. ( 2nd ` t ) , ( 1st ` t ) >. ) -> z = <. ( 2nd ` t ) , ( 1st ` t ) >. )
146 df-rel 
 |-  ( Rel ( `' F \ ( { .0. } X. _V ) ) <-> ( `' F \ ( { .0. } X. _V ) ) C_ ( _V X. _V ) )
147 120 146 sylib 
 |-  ( ph -> ( `' F \ ( { .0. } X. _V ) ) C_ ( _V X. _V ) )
148 147 ad3antrrr 
 |-  ( ( ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ t e. ( `' F \ ( { .0. } X. _V ) ) ) /\ z = <. ( 2nd ` t ) , ( 1st ` t ) >. ) -> ( `' F \ ( { .0. } X. _V ) ) C_ ( _V X. _V ) )
149 148 144 sseldd 
 |-  ( ( ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ t e. ( `' F \ ( { .0. } X. _V ) ) ) /\ z = <. ( 2nd ` t ) , ( 1st ` t ) >. ) -> t e. ( _V X. _V ) )
150 2nd1st 
 |-  ( t e. ( _V X. _V ) -> U. `' { t } = <. ( 2nd ` t ) , ( 1st ` t ) >. )
151 149 150 syl 
 |-  ( ( ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ t e. ( `' F \ ( { .0. } X. _V ) ) ) /\ z = <. ( 2nd ` t ) , ( 1st ` t ) >. ) -> U. `' { t } = <. ( 2nd ` t ) , ( 1st ` t ) >. )
152 145 151 eqtr4d 
 |-  ( ( ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ t e. ( `' F \ ( { .0. } X. _V ) ) ) /\ z = <. ( 2nd ` t ) , ( 1st ` t ) >. ) -> z = U. `' { t } )
153 cnvf1olem 
 |-  ( ( Rel ( `' F \ ( { .0. } X. _V ) ) /\ ( t e. ( `' F \ ( { .0. } X. _V ) ) /\ z = U. `' { t } ) ) -> ( z e. `' ( `' F \ ( { .0. } X. _V ) ) /\ t = U. `' { z } ) )
154 153 simprd 
 |-  ( ( Rel ( `' F \ ( { .0. } X. _V ) ) /\ ( t e. ( `' F \ ( { .0. } X. _V ) ) /\ z = U. `' { t } ) ) -> t = U. `' { z } )
155 143 144 152 154 syl12anc 
 |-  ( ( ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ t e. ( `' F \ ( { .0. } X. _V ) ) ) /\ z = <. ( 2nd ` t ) , ( 1st ` t ) >. ) -> t = U. `' { z } )
156 28 ad3antrrr 
 |-  ( ( ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ t e. ( `' F \ ( { .0. } X. _V ) ) ) /\ t = U. `' { z } ) -> Rel ( F \ ( _V X. { .0. } ) ) )
157 97 ad2antrr 
 |-  ( ( ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ t e. ( `' F \ ( { .0. } X. _V ) ) ) /\ t = U. `' { z } ) -> z e. ( F \ ( _V X. { .0. } ) ) )
158 simpr 
 |-  ( ( ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ t e. ( `' F \ ( { .0. } X. _V ) ) ) /\ t = U. `' { z } ) -> t = U. `' { z } )
159 cnvf1olem 
 |-  ( ( Rel ( F \ ( _V X. { .0. } ) ) /\ ( z e. ( F \ ( _V X. { .0. } ) ) /\ t = U. `' { z } ) ) -> ( t e. `' ( F \ ( _V X. { .0. } ) ) /\ z = U. `' { t } ) )
160 159 simprd 
 |-  ( ( Rel ( F \ ( _V X. { .0. } ) ) /\ ( z e. ( F \ ( _V X. { .0. } ) ) /\ t = U. `' { z } ) ) -> z = U. `' { t } )
161 156 157 158 160 syl12anc 
 |-  ( ( ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ t e. ( `' F \ ( { .0. } X. _V ) ) ) /\ t = U. `' { z } ) -> z = U. `' { t } )
162 147 ad3antrrr 
 |-  ( ( ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ t e. ( `' F \ ( { .0. } X. _V ) ) ) /\ t = U. `' { z } ) -> ( `' F \ ( { .0. } X. _V ) ) C_ ( _V X. _V ) )
163 simplr 
 |-  ( ( ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ t e. ( `' F \ ( { .0. } X. _V ) ) ) /\ t = U. `' { z } ) -> t e. ( `' F \ ( { .0. } X. _V ) ) )
164 162 163 sseldd 
 |-  ( ( ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ t e. ( `' F \ ( { .0. } X. _V ) ) ) /\ t = U. `' { z } ) -> t e. ( _V X. _V ) )
165 164 150 syl 
 |-  ( ( ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ t e. ( `' F \ ( { .0. } X. _V ) ) ) /\ t = U. `' { z } ) -> U. `' { t } = <. ( 2nd ` t ) , ( 1st ` t ) >. )
166 161 165 eqtrd 
 |-  ( ( ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ t e. ( `' F \ ( { .0. } X. _V ) ) ) /\ t = U. `' { z } ) -> z = <. ( 2nd ` t ) , ( 1st ` t ) >. )
167 155 166 impbida 
 |-  ( ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) /\ t e. ( `' F \ ( { .0. } X. _V ) ) ) -> ( z = <. ( 2nd ` t ) , ( 1st ` t ) >. <-> t = U. `' { z } ) )
168 167 ralrimiva 
 |-  ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) -> A. t e. ( `' F \ ( { .0. } X. _V ) ) ( z = <. ( 2nd ` t ) , ( 1st ` t ) >. <-> t = U. `' { z } ) )
169 138 142 168 rspcedvd 
 |-  ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) -> E. u e. ( `' F \ ( { .0. } X. _V ) ) A. t e. ( `' F \ ( { .0. } X. _V ) ) ( z = <. ( 2nd ` t ) , ( 1st ` t ) >. <-> t = u ) )
170 reu6 
 |-  ( E! t e. ( `' F \ ( { .0. } X. _V ) ) z = <. ( 2nd ` t ) , ( 1st ` t ) >. <-> E. u e. ( `' F \ ( { .0. } X. _V ) ) A. t e. ( `' F \ ( { .0. } X. _V ) ) ( z = <. ( 2nd ` t ) , ( 1st ` t ) >. <-> t = u ) )
171 169 170 sylibr 
 |-  ( ( ph /\ z e. ( F \ ( _V X. { .0. } ) ) ) -> E! t e. ( `' F \ ( { .0. } X. _V ) ) z = <. ( 2nd ` t ) , ( 1st ` t ) >. )
172 104 1 2 107 4 110 115 117 132 171 gsummptf1o 
 |-  ( ph -> ( G gsum ( z e. ( F \ ( _V X. { .0. } ) ) |-> ( 2nd ` z ) ) ) = ( G gsum ( t e. ( `' F \ ( { .0. } X. _V ) ) |-> ( 1st ` t ) ) ) )
173 fveq2 
 |-  ( t = z -> ( 1st ` t ) = ( 1st ` z ) )
174 173 cbvmptv 
 |-  ( t e. ( `' F \ ( { .0. } X. _V ) ) |-> ( 1st ` t ) ) = ( z e. ( `' F \ ( { .0. } X. _V ) ) |-> ( 1st ` z ) )
175 34 cnveqd 
 |-  ( ph -> `' ( F |` ( F supp .0. ) ) = `' ( F \ ( _V X. { .0. } ) ) )
176 175 126 eqtr2di 
 |-  ( ph -> ( `' F \ ( { .0. } X. _V ) ) = `' ( F |` ( F supp .0. ) ) )
177 176 mpteq1d 
 |-  ( ph -> ( z e. ( `' F \ ( { .0. } X. _V ) ) |-> ( 1st ` z ) ) = ( z e. `' ( F |` ( F supp .0. ) ) |-> ( 1st ` z ) ) )
178 174 177 eqtrid 
 |-  ( ph -> ( t e. ( `' F \ ( { .0. } X. _V ) ) |-> ( 1st ` t ) ) = ( z e. `' ( F |` ( F supp .0. ) ) |-> ( 1st ` z ) ) )
179 178 oveq2d 
 |-  ( ph -> ( G gsum ( t e. ( `' F \ ( { .0. } X. _V ) ) |-> ( 1st ` t ) ) ) = ( G gsum ( z e. `' ( F |` ( F supp .0. ) ) |-> ( 1st ` z ) ) ) )
180 103 172 179 3eqtrd 
 |-  ( ph -> ( G gsum F ) = ( G gsum ( z e. `' ( F |` ( F supp .0. ) ) |-> ( 1st ` z ) ) ) )
181 nfcv 
 |-  F/_ y ( 1st ` z )
182 nfv 
 |-  F/ x ph
183 vex 
 |-  y e. _V
184 75 183 op1std 
 |-  ( z = <. x , y >. -> ( 1st ` z ) = x )
185 relcnv 
 |-  Rel `' ( F |` ( F supp .0. ) )
186 185 a1i 
 |-  ( ph -> Rel `' ( F |` ( F supp .0. ) ) )
187 cnvfi 
 |-  ( ( F |` ( F supp .0. ) ) e. Fin -> `' ( F |` ( F supp .0. ) ) e. Fin )
188 109 187 syl 
 |-  ( ph -> `' ( F |` ( F supp .0. ) ) e. Fin )
189 113 adantr 
 |-  ( ( ph /\ z e. `' ( F |` ( F supp .0. ) ) ) -> ran F C_ B )
190 185 a1i 
 |-  ( ( ph /\ z e. `' ( F |` ( F supp .0. ) ) ) -> Rel `' ( F |` ( F supp .0. ) ) )
191 simpr 
 |-  ( ( ph /\ z e. `' ( F |` ( F supp .0. ) ) ) -> z e. `' ( F |` ( F supp .0. ) ) )
192 1stdm 
 |-  ( ( Rel `' ( F |` ( F supp .0. ) ) /\ z e. `' ( F |` ( F supp .0. ) ) ) -> ( 1st ` z ) e. dom `' ( F |` ( F supp .0. ) ) )
193 190 191 192 syl2anc 
 |-  ( ( ph /\ z e. `' ( F |` ( F supp .0. ) ) ) -> ( 1st ` z ) e. dom `' ( F |` ( F supp .0. ) ) )
194 df-rn 
 |-  ran ( F |` ( F supp .0. ) ) = dom `' ( F |` ( F supp .0. ) )
195 193 194 eleqtrrdi 
 |-  ( ( ph /\ z e. `' ( F |` ( F supp .0. ) ) ) -> ( 1st ` z ) e. ran ( F |` ( F supp .0. ) ) )
196 112 195 sselid 
 |-  ( ( ph /\ z e. `' ( F |` ( F supp .0. ) ) ) -> ( 1st ` z ) e. ran F )
197 189 196 sseldd 
 |-  ( ( ph /\ z e. `' ( F |` ( F supp .0. ) ) ) -> ( 1st ` z ) e. B )
198 181 182 1 184 186 188 4 197 gsummpt2d 
 |-  ( ph -> ( G gsum ( z e. `' ( F |` ( F supp .0. ) ) |-> ( 1st ` z ) ) ) = ( G gsum ( x e. dom `' ( F |` ( F supp .0. ) ) |-> ( G gsum ( y e. ( `' ( F |` ( F supp .0. ) ) " { x } ) |-> x ) ) ) ) )
199 df-ima 
 |-  ( F " ( F supp .0. ) ) = ran ( F |` ( F supp .0. ) )
200 supppreima 
 |-  ( ( Fun F /\ F e. _V /\ .0. e. _V ) -> ( F supp .0. ) = ( `' F " ( ran F \ { .0. } ) ) )
201 25 13 32 200 syl3anc 
 |-  ( ph -> ( F supp .0. ) = ( `' F " ( ran F \ { .0. } ) ) )
202 201 imaeq2d 
 |-  ( ph -> ( F " ( F supp .0. ) ) = ( F " ( `' F " ( ran F \ { .0. } ) ) ) )
203 199 202 eqtr3id 
 |-  ( ph -> ran ( F |` ( F supp .0. ) ) = ( F " ( `' F " ( ran F \ { .0. } ) ) ) )
204 funimacnv 
 |-  ( Fun F -> ( F " ( `' F " ( ran F \ { .0. } ) ) ) = ( ( ran F \ { .0. } ) i^i ran F ) )
205 25 204 syl 
 |-  ( ph -> ( F " ( `' F " ( ran F \ { .0. } ) ) ) = ( ( ran F \ { .0. } ) i^i ran F ) )
206 difssd 
 |-  ( ph -> ( ran F \ { .0. } ) C_ ran F )
207 dfss2 
 |-  ( ( ran F \ { .0. } ) C_ ran F <-> ( ( ran F \ { .0. } ) i^i ran F ) = ( ran F \ { .0. } ) )
208 206 207 sylib 
 |-  ( ph -> ( ( ran F \ { .0. } ) i^i ran F ) = ( ran F \ { .0. } ) )
209 203 205 208 3eqtrd 
 |-  ( ph -> ran ( F |` ( F supp .0. ) ) = ( ran F \ { .0. } ) )
210 194 209 eqtr3id 
 |-  ( ph -> dom `' ( F |` ( F supp .0. ) ) = ( ran F \ { .0. } ) )
211 4 cmnmndd 
 |-  ( ph -> G e. Mnd )
212 211 adantr 
 |-  ( ( ph /\ x e. dom `' ( F |` ( F supp .0. ) ) ) -> G e. Mnd )
213 109 adantr 
 |-  ( ( ph /\ x e. dom `' ( F |` ( F supp .0. ) ) ) -> ( F |` ( F supp .0. ) ) e. Fin )
214 imafi2 
 |-  ( `' ( F |` ( F supp .0. ) ) e. Fin -> ( `' ( F |` ( F supp .0. ) ) " { x } ) e. Fin )
215 213 187 214 3syl 
 |-  ( ( ph /\ x e. dom `' ( F |` ( F supp .0. ) ) ) -> ( `' ( F |` ( F supp .0. ) ) " { x } ) e. Fin )
216 194 114 eqsstrrid 
 |-  ( ph -> dom `' ( F |` ( F supp .0. ) ) C_ B )
217 216 sselda 
 |-  ( ( ph /\ x e. dom `' ( F |` ( F supp .0. ) ) ) -> x e. B )
218 1 3 gsumconst 
 |-  ( ( G e. Mnd /\ ( `' ( F |` ( F supp .0. ) ) " { x } ) e. Fin /\ x e. B ) -> ( G gsum ( y e. ( `' ( F |` ( F supp .0. ) ) " { x } ) |-> x ) ) = ( ( # ` ( `' ( F |` ( F supp .0. ) ) " { x } ) ) .x. x ) )
219 212 215 217 218 syl3anc 
 |-  ( ( ph /\ x e. dom `' ( F |` ( F supp .0. ) ) ) -> ( G gsum ( y e. ( `' ( F |` ( F supp .0. ) ) " { x } ) |-> x ) ) = ( ( # ` ( `' ( F |` ( F supp .0. ) ) " { x } ) ) .x. x ) )
220 cnvresima 
 |-  ( `' ( F |` ( F supp .0. ) ) " { x } ) = ( ( `' F " { x } ) i^i ( F supp .0. ) )
221 210 eleq2d 
 |-  ( ph -> ( x e. dom `' ( F |` ( F supp .0. ) ) <-> x e. ( ran F \ { .0. } ) ) )
222 221 biimpa 
 |-  ( ( ph /\ x e. dom `' ( F |` ( F supp .0. ) ) ) -> x e. ( ran F \ { .0. } ) )
223 222 snssd 
 |-  ( ( ph /\ x e. dom `' ( F |` ( F supp .0. ) ) ) -> { x } C_ ( ran F \ { .0. } ) )
224 sspreima 
 |-  ( ( Fun F /\ { x } C_ ( ran F \ { .0. } ) ) -> ( `' F " { x } ) C_ ( `' F " ( ran F \ { .0. } ) ) )
225 25 223 224 syl2an2r 
 |-  ( ( ph /\ x e. dom `' ( F |` ( F supp .0. ) ) ) -> ( `' F " { x } ) C_ ( `' F " ( ran F \ { .0. } ) ) )
226 201 adantr 
 |-  ( ( ph /\ x e. dom `' ( F |` ( F supp .0. ) ) ) -> ( F supp .0. ) = ( `' F " ( ran F \ { .0. } ) ) )
227 225 226 sseqtrrd 
 |-  ( ( ph /\ x e. dom `' ( F |` ( F supp .0. ) ) ) -> ( `' F " { x } ) C_ ( F supp .0. ) )
228 dfss2 
 |-  ( ( `' F " { x } ) C_ ( F supp .0. ) <-> ( ( `' F " { x } ) i^i ( F supp .0. ) ) = ( `' F " { x } ) )
229 227 228 sylib 
 |-  ( ( ph /\ x e. dom `' ( F |` ( F supp .0. ) ) ) -> ( ( `' F " { x } ) i^i ( F supp .0. ) ) = ( `' F " { x } ) )
230 220 229 eqtr2id 
 |-  ( ( ph /\ x e. dom `' ( F |` ( F supp .0. ) ) ) -> ( `' F " { x } ) = ( `' ( F |` ( F supp .0. ) ) " { x } ) )
231 230 fveq2d 
 |-  ( ( ph /\ x e. dom `' ( F |` ( F supp .0. ) ) ) -> ( # ` ( `' F " { x } ) ) = ( # ` ( `' ( F |` ( F supp .0. ) ) " { x } ) ) )
232 231 oveq1d 
 |-  ( ( ph /\ x e. dom `' ( F |` ( F supp .0. ) ) ) -> ( ( # ` ( `' F " { x } ) ) .x. x ) = ( ( # ` ( `' ( F |` ( F supp .0. ) ) " { x } ) ) .x. x ) )
233 219 232 eqtr4d 
 |-  ( ( ph /\ x e. dom `' ( F |` ( F supp .0. ) ) ) -> ( G gsum ( y e. ( `' ( F |` ( F supp .0. ) ) " { x } ) |-> x ) ) = ( ( # ` ( `' F " { x } ) ) .x. x ) )
234 210 233 mpteq12dva 
 |-  ( ph -> ( x e. dom `' ( F |` ( F supp .0. ) ) |-> ( G gsum ( y e. ( `' ( F |` ( F supp .0. ) ) " { x } ) |-> x ) ) ) = ( x e. ( ran F \ { .0. } ) |-> ( ( # ` ( `' F " { x } ) ) .x. x ) ) )
235 234 oveq2d 
 |-  ( ph -> ( G gsum ( x e. dom `' ( F |` ( F supp .0. ) ) |-> ( G gsum ( y e. ( `' ( F |` ( F supp .0. ) ) " { x } ) |-> x ) ) ) ) = ( G gsum ( x e. ( ran F \ { .0. } ) |-> ( ( # ` ( `' F " { x } ) ) .x. x ) ) ) )
236 180 198 235 3eqtrd 
 |-  ( ph -> ( G gsum F ) = ( G gsum ( x e. ( ran F \ { .0. } ) |-> ( ( # ` ( `' F " { x } ) ) .x. x ) ) ) )