Metamath Proof Explorer

Theorem gsum2dlem2

Description: Lemma for gsum2d . (Contributed by Mario Carneiro, 28-Dec-2014) (Revised by AV, 8-Jun-2019)

Ref Expression
Hypotheses gsum2d.b 
|- B = ( Base ` G )
gsum2d.z 
|- .0. = ( 0g ` G )
gsum2d.g 
|- ( ph -> G e. CMnd )
gsum2d.a 
|- ( ph -> A e. V )
gsum2d.r 
|- ( ph -> Rel A )
gsum2d.d 
|- ( ph -> D e. W )
gsum2d.s 
|- ( ph -> dom A C_ D )
gsum2d.f 
|- ( ph -> F : A --> B )
gsum2d.w 
|- ( ph -> F finSupp .0. )
Assertion gsum2dlem2 
|- ( ph -> ( G gsum ( F |` ( A |` dom ( F supp .0. ) ) ) ) = ( G gsum ( j e. dom ( F supp .0. ) |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 gsum2d.b 
 |-  B = ( Base ` G )
2 gsum2d.z 
 |-  .0. = ( 0g ` G )
3 gsum2d.g 
 |-  ( ph -> G e. CMnd )
4 gsum2d.a 
 |-  ( ph -> A e. V )
5 gsum2d.r 
 |-  ( ph -> Rel A )
6 gsum2d.d 
 |-  ( ph -> D e. W )
7 gsum2d.s 
 |-  ( ph -> dom A C_ D )
8 gsum2d.f 
 |-  ( ph -> F : A --> B )
9 gsum2d.w 
 |-  ( ph -> F finSupp .0. )
10 9 fsuppimpd 
 |-  ( ph -> ( F supp .0. ) e. Fin )
11 dmfi 
 |-  ( ( F supp .0. ) e. Fin -> dom ( F supp .0. ) e. Fin )
12 10 11 syl 
 |-  ( ph -> dom ( F supp .0. ) e. Fin )
13 reseq2 
 |-  ( x = (/) -> ( A |` x ) = ( A |` (/) ) )
14 res0 
 |-  ( A |` (/) ) = (/)
15 13 14 eqtrdi 
 |-  ( x = (/) -> ( A |` x ) = (/) )
16 15 reseq2d 
 |-  ( x = (/) -> ( F |` ( A |` x ) ) = ( F |` (/) ) )
17 res0 
 |-  ( F |` (/) ) = (/)
18 16 17 eqtrdi 
 |-  ( x = (/) -> ( F |` ( A |` x ) ) = (/) )
19 18 oveq2d 
 |-  ( x = (/) -> ( G gsum ( F |` ( A |` x ) ) ) = ( G gsum (/) ) )
20 mpteq1 
 |-  ( x = (/) -> ( j e. x |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) = ( j e. (/) |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) )
21 mpt0 
 |-  ( j e. (/) |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) = (/)
22 20 21 eqtrdi 
 |-  ( x = (/) -> ( j e. x |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) = (/) )
23 22 oveq2d 
 |-  ( x = (/) -> ( G gsum ( j e. x |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) = ( G gsum (/) ) )
24 19 23 eqeq12d 
 |-  ( x = (/) -> ( ( G gsum ( F |` ( A |` x ) ) ) = ( G gsum ( j e. x |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) <-> ( G gsum (/) ) = ( G gsum (/) ) ) )
25 24 imbi2d 
 |-  ( x = (/) -> ( ( ph -> ( G gsum ( F |` ( A |` x ) ) ) = ( G gsum ( j e. x |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) ) <-> ( ph -> ( G gsum (/) ) = ( G gsum (/) ) ) ) )
26 reseq2 
 |-  ( x = y -> ( A |` x ) = ( A |` y ) )
27 26 reseq2d 
 |-  ( x = y -> ( F |` ( A |` x ) ) = ( F |` ( A |` y ) ) )
28 27 oveq2d 
 |-  ( x = y -> ( G gsum ( F |` ( A |` x ) ) ) = ( G gsum ( F |` ( A |` y ) ) ) )
29 mpteq1 
 |-  ( x = y -> ( j e. x |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) = ( j e. y |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) )
