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 resexg 
 |-  ( A e. V -> ( A |` ( y u. { z } ) ) e. _V )
52 4 51 syl 
 |-  ( ph -> ( A |` ( y u. { z } ) ) e. _V )
53 52 adantr 
 |-  ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> ( A |` ( y u. { z } ) ) e. _V )
54 resss 
 |-  ( A |` ( y u. { z } ) ) C_ A
55 fssres 
 |-  ( ( F : A --> B /\ ( A |` ( y u. { z } ) ) C_ A ) -> ( F |` ( A |` ( y u. { z } ) ) ) : ( A |` ( y u. { z } ) ) --> B )
56 8 54 55 sylancl 
 |-  ( ph -> ( F |` ( A |` ( y u. { z } ) ) ) : ( A |` ( y u. { z } ) ) --> B )
57 56 adantr 
 |-  ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> ( F |` ( A |` ( y u. { z } ) ) ) : ( A |` ( y u. { z } ) ) --> B )
58 8 ffund 
 |-  ( ph -> Fun F )
59 funres 
 |-  ( Fun F -> Fun ( F |` ( A |` ( y u. { z } ) ) ) )
60 58 59 syl 
 |-  ( ph -> Fun ( F |` ( A |` ( y u. { z } ) ) ) )
61 60 adantr 
 |-  ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> Fun ( F |` ( A |` ( y u. { z } ) ) ) )
62 10 adantr 
 |-  ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> ( F supp .0. ) e. Fin )
63 fex 
 |-  ( ( F : A --> B /\ A e. V ) -> F e. _V )
64 8 4 63 syl2anc 
 |-  ( ph -> F e. _V )
65 2 fvexi 
 |-  .0. e. _V
66 ressuppss 
 |-  ( ( F e. _V /\ .0. e. _V ) -> ( ( F |` ( A |` ( y u. { z } ) ) ) supp .0. ) C_ ( F supp .0. ) )
67 64 65 66 sylancl 
 |-  ( ph -> ( ( F |` ( A |` ( y u. { z } ) ) ) supp .0. ) C_ ( F supp .0. ) )
68 67 adantr 
 |-  ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> ( ( F |` ( A |` ( y u. { z } ) ) ) supp .0. ) C_ ( F supp .0. ) )
69 62 68 ssfid 
 |-  ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> ( ( F |` ( A |` ( y u. { z } ) ) ) supp .0. ) e. Fin )
70 resexg 
 |-  ( F e. _V -> ( F |` ( A |` ( y u. { z } ) ) ) e. _V )
71 64 70 syl 
 |-  ( ph -> ( F |` ( A |` ( y u. { z } ) ) ) e. _V )
72 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 ) ) )
73 71 65 72 sylancl 
 |-  ( ph -> ( ( F |` ( A |` ( y u. { z } ) ) ) finSupp .0. <-> ( Fun ( F |` ( A |` ( y u. { z } ) ) ) /\ ( ( F |` ( A |` ( y u. { z } ) ) ) supp .0. ) e. Fin ) ) )
74 73 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 ) ) )
75 61 69 74 mpbir2and 
 |-  ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> ( F |` ( A |` ( y u. { z } ) ) ) finSupp .0. )
76 simprr 
 |-  ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> -. z e. y )
77 disjsn 
 |-  ( ( y i^i { z } ) = (/) <-> -. z e. y )
78 76 77 sylibr 
 |-  ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> ( y i^i { z } ) = (/) )
79 78 reseq2d 
 |-  ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> ( A |` ( y i^i { z } ) ) = ( A |` (/) ) )
80 resindi 
 |-  ( A |` ( y i^i { z } ) ) = ( ( A |` y ) i^i ( A |` { z } ) )
81 79 80 14 3eqtr3g 
 |-  ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> ( ( A |` y ) i^i ( A |` { z } ) ) = (/) )
82 resundi 
 |-  ( A |` ( y u. { z } ) ) = ( ( A |` y ) u. ( A |` { z } ) )