30 29 oveq2d 
 |-  ( x = y -> ( G gsum ( j e. x |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) = ( G gsum ( j e. y |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) )
31 28 30 eqeq12d 
 |-  ( x = y -> ( ( G gsum ( F |` ( A |` x ) ) ) = ( G gsum ( j e. x |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) <-> ( G gsum ( F |` ( A |` y ) ) ) = ( G gsum ( j e. y |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) ) )
32 31 imbi2d 
 |-  ( x = y -> ( ( ph -> ( G gsum ( F |` ( A |` x ) ) ) = ( G gsum ( j e. x |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) ) <-> ( ph -> ( G gsum ( F |` ( A |` y ) ) ) = ( G gsum ( j e. y |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) ) ) )
33 reseq2 
 |-  ( x = ( y u. { z } ) -> ( A |` x ) = ( A |` ( y u. { z } ) ) )
34 33 reseq2d 
 |-  ( x = ( y u. { z } ) -> ( F |` ( A |` x ) ) = ( F |` ( A |` ( y u. { z } ) ) ) )
35 34 oveq2d 
 |-  ( x = ( y u. { z } ) -> ( G gsum ( F |` ( A |` x ) ) ) = ( G gsum ( F |` ( A |` ( y u. { z } ) ) ) ) )
36 mpteq1 
 |-  ( x = ( y u. { z } ) -> ( j e. x |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) = ( j e. ( y u. { z } ) |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) )
37 36 oveq2d 
 |-  ( x = ( y u. { z } ) -> ( G gsum ( j e. x |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) = ( G gsum ( j e. ( y u. { z } ) |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) )
38 35 37 eqeq12d 
 |-  ( x = ( y u. { z } ) -> ( ( G gsum ( F |` ( A |` x ) ) ) = ( G gsum ( j e. x |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) <-> ( G gsum ( F |` ( A |` ( y u. { z } ) ) ) ) = ( G gsum ( j e. ( y u. { z } ) |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) ) )
39 38 imbi2d 
 |-  ( x = ( y u. { z } ) -> ( ( ph -> ( G gsum ( F |` ( A |` x ) ) ) = ( G gsum ( j e. x |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) ) <-> ( ph -> ( G gsum ( F |` ( A |` ( y u. { z } ) ) ) ) = ( G gsum ( j e. ( y u. { z } ) |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) ) ) )
40 reseq2 
 |-  ( x = dom ( F supp .0. ) -> ( A |` x ) = ( A |` dom ( F supp .0. ) ) )
41 40 reseq2d 
 |-  ( x = dom ( F supp .0. ) -> ( F |` ( A |` x ) ) = ( F |` ( A |` dom ( F supp .0. ) ) ) )
42 41 oveq2d 
 |-  ( x = dom ( F supp .0. ) -> ( G gsum ( F |` ( A |` x ) ) ) = ( G gsum ( F |` ( A |` dom ( F supp .0. ) ) ) ) )
43 mpteq1 
 |-  ( x = dom ( F supp .0. ) -> ( j e. x |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) = ( j e. dom ( F supp .0. ) |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) )
44 43 oveq2d 
 |-  ( x = dom ( F supp .0. ) -> ( G gsum ( j e. x |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) = ( G gsum ( j e. dom ( F supp .0. ) |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) )
45 42 44 eqeq12d 
 |-  ( x = dom ( F supp .0. ) -> ( ( G gsum ( F |` ( A |` x ) ) ) = ( G gsum ( j e. x |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) <-> ( G gsum ( F |` ( A |` dom ( F supp .0. ) ) ) ) = ( G gsum ( j e. dom ( F supp .0. ) |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) ) )
46 45 imbi2d 
 |-  ( x = dom ( F supp .0. ) -> ( ( ph -> ( G gsum ( F |` ( A |` x ) ) ) = ( G gsum ( j e. x |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) ) <-> ( ph -> ( G gsum ( F |` ( A |` dom ( F supp .0. ) ) ) ) = ( G gsum ( j e. dom ( F supp .0. ) |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) ) ) )
47 eqidd 
 |-  ( ph -> ( G gsum (/) ) = ( G gsum (/) ) )
48 oveq1 
 |-  ( ( G gsum ( F |` ( A |` y ) ) ) = ( G gsum ( j e. y |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) -> ( ( G gsum ( F |` ( A |` y ) ) ) ( +g ` G ) ( G gsum ( F |` ( A |` { z } ) ) ) ) = ( ( G gsum ( j e. y |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) ( +g ` G ) ( G gsum ( F |` ( A |` { z } ) ) ) ) )
49 eqid 
 |-  ( +g ` G ) = ( +g ` G )
50 3 adantr 
 |-  ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> G e. CMnd )