83 82 a1i 
 |-  ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> ( A |` ( y u. { z } ) ) = ( ( A |` y ) u. ( A |` { z } ) ) )
84 1 2 49 50 53 57 75 81 83 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 } ) ) ) ) )
85 ssun1 
 |-  y C_ ( y u. { z } )
86 ssres2 
 |-  ( y C_ ( y u. { z } ) -> ( A |` y ) C_ ( A |` ( y u. { z } ) ) )
87 resabs1 
 |-  ( ( A |` y ) C_ ( A |` ( y u. { z } ) ) -> ( ( F |` ( A |` ( y u. { z } ) ) ) |` ( A |` y ) ) = ( F |` ( A |` y ) ) )
88 85 86 87 mp2b 
 |-  ( ( F |` ( A |` ( y u. { z } ) ) ) |` ( A |` y ) ) = ( F |` ( A |` y ) )
89 88 oveq2i 
 |-  ( G gsum ( ( F |` ( A |` ( y u. { z } ) ) ) |` ( A |` y ) ) ) = ( G gsum ( F |` ( A |` y ) ) )
90 ssun2 
 |-  { z } C_ ( y u. { z } )
91 ssres2 
 |-  ( { z } C_ ( y u. { z } ) -> ( A |` { z } ) C_ ( A |` ( y u. { z } ) ) )
92 resabs1 
 |-  ( ( A |` { z } ) C_ ( A |` ( y u. { z } ) ) -> ( ( F |` ( A |` ( y u. { z } ) ) ) |` ( A |` { z } ) ) = ( F |` ( A |` { z } ) ) )
93 90 91 92 mp2b 
 |-  ( ( F |` ( A |` ( y u. { z } ) ) ) |` ( A |` { z } ) ) = ( F |` ( A |` { z } ) )
94 93 oveq2i 
 |-  ( G gsum ( ( F |` ( A |` ( y u. { z } ) ) ) |` ( A |` { z } ) ) ) = ( G gsum ( F |` ( A |` { z } ) ) )
95 89 94 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 } ) ) ) )
96 84 95 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 } ) ) ) ) )
97 simprl 
 |-  ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> y e. Fin )
98 1 2 3 4 5 6 7 8 9 gsum2dlem1 
 |-  ( ph -> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) e. B )
99 98 ad2antrr 
 |-  ( ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) /\ j e. y ) -> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) e. B )
100 vex 
 |-  z e. _V
101 100 a1i 
 |-  ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> z e. _V )
102 sneq 
 |-  ( j = z -> { j } = { z } )
103 102 imaeq2d 
 |-  ( j = z -> ( A " { j } ) = ( A " { z } ) )
104 oveq1 
 |-  ( j = z -> ( j F k ) = ( z F k ) )
105 103 104 mpteq12dv 
 |-  ( j = z -> ( k e. ( A " { j } ) |-> ( j F k ) ) = ( k e. ( A " { z } ) |-> ( z F k ) ) )
106 105 oveq2d 
 |-  ( j = z -> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) = ( G gsum ( k e. ( A " { z } ) |-> ( z F k ) ) ) )
107 106 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 ) )
108 107 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 ) ) )
109 108 98 chvarvv 
 |-  ( ph -> ( G gsum ( k e. ( A " { z } ) |-> ( z F k ) ) ) e. B )
110 109 adantr 
 |-  ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> ( G gsum ( k e. ( A " { z } ) |-> ( z F k ) ) ) e. B )
111 1 49 50 97 99 101 76 110 106 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 ) ) ) ) )
112 102 reseq2d 
 |-  ( j = z -> ( A |` { j } ) = ( A |` { z } ) )
113 112 reseq2d 
 |-  ( j = z -> ( F |` ( A |` { j } ) ) = ( F |` ( A |` { z } ) ) )
114 113 oveq2d 
 |-  ( j = z -> ( G gsum ( F |` ( A |` { j } ) ) ) = ( G gsum ( F |` ( A |` { z } ) ) ) )
115 106 114 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 } ) ) ) ) )
116 115 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 } ) ) ) ) ) )
117 imaexg 
 |-  ( A e. V -> ( A " { j } ) e. _V )
118 4 117 syl 
 |-  ( ph -> ( A " { j } ) e. _V )
119 vex 
 |-  j e. _V
120 vex 
 |-  k e. _V
121 119 120 elimasn 
 |-  ( k e. ( A " { j } ) <-> <. j , k >. e. A )
122 df-ov 
 |-  ( j F k ) = ( F ` <. j , k >. )
123 8 ffvelrnda 
 |-  ( ( ph /\ <. j , k >. e. A ) -> ( F ` <. j , k >. ) e. B )
124 122 123 eqeltrid 
 |-  ( ( ph /\ <. j , k >. e. A ) -> ( j F k ) e. B )
125 121 124 sylan2b 
 |-  ( ( ph /\ k e. ( A " { j } ) ) -> ( j F k ) e. B )
126 125 fmpttd 
 |-  ( ph -> ( k e. ( A " { j } ) |-> ( j F k ) ) : ( A " { j } ) --> B )
127 funmpt 
 |-  Fun ( k e. ( A " { j } ) |-> ( j F k ) )
128 127 a1i 
 |-  ( ph -> Fun ( k e. ( A " { j } ) |-> ( j F k ) ) )
129 rnfi 
 |-  ( ( F supp .0. ) e. Fin -> ran ( F supp .0. ) e. Fin )
130 10 129 syl 
 |-  ( ph -> ran ( F supp .0. ) e. Fin )
131 121 biimpi 
 |-  ( k e. ( A " { j } ) -> <. j , k >. e. A )
132 119 120 opelrn 
 |-  ( <. j , k >. e. ( F supp .0. ) -> k e. ran ( F supp .0. ) )
133 132 con3i 
 |-  ( -. k e. ran ( F supp .0. ) -> -. <. j , k >. e. ( F supp .0. ) )
134 131 133 anim12i 
 |-  ( ( k e. ( A " { j } ) /\ -. k e. ran ( F supp .0. ) ) -> ( <. j , k >. e. A /\ -. <. j , k >. e. ( F supp .0. ) ) )
135 eldif 
 |-  ( k e. ( ( A " { j } ) \ ran ( F supp .0. ) ) <-> ( k e. ( A " { j } ) /\ -. k e. ran ( F supp .0. ) ) )
136 eldif 
 |-  ( <. j , k >. e. ( A \ ( F supp .0. ) ) <-> ( <. j , k >. e. A /\ -. <. j , k >. e. ( F supp .0. ) ) )
137 134 135 136 3imtr4i 
 |-  ( k e. ( ( A " { j } ) \ ran ( F supp .0. ) ) -> <. j , k >. e. ( A \ ( F supp .0. ) ) )
138 ssidd 
 |-  ( ph -> ( F supp .0. ) C_ ( F supp .0. ) )
139 65 a1i 
 |-  ( ph -> .0. e. _V )
140 8 138 4 139 suppssr 
 |-  ( ( ph /\ <. j , k >. e. ( A \ ( F supp .0. ) ) ) -> ( F ` <. j , k >. ) = .0. )
141 122 140 syl5eq 
 |-  ( ( ph /\ <. j , k >. e. ( A \ ( F supp .0. ) ) ) -> ( j F k ) = .0. )
142 137 141 sylan2 
 |-  ( ( ph /\ k e. ( ( A " { j } ) \ ran ( F supp .0. ) ) ) -> ( j F k ) = .0. )
143 142 118 suppss2 
 |-  ( ph -> ( ( k e. ( A " { j } ) |-> ( j F k ) ) supp .0. ) C_ ran ( F supp .0. ) )
144 130 143 ssfid 
 |-  ( ph -> ( ( k e. ( A " { j } ) |-> ( j F k ) ) supp .0. ) e. Fin )
145 118 mptexd 
 |-  ( ph -> ( k e. ( A " { j } ) |-> ( j F k ) ) e. _V )
146 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 ) ) )
147 145 65 146 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 ) ) )
148 128 144 147 mpbir2and 
 |-  ( ph -> ( k e. ( A " { j } ) |-> ( j F k ) ) finSupp .0. )
149 2ndconst 
 |-  ( j e. _V -> ( 2nd |` ( { j } X. ( A " { j } ) ) ) : ( { j } X. ( A " { j } ) ) -1-1-onto-> ( A " { j } ) )
150 119 149 mp1i 
 |-  ( ph -> ( 2nd |` ( { j } X. ( A " { j } ) ) ) : ( { j } X. ( A " { j } ) ) -1-1-onto-> ( A " { j } ) )
151 1 2 3 118 126 148 150 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 } ) ) ) ) ) )
152 1st2nd2 
 |-  ( x e. ( { j } X. ( A " { j } ) ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
153 xp1st 
 |-  ( x e. ( { j } X. ( A " { j } ) ) -> ( 1st ` x ) e. { j } )
154 elsni 
 |-  ( ( 1st ` x ) e. { j } -> ( 1st ` x ) = j )
155 153 154 syl 
 |-  ( x e. ( { j } X. ( A " { j } ) ) -> ( 1st ` x ) = j )
156 155 opeq1d 
 |-  ( x e. ( { j } X. ( A " { j } ) ) -> <. ( 1st ` x ) , ( 2nd ` x ) >. = <. j , ( 2nd ` x ) >. )
157 152 156 eqtrd 
 |-  ( x e. ( { j } X. ( A " { j } ) ) -> x = <. j , ( 2nd ` x ) >. )
158 157 fveq2d 
 |-  ( x e. ( { j } X. ( A " { j } ) ) -> ( F ` x ) = ( F ` <. j , ( 2nd ` x ) >. ) )
159 df-ov 
 |-  ( j F ( 2nd ` x ) ) = ( F ` <. j , ( 2nd ` x ) >. )
160 158 159 eqtr4di 
 |-  ( x e. ( { j } X. ( A " { j } ) ) -> ( F ` x ) = ( j F ( 2nd ` x ) ) )
161 160 mpteq2ia 
 |-  ( x e. ( { j } X. ( A " { j } ) ) |-> ( F ` x ) ) = ( x e. ( { j } X. ( A " { j } ) ) |-> ( j F ( 2nd ` x ) ) )
162 8 feqmptd 
 |-  ( ph -> F = ( x e. A |-> ( F ` x ) ) )
163 162 reseq1d 
 |-  ( ph -> ( F |` ( A |` { j } ) ) = ( ( x e. A |-> ( F ` x ) ) |` ( A |` { j } ) ) )
164 resss 
 |-  ( A |` { j } ) C_ A
165 resmpt 
 |-  ( ( A |` { j } ) C_ A -> ( ( x e. A |-> ( F ` x ) ) |` ( A |` { j } ) ) = ( x e. ( A |` { j } ) |-> ( F ` x ) ) )
166 164 165 ax-mp 
 |-  ( ( x e. A |-> ( F ` x ) ) |` ( A |` { j } ) ) = ( x e. ( A |` { j } ) |-> ( F ` x ) )
167 ressn 
 |-  ( A |` { j } ) = ( { j } X. ( A " { j } ) )
168 167 mpteq1i 
 |-  ( x e. ( A |` { j } ) |-> ( F ` x ) ) = ( x e. ( { j } X. ( A " { j } ) ) |-> ( F ` x ) )
169 166 168 eqtri 
 |-  ( ( x e. A |-> ( F ` x ) ) |` ( A |` { j } ) ) = ( x e. ( { j } X. ( A " { j } ) ) |-> ( F ` x ) )
170 163 169 eqtrdi 
 |-  ( ph -> ( F |` ( A |` { j } ) ) = ( x e. ( { j } X. ( A " { j } ) ) |-> ( F ` x ) ) )
171 xp2nd 
 |-  ( x e. ( { j } X. ( A " { j } ) ) -> ( 2nd ` x ) e. ( A " { j } ) )
172 171 adantl 
 |-  ( ( ph /\ x e. ( { j } X. ( A " { j } ) ) ) -> ( 2nd ` x ) e. ( A " { j } ) )
173 fo2nd 
 |-  2nd : _V -onto-> _V
174 fof 
 |-  ( 2nd : _V -onto-> _V -> 2nd : _V --> _V )
175 173 174 mp1i 
 |-  ( ph -> 2nd : _V --> _V )
176 175 feqmptd 
 |-  ( ph -> 2nd = ( x e. _V |-> ( 2nd ` x ) ) )
177 176 reseq1d 
 |-  ( ph -> ( 2nd |` ( { j } X. ( A " { j } ) ) ) = ( ( x e. _V |-> ( 2nd ` x ) ) |` ( { j } X. ( A " { j } ) ) ) )
178 ssv 
 |-  ( { j } X. ( A " { j } ) ) C_ _V
179 resmpt 
 |-  ( ( { j } X. ( A " { j } ) ) C_ _V -> ( ( x e. _V |-> ( 2nd ` x ) ) |` ( { j } X. ( A " { j } ) ) ) = ( x e. ( { j } X. ( A " { j } ) ) |-> ( 2nd ` x ) ) )
180 178 179 ax-mp 
 |-  ( ( x e. _V |-> ( 2nd ` x ) ) |` ( { j } X. ( A " { j } ) ) ) = ( x e. ( { j } X. ( A " { j } ) ) |-> ( 2nd ` x ) )
181 177 180 eqtrdi 
 |-  ( ph -> ( 2nd |` ( { j } X. ( A " { j } ) ) ) = ( x e. ( { j } X. ( A " { j } ) ) |-> ( 2nd ` x ) ) )
182 eqidd 
 |-  ( ph -> ( k e. ( A " { j } ) |-> ( j F k ) ) = ( k e. ( A " { j } ) |-> ( j F k ) ) )
183 oveq2 
 |-  ( k = ( 2nd ` x ) -> ( j F k ) = ( j F ( 2nd ` x ) ) )
184 172 181 182 183 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 ) ) ) )
185 161 170 184 3eqtr4a 
 |-  ( ph -> ( F |` ( A |` { j } ) ) = ( ( k e. ( A " { j } ) |-> ( j F k ) ) o. ( 2nd |` ( { j } X. ( A " { j } ) ) ) ) )
186 185 oveq2d 
 |-  ( ph -> ( G gsum ( F |` ( A |` { j } ) ) ) = ( G gsum ( ( k e. ( A " { j } ) |-> ( j F k ) ) o. ( 2nd |` ( { j } X. ( A " { j } ) ) ) ) ) )
187 151 186 eqtr4d 
 |-  ( ph -> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) = ( G gsum ( F |` ( A |` { j } ) ) ) )
188 116 187 chvarvv 
 |-  ( ph -> ( G gsum ( k e. ( A " { z } ) |-> ( z F k ) ) ) = ( G gsum ( F |` ( A |` { z } ) ) ) )
189 188 adantr 
 |-  ( ( ph /\ ( y e. Fin /\ -. z e. y ) ) -> ( G gsum ( k e. ( A " { z } ) |-> ( z F k ) ) ) = ( G gsum ( F |` ( A |` { z } ) ) ) )
190 189 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 } ) ) ) ) )
191 111 190 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 } ) ) ) ) )
192 96 191 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 } ) ) ) ) ) )
193 48 192 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 ) ) ) ) ) ) )
194 193 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 ) ) ) ) ) ) ) )
195 194 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 ) ) ) ) ) ) ) )
196 25 32 39 46 47 195 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 ) ) ) ) ) ) )
197 12 196 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 ) ) ) ) ) )