51 4 resexd 
 |-  ( ph -> ( A |` ( y u. { z } ) ) e. _V )
52 51 adantr 
 |-  ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> ( A |` ( y u. { z } ) ) e. _V )
53 resss 
 |-  ( A |` ( y u. { z } ) ) C_ A
54 fssres 
 |-  ( ( F : A --> B /\ ( A |` ( y u. { z } ) ) C_ A ) -> ( F |` ( A |` ( y u. { z } ) ) ) : ( A |` ( y u. { z } ) ) --> B )
55 8 53 54 sylancl 
 |-  ( ph -> ( F |` ( A |` ( y u. { z } ) ) ) : ( A |` ( y u. { z } ) ) --> B )
56 55 adantr 
 |-  ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> ( F |` ( A |` ( y u. { z } ) ) ) : ( A |` ( y u. { z } ) ) --> B )
57 8 ffund 
 |-  ( ph -> Fun F )
58 57 funresd 
 |-  ( ph -> Fun ( F |` ( A |` ( y u. { z } ) ) ) )
59 58 adantr 
 |-  ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> Fun ( F |` ( A |` ( y u. { z } ) ) ) )
60 10 adantr 
 |-  ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> ( F supp .0. ) e. Fin )
61 8 4 fexd 
 |-  ( ph -> F e. _V )
62 2 fvexi 
 |-  .0. e. _V
63 ressuppss 
 |-  ( ( F e. _V /\ .0. e. _V ) -> ( ( F |` ( A |` ( y u. { z } ) ) ) supp .0. ) C_ ( F supp .0. ) )
64 61 62 63 sylancl 
 |-  ( ph -> ( ( F |` ( A |` ( y u. { z } ) ) ) supp .0. ) C_ ( F supp .0. ) )
65 64 adantr 
 |-  ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> ( ( F |` ( A |` ( y u. { z } ) ) ) supp .0. ) C_ ( F supp .0. ) )
66 60 65 ssfid 
 |-  ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> ( ( F |` ( A |` ( y u. { z } ) ) ) supp .0. ) e. Fin )
67 61 resexd 
 |-  ( ph -> ( F |` ( A |` ( y u. { z } ) ) ) e. _V )
68 isfsupp 
 |-  ( ( ( F |` ( A |` ( y u. { z } ) ) ) e. _V /\ .0. e. _V ) -> ( ( F |` ( A |` ( y u. { z } ) ) ) finSupp .0. <-> ( Fun ( F |` ( A |` ( y u. { z } ) ) ) /\ ( ( F |` ( A |` ( y u. { z } ) ) ) supp .0. ) e. Fin ) ) )
69 67 62 68 sylancl 
 |-  ( ph -> ( ( F |` ( A |` ( y u. { z } ) ) ) finSupp .0. <-> ( Fun ( F |` ( A |` ( y u. { z } ) ) ) /\ ( ( F |` ( A |` ( y u. { z } ) ) ) supp .0. ) e. Fin ) ) )
70 69 adantr 
 |-  ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> ( ( F |` ( A |` ( y u. { z } ) ) ) finSupp .0. <-> ( Fun ( F |` ( A |` ( y u. { z } ) ) ) /\ ( ( F |` ( A |` ( y u. { z } ) ) ) supp .0. ) e. Fin ) ) )
71 59 66 70 mpbir2and 
 |-  ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> ( F |` ( A |` ( y u. { z } ) ) ) finSupp .0. )
72 simprr 
 |-  ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> -. z e. y )
73 disjsn 
 |-  ( ( y i^i { z } ) = (/) <-> -. z e. y )
74 72 73 sylibr 
 |-  ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> ( y i^i { z } ) = (/) )
75 74 reseq2d 
 |-  ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> ( A |` ( y i^i { z } ) ) = ( A |` (/) ) )
76 resindi 
 |-  ( A |` ( y i^i { z } ) ) = ( ( A |` y ) i^i ( A |` { z } ) )
77 75 76 14 3eqtr3g 
 |-  ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> ( ( A |` y ) i^i ( A |` { z } ) ) = (/) )
78 resundi 
 |-  ( A |` ( y u. { z } ) ) = ( ( A |` y ) u. ( A |` { z } ) )
79 78 a1i 
 |-  ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> ( A |` ( y u. { z } ) ) = ( ( A |` y ) u. ( A |` { z } ) ) )
80 1 2 49 50 52 56 71 77 79 gsumsplit 
 |-  ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> ( G gsum ( F |` ( A |` ( y u. { z } ) ) ) ) = ( ( G gsum ( ( F |` ( A |` ( y u. { z } ) ) ) |` ( A |` y ) ) ) ( +g ` G ) ( G gsum ( ( F |` ( A |` ( y u. { z } ) ) ) |` ( A |` { z } ) ) ) ) )
81 ssun1 
 |-  y C_ ( y u. { z } )
82 ssres2 
 |-  ( y C_ ( y u. { z } ) -> ( A |` y ) C_ ( A |` ( y u. { z } ) ) )
83 resabs1 
 |-  ( ( A |` y ) C_ ( A |` ( y u. { z } ) ) -> ( ( F |` ( A |` ( y u. { z } ) ) ) |` ( A |` y ) ) = ( F |` ( A |` y ) ) )
84 81 82 83 mp2b 
 |-  ( ( F |` ( A |` ( y u. { z } ) ) ) |` ( A |` y ) ) = ( F |` ( A |` y ) )
85 84 oveq2i 
 |-  ( G gsum ( ( F |` ( A |` ( y u. { z } ) ) ) |` ( A |` y ) ) ) = ( G gsum ( F |` ( A |` y ) ) )
86 ssun2 
 |-  { z } C_ ( y u. { z } )
87 ssres2 
 |-  ( { z } C_ ( y u. { z } ) -> ( A |` { z } ) C_ ( A |` ( y u. { z } ) ) )
88 resabs1 
 |-  ( ( A |` { z } ) C_ ( A |` ( y u. { z } ) ) -> ( ( F |` ( A |` ( y u. { z } ) ) ) |` ( A |` { z } ) ) = ( F |` ( A |` { z } ) ) )
89 86 87 88 mp2b 
 |-  ( ( F |` ( A |` ( y u. { z } ) ) ) |` ( A |` { z } ) ) = ( F |` ( A |` { z } ) )
90 89 oveq2i 
 |-  ( G gsum ( ( F |` ( A |` ( y u. { z } ) ) ) |` ( A |` { z } ) ) ) = ( G gsum ( F |` ( A |` { z } ) ) )
91 85 90 oveq12i 
 |-  ( ( G gsum ( ( F |` ( A |` ( y u. { z } ) ) ) |` ( A |` y ) ) ) ( +g ` G ) ( G gsum ( ( F |` ( A |` ( y u. { z } ) ) ) |` ( A |` { z } ) ) ) ) = ( ( G gsum ( F |` ( A |` y ) ) ) ( +g ` G ) ( G gsum ( F |` ( A |` { z } ) ) ) )
92 80 91 eqtrdi 
 |-  ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> ( G gsum ( F |` ( A |` ( y u. { z } ) ) ) ) = ( ( G gsum ( F |` ( A |` y ) ) ) ( +g ` G ) ( G gsum ( F |` ( A |` { z } ) ) ) ) )
93 simprl 
 |-  ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> y e. Fin )
94 1 2 3 4 5 6 7 8 9 gsum2dlem1 
 |-  ( ph -> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) e. B )
95 94 ad2antrr 
 |-  ( ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) /\ j e. y ) -> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) e. B )
96 vex 
 |-  z e. _V
97 96 a1i 
 |-  ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> z e. _V )
98 sneq 
 |-  ( j = z -> { j } = { z } )
99 98 imaeq2d 
 |-  ( j = z -> ( A " { j } ) = ( A " { z } ) )
100 oveq1 
 |-  ( j = z -> ( j F k ) = ( z F k ) )
101 99 100 mpteq12dv 
 |-  ( j = z -> ( k e. ( A " { j } ) |-> ( j F k ) ) = ( k e. ( A " { z } ) |-> ( z F k ) ) )
102 101 oveq2d 
 |-  ( j = z -> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) = ( G gsum ( k e. ( A " { z } ) |-> ( z F k ) ) ) )
103 102 eleq1d 
 |-  ( j = z -> ( ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) e. B <-> ( G gsum ( k e. ( A " { z } ) |-> ( z F k ) ) ) e. B ) )
104 103 imbi2d 
 |-  ( j = z -> ( ( ph -> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) e. B ) <-> ( ph -> ( G gsum ( k e. ( A " { z } ) |-> ( z F k ) ) ) e. B ) ) )
105 104 94 chvarvv 
 |-  ( ph -> ( G gsum ( k e. ( A " { z } ) |-> ( z F k ) ) ) e. B )
106 105 adantr 
 |-  ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> ( G gsum ( k e. ( A " { z } ) |-> ( z F k ) ) ) e. B )
107 1 49 50 93 95 97 72 106 102 gsumunsn 
 |-  ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> ( G gsum ( j e. ( y u. { z } ) |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) = ( ( G gsum ( j e. y |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) ( +g ` G ) ( G gsum ( k e. ( A " { z } ) |-> ( z F k ) ) ) ) )
108 98 reseq2d 
 |-  ( j = z -> ( A |` { j } ) = ( A |` { z } ) )
109 108 reseq2d 
 |-  ( j = z -> ( F |` ( A |` { j } ) ) = ( F |` ( A |` { z } ) ) )
110 109 oveq2d 
 |-  ( j = z -> ( G gsum ( F |` ( A |` { j } ) ) ) = ( G gsum ( F |` ( A |` { z } ) ) ) )
111 102 110 eqeq12d 
 |-  ( j = z -> ( ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) = ( G gsum ( F |` ( A |` { j } ) ) ) <-> ( G gsum ( k e. ( A " { z } ) |-> ( z F k ) ) ) = ( G gsum ( F |` ( A |` { z } ) ) ) ) )
112 111 imbi2d 
 |-  ( j = z -> ( ( ph -> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) = ( G gsum ( F |` ( A |` { j } ) ) ) ) <-> ( ph -> ( G gsum ( k e. ( A " { z } ) |-> ( z F k ) ) ) = ( G gsum ( F |` ( A |` { z } ) ) ) ) ) )
113 imaexg 
 |-  ( A e. V -> ( A " { j } ) e. _V )
114 4 113 syl 
 |-  ( ph -> ( A " { j } ) e. _V )
115 vex 
 |-  j e. _V
116 vex 
 |-  k e. _V
117 115 116 elimasn 
 |-  ( k e. ( A " { j } ) <-> <. j , k >. e. A )
118 df-ov 
 |-  ( j F k ) = ( F ` <. j , k >. )
119 8 ffvelrnda 
 |-  ( ( ph /\ <. j , k >. e. A ) -> ( F ` <. j , k >. ) e. B )
120 118 119 eqeltrid 
 |-  ( ( ph /\ <. j , k >. e. A ) -> ( j F k ) e. B )
121 117 120 sylan2b 
 |-  ( ( ph /\ k e. ( A " { j } ) ) -> ( j F k ) e. B )
122 121 fmpttd 
 |-  ( ph -> ( k e. ( A " { j } ) |-> ( j F k ) ) : ( A " { j } ) --> B )
123 funmpt 
 |-  Fun ( k e. ( A " { j } ) |-> ( j F k ) )
124 123 a1i 
 |-  ( ph -> Fun ( k e. ( A " { j } ) |-> ( j F k ) ) )
125 rnfi 
 |-  ( ( F supp .0. ) e. Fin -> ran ( F supp .0. ) e. Fin )
126 10 125 syl 
 |-  ( ph -> ran ( F supp .0. ) e. Fin )
127 117 biimpi 
 |-  ( k e. ( A " { j } ) -> <. j , k >. e. A )
128 115 116 opelrn 
 |-  ( <. j , k >. e. ( F supp .0. ) -> k e. ran ( F supp .0. ) )
129 128 con3i 
 |-  ( -. k e. ran ( F supp .0. ) -> -. <. j , k >. e. ( F supp .0. ) )
130 127 129 anim12i 
 |-  ( ( k e. ( A " { j } ) /\ -. k e. ran ( F supp .0. ) ) -> ( <. j , k >. e. A /\ -. <. j , k >. e. ( F supp .0. ) ) )
131 eldif 
 |-  ( k e. ( ( A " { j } ) \ ran ( F supp .0. ) ) <-> ( k e. ( A " { j } ) /\ -. k e. ran ( F supp .0. ) ) )
132 eldif 
 |-  ( <. j , k >. e. ( A \ ( F supp .0. ) ) <-> ( <. j , k >. e. A /\ -. <. j , k >. e. ( F supp .0. ) ) )
133 130 131 132 3imtr4i 
 |-  ( k e. ( ( A " { j } ) \ ran ( F supp .0. ) ) -> <. j , k >. e. ( A \ ( F supp .0. ) ) )
134 ssidd 
 |-  ( ph -> ( F supp .0. ) C_ ( F supp .0. ) )
135 62 a1i 
 |-  ( ph -> .0. e. _V )
136 8 134 4 135 suppssr 
 |-  ( ( ph /\ <. j , k >. e. ( A \ ( F supp .0. ) ) ) -> ( F ` <. j , k >. ) = .0. )
137 118 136 syl5eq 
 |-  ( ( ph /\ <. j , k >. e. ( A \ ( F supp .0. ) ) ) -> ( j F k ) = .0. )
138 133 137 sylan2 
 |-  ( ( ph /\ k e. ( ( A " { j } ) \ ran ( F supp .0. ) ) ) -> ( j F k ) = .0. )
139 138 114 suppss2 
 |-  ( ph -> ( ( k e. ( A " { j } ) |-> ( j F k ) ) supp .0. ) C_ ran ( F supp .0. ) )
140 126 139 ssfid 
 |-  ( ph -> ( ( k e. ( A " { j } ) |-> ( j F k ) ) supp .0. ) e. Fin )
141 114 mptexd 
 |-  ( ph -> ( k e. ( A " { j } ) |-> ( j F k ) ) e. _V )
142 isfsupp 
 |-  ( ( ( k e. ( A " { j } ) |-> ( j F k ) ) e. _V /\ .0. e. _V ) -> ( ( k e. ( A " { j } ) |-> ( j F k ) ) finSupp .0. <-> ( Fun ( k e. ( A " { j } ) |-> ( j F k ) ) /\ ( ( k e. ( A " { j } ) |-> ( j F k ) ) supp .0. ) e. Fin ) ) )
143 141 62 142 sylancl 
 |-  ( ph -> ( ( k e. ( A " { j } ) |-> ( j F k ) ) finSupp .0. <-> ( Fun ( k e. ( A " { j } ) |-> ( j F k ) ) /\ ( ( k e. ( A " { j } ) |-> ( j F k ) ) supp .0. ) e. Fin ) ) )
144 124 140 143 mpbir2and 
 |-  ( ph -> ( k e. ( A " { j } ) |-> ( j F k ) ) finSupp .0. )
145 2ndconst 
 |-  ( j e. _V -> ( 2nd |` ( { j } X. ( A " { j } ) ) ) : ( { j } X. ( A " { j } ) ) -1-1-onto-> ( A " { j } ) )
146 115 145 mp1i 
 |-  ( ph -> ( 2nd |` ( { j } X. ( A " { j } ) ) ) : ( { j } X. ( A " { j } ) ) -1-1-onto-> ( A " { j } ) )
147 1 2 3 114 122 144 146 gsumf1o 
 |-  ( ph -> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) = ( G gsum ( ( k e. ( A " { j } ) |-> ( j F k ) ) o. ( 2nd |` ( { j } X. ( A " { j } ) ) ) ) ) )
148 1st2nd2 
 |-  ( x e. ( { j } X. ( A " { j } ) ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
149 xp1st 
 |-  ( x e. ( { j } X. ( A " { j } ) ) -> ( 1st ` x ) e. { j } )
150 elsni 
 |-  ( ( 1st ` x ) e. { j } -> ( 1st ` x ) = j )
151 149 150 syl 
 |-  ( x e. ( { j } X. ( A " { j } ) ) -> ( 1st ` x ) = j )
152 151 opeq1d 
 |-  ( x e. ( { j } X. ( A " { j } ) ) -> <. ( 1st ` x ) , ( 2nd ` x ) >. = <. j , ( 2nd ` x ) >. )
153 148 152 eqtrd 
 |-  ( x e. ( { j } X. ( A " { j } ) ) -> x = <. j , ( 2nd ` x ) >. )
154 153 fveq2d 
 |-  ( x e. ( { j } X. ( A " { j } ) ) -> ( F ` x ) = ( F ` <. j , ( 2nd ` x ) >. ) )
155 df-ov 
 |-  ( j F ( 2nd ` x ) ) = ( F ` <. j , ( 2nd ` x ) >. )
156 154 155 eqtr4di 
 |-  ( x e. ( { j } X. ( A " { j } ) ) -> ( F ` x ) = ( j F ( 2nd ` x ) ) )
157 156 mpteq2ia 
 |-  ( x e. ( { j } X. ( A " { j } ) ) |-> ( F ` x ) ) = ( x e. ( { j } X. ( A " { j } ) ) |-> ( j F ( 2nd ` x ) ) )
158 8 feqmptd 
 |-  ( ph -> F = ( x e. A |-> ( F ` x ) ) )
159 158 reseq1d 
 |-  ( ph -> ( F |` ( A |` { j } ) ) = ( ( x e. A |-> ( F ` x ) ) |` ( A |` { j } ) ) )
160 resss 
 |-  ( A |` { j } ) C_ A
161 resmpt 
 |-  ( ( A |` { j } ) C_ A -> ( ( x e. A |-> ( F ` x ) ) |` ( A |` { j } ) ) = ( x e. ( A |` { j } ) |-> ( F ` x ) ) )
162 160 161 ax-mp 
 |-  ( ( x e. A |-> ( F ` x ) ) |` ( A |` { j } ) ) = ( x e. ( A |` { j } ) |-> ( F ` x ) )
163 ressn 
 |-  ( A |` { j } ) = ( { j } X. ( A " { j } ) )
164 163 mpteq1i 
 |-  ( x e. ( A |` { j } ) |-> ( F ` x ) ) = ( x e. ( { j } X. ( A " { j } ) ) |-> ( F ` x ) )
165 162 164 eqtri 
 |-  ( ( x e. A |-> ( F ` x ) ) |` ( A |` { j } ) ) = ( x e. ( { j } X. ( A " { j } ) ) |-> ( F ` x ) )
166 159 165 eqtrdi 
 |-  ( ph -> ( F |` ( A |` { j } ) ) = ( x e. ( { j } X. ( A " { j } ) ) |-> ( F ` x ) ) )
167 xp2nd 
 |-  ( x e. ( { j } X. ( A " { j } ) ) -> ( 2nd ` x ) e. ( A " { j } ) )
168 167 adantl 
 |-  ( ( ph /\ x e. ( { j } X. ( A " { j } ) ) ) -> ( 2nd ` x ) e. ( A " { j } ) )
169 fo2nd 
 |-  2nd : _V -onto-> _V
170 fof 
 |-  ( 2nd : _V -onto-> _V -> 2nd : _V --> _V )
171 169 170 mp1i 
 |-  ( ph -> 2nd : _V --> _V )
172 171 feqmptd 
 |-  ( ph -> 2nd = ( x e. _V |-> ( 2nd ` x ) ) )
173 172 reseq1d 
 |-  ( ph -> ( 2nd |` ( { j } X. ( A " { j } ) ) ) = ( ( x e. _V |-> ( 2nd ` x ) ) |` ( { j } X. ( A " { j } ) ) ) )
174 ssv 
 |-  ( { j } X. ( A " { j } ) ) C_ _V
175 resmpt 
 |-  ( ( { j } X. ( A " { j } ) ) C_ _V -> ( ( x e. _V |-> ( 2nd ` x ) ) |` ( { j } X. ( A " { j } ) ) ) = ( x e. ( { j } X. ( A " { j } ) ) |-> ( 2nd ` x ) ) )
176 174 175 ax-mp 
 |-  ( ( x e. _V |-> ( 2nd ` x ) ) |` ( { j } X. ( A " { j } ) ) ) = ( x e. ( { j } X. ( A " { j } ) ) |-> ( 2nd ` x ) )
177 173 176 eqtrdi 
 |-  ( ph -> ( 2nd |` ( { j } X. ( A " { j } ) ) ) = ( x e. ( { j } X. ( A " { j } ) ) |-> ( 2nd ` x ) ) )
178 eqidd 
 |-  ( ph -> ( k e. ( A " { j } ) |-> ( j F k ) ) = ( k e. ( A " { j } ) |-> ( j F k ) ) )
179 oveq2 
 |-  ( k = ( 2nd ` x ) -> ( j F k ) = ( j F ( 2nd ` x ) ) )
180 168 177 178 179 fmptco 
 |-  ( ph -> ( ( k e. ( A " { j } ) |-> ( j F k ) ) o. ( 2nd |` ( { j } X. ( A " { j } ) ) ) ) = ( x e. ( { j } X. ( A " { j } ) ) |-> ( j F ( 2nd ` x ) ) ) )
181 157 166 180 3eqtr4a 
 |-  ( ph -> ( F |` ( A |` { j } ) ) = ( ( k e. ( A " { j } ) |-> ( j F k ) ) o. ( 2nd |` ( { j } X. ( A " { j } ) ) ) ) )
182 181 oveq2d 
 |-  ( ph -> ( G gsum ( F |` ( A |` { j } ) ) ) = ( G gsum ( ( k e. ( A " { j } ) |-> ( j F k ) ) o. ( 2nd |` ( { j } X. ( A " { j } ) ) ) ) ) )
183 147 182 eqtr4d 
 |-  ( ph -> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) = ( G gsum ( F |` ( A |` { j } ) ) ) )
184 112 183 chvarvv 
 |-  ( ph -> ( G gsum ( k e. ( A " { z } ) |-> ( z F k ) ) ) = ( G gsum ( F |` ( A |` { z } ) ) ) )
185 184 adantr 
 |-  ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> ( G gsum ( k e. ( A " { z } ) |-> ( z F k ) ) ) = ( G gsum ( F |` ( A |` { z } ) ) ) )
186 185 oveq2d 
 |-  ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> ( ( G gsum ( j e. y |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) ( +g ` G ) ( G gsum ( k e. ( A " { z } ) |-> ( z F k ) ) ) ) = ( ( G gsum ( j e. y |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) ( +g ` G ) ( G gsum ( F |` ( A |` { z } ) ) ) ) )
187 107 186 eqtrd 
 |-  ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> ( G gsum ( j e. ( y u. { z } ) |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) = ( ( G gsum ( j e. y |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) ( +g ` G ) ( G gsum ( F |` ( A |` { z } ) ) ) ) )
188 92 187 eqeq12d 
 |-  ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> ( ( G gsum ( F |` ( A |` ( y u. { z } ) ) ) ) = ( G gsum ( j e. ( y u. { z } ) |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) <-> ( ( G gsum ( F |` ( A |` y ) ) ) ( +g ` G ) ( G gsum ( F |` ( A |` { z } ) ) ) ) = ( ( G gsum ( j e. y |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) ( +g ` G ) ( G gsum ( F |` ( A |` { z } ) ) ) ) ) )
189 48 188 syl5ibr 
 |-  ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> ( ( G gsum ( F |` ( A |` y ) ) ) = ( G gsum ( j e. y |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) -> ( G gsum ( F |` ( A |` ( y u. { z } ) ) ) ) = ( G gsum ( j e. ( y u. { z } ) |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) ) )
190 189 expcom 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( ph -> ( ( G gsum ( F |` ( A |` y ) ) ) = ( G gsum ( j e. y |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) -> ( G gsum ( F |` ( A |` ( y u. { z } ) ) ) ) = ( G gsum ( j e. ( y u. { z } ) |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) ) ) )
191 190 a2d 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( ( ph -> ( G gsum ( F |` ( A |` y ) ) ) = ( G gsum ( j e. y |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) ) -> ( ph -> ( G gsum ( F |` ( A |` ( y u. { z } ) ) ) ) = ( G gsum ( j e. ( y u. { z } ) |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) ) ) )
192 25 32 39 46 47 191 findcard2s 
 |-  ( dom ( F supp .0. ) e. Fin -> ( ph -> ( G gsum ( F |` ( A |` dom ( F supp .0. ) ) ) ) = ( G gsum ( j e. dom ( F supp .0. ) |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) ) )
193 12 192 mpcom 
 |-  ( ph -> ( G gsum ( F |` ( A |` dom ( F supp .0. ) ) ) ) = ( G gsum ( j e. dom ( F supp .0. ) |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) )