Metamath Proof Explorer


Theorem tmdgsum

Description: In a topological monoid, the group sum operation is a continuous function from the function space to the base topology. This theorem is not true when A is infinite, because in this case for any basic open set of the domain one of the factors will be the whole space, so by varying the value of the functions to sum at this index, one can achieve any desired sum. (Contributed by Mario Carneiro, 19-Sep-2015) (Proof shortened by AV, 24-Jul-2019)

Ref Expression
Hypotheses tmdgsum.j
|- J = ( TopOpen ` G )
tmdgsum.b
|- B = ( Base ` G )
Assertion tmdgsum
|- ( ( G e. CMnd /\ G e. TopMnd /\ A e. Fin ) -> ( x e. ( B ^m A ) |-> ( G gsum x ) ) e. ( ( J ^ko ~P A ) Cn J ) )

Proof

Step Hyp Ref Expression
1 tmdgsum.j
 |-  J = ( TopOpen ` G )
2 tmdgsum.b
 |-  B = ( Base ` G )
3 oveq2
 |-  ( w = (/) -> ( B ^m w ) = ( B ^m (/) ) )
4 3 mpteq1d
 |-  ( w = (/) -> ( x e. ( B ^m w ) |-> ( G gsum x ) ) = ( x e. ( B ^m (/) ) |-> ( G gsum x ) ) )
5 xpeq1
 |-  ( w = (/) -> ( w X. { J } ) = ( (/) X. { J } ) )
6 0xp
 |-  ( (/) X. { J } ) = (/)
7 5 6 eqtrdi
 |-  ( w = (/) -> ( w X. { J } ) = (/) )
8 7 fveq2d
 |-  ( w = (/) -> ( Xt_ ` ( w X. { J } ) ) = ( Xt_ ` (/) ) )
9 8 oveq1d
 |-  ( w = (/) -> ( ( Xt_ ` ( w X. { J } ) ) Cn J ) = ( ( Xt_ ` (/) ) Cn J ) )
10 4 9 eleq12d
 |-  ( w = (/) -> ( ( x e. ( B ^m w ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( w X. { J } ) ) Cn J ) <-> ( x e. ( B ^m (/) ) |-> ( G gsum x ) ) e. ( ( Xt_ ` (/) ) Cn J ) ) )
11 10 imbi2d
 |-  ( w = (/) -> ( ( ( G e. CMnd /\ G e. TopMnd ) -> ( x e. ( B ^m w ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( w X. { J } ) ) Cn J ) ) <-> ( ( G e. CMnd /\ G e. TopMnd ) -> ( x e. ( B ^m (/) ) |-> ( G gsum x ) ) e. ( ( Xt_ ` (/) ) Cn J ) ) ) )
12 oveq2
 |-  ( w = y -> ( B ^m w ) = ( B ^m y ) )
13 12 mpteq1d
 |-  ( w = y -> ( x e. ( B ^m w ) |-> ( G gsum x ) ) = ( x e. ( B ^m y ) |-> ( G gsum x ) ) )
14 xpeq1
 |-  ( w = y -> ( w X. { J } ) = ( y X. { J } ) )
15 14 fveq2d
 |-  ( w = y -> ( Xt_ ` ( w X. { J } ) ) = ( Xt_ ` ( y X. { J } ) ) )
16 15 oveq1d
 |-  ( w = y -> ( ( Xt_ ` ( w X. { J } ) ) Cn J ) = ( ( Xt_ ` ( y X. { J } ) ) Cn J ) )
17 13 16 eleq12d
 |-  ( w = y -> ( ( x e. ( B ^m w ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( w X. { J } ) ) Cn J ) <-> ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) )
18 17 imbi2d
 |-  ( w = y -> ( ( ( G e. CMnd /\ G e. TopMnd ) -> ( x e. ( B ^m w ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( w X. { J } ) ) Cn J ) ) <-> ( ( G e. CMnd /\ G e. TopMnd ) -> ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) ) )
19 oveq2
 |-  ( w = ( y u. { z } ) -> ( B ^m w ) = ( B ^m ( y u. { z } ) ) )
20 19 mpteq1d
 |-  ( w = ( y u. { z } ) -> ( x e. ( B ^m w ) |-> ( G gsum x ) ) = ( x e. ( B ^m ( y u. { z } ) ) |-> ( G gsum x ) ) )
21 xpeq1
 |-  ( w = ( y u. { z } ) -> ( w X. { J } ) = ( ( y u. { z } ) X. { J } ) )
22 21 fveq2d
 |-  ( w = ( y u. { z } ) -> ( Xt_ ` ( w X. { J } ) ) = ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) )
23 22 oveq1d
 |-  ( w = ( y u. { z } ) -> ( ( Xt_ ` ( w X. { J } ) ) Cn J ) = ( ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) Cn J ) )
24 20 23 eleq12d
 |-  ( w = ( y u. { z } ) -> ( ( x e. ( B ^m w ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( w X. { J } ) ) Cn J ) <-> ( x e. ( B ^m ( y u. { z } ) ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) Cn J ) ) )
25 24 imbi2d
 |-  ( w = ( y u. { z } ) -> ( ( ( G e. CMnd /\ G e. TopMnd ) -> ( x e. ( B ^m w ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( w X. { J } ) ) Cn J ) ) <-> ( ( G e. CMnd /\ G e. TopMnd ) -> ( x e. ( B ^m ( y u. { z } ) ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) Cn J ) ) ) )
26 oveq2
 |-  ( w = A -> ( B ^m w ) = ( B ^m A ) )
27 26 mpteq1d
 |-  ( w = A -> ( x e. ( B ^m w ) |-> ( G gsum x ) ) = ( x e. ( B ^m A ) |-> ( G gsum x ) ) )
28 xpeq1
 |-  ( w = A -> ( w X. { J } ) = ( A X. { J } ) )
29 28 fveq2d
 |-  ( w = A -> ( Xt_ ` ( w X. { J } ) ) = ( Xt_ ` ( A X. { J } ) ) )
30 29 oveq1d
 |-  ( w = A -> ( ( Xt_ ` ( w X. { J } ) ) Cn J ) = ( ( Xt_ ` ( A X. { J } ) ) Cn J ) )
31 27 30 eleq12d
 |-  ( w = A -> ( ( x e. ( B ^m w ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( w X. { J } ) ) Cn J ) <-> ( x e. ( B ^m A ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( A X. { J } ) ) Cn J ) ) )
32 31 imbi2d
 |-  ( w = A -> ( ( ( G e. CMnd /\ G e. TopMnd ) -> ( x e. ( B ^m w ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( w X. { J } ) ) Cn J ) ) <-> ( ( G e. CMnd /\ G e. TopMnd ) -> ( x e. ( B ^m A ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( A X. { J } ) ) Cn J ) ) ) )
33 elmapfn
 |-  ( x e. ( B ^m (/) ) -> x Fn (/) )
34 fn0
 |-  ( x Fn (/) <-> x = (/) )
35 33 34 sylib
 |-  ( x e. ( B ^m (/) ) -> x = (/) )
36 35 oveq2d
 |-  ( x e. ( B ^m (/) ) -> ( G gsum x ) = ( G gsum (/) ) )
37 eqid
 |-  ( 0g ` G ) = ( 0g ` G )
38 37 gsum0
 |-  ( G gsum (/) ) = ( 0g ` G )
39 36 38 eqtrdi
 |-  ( x e. ( B ^m (/) ) -> ( G gsum x ) = ( 0g ` G ) )
40 39 mpteq2ia
 |-  ( x e. ( B ^m (/) ) |-> ( G gsum x ) ) = ( x e. ( B ^m (/) ) |-> ( 0g ` G ) )
41 0ex
 |-  (/) e. _V
42 1 2 tmdtopon
 |-  ( G e. TopMnd -> J e. ( TopOn ` B ) )
43 42 adantl
 |-  ( ( G e. CMnd /\ G e. TopMnd ) -> J e. ( TopOn ` B ) )
44 6 fveq2i
 |-  ( Xt_ ` ( (/) X. { J } ) ) = ( Xt_ ` (/) )
45 44 eqcomi
 |-  ( Xt_ ` (/) ) = ( Xt_ ` ( (/) X. { J } ) )
46 45 pttoponconst
 |-  ( ( (/) e. _V /\ J e. ( TopOn ` B ) ) -> ( Xt_ ` (/) ) e. ( TopOn ` ( B ^m (/) ) ) )
47 41 43 46 sylancr
 |-  ( ( G e. CMnd /\ G e. TopMnd ) -> ( Xt_ ` (/) ) e. ( TopOn ` ( B ^m (/) ) ) )
48 tmdmnd
 |-  ( G e. TopMnd -> G e. Mnd )
49 48 adantl
 |-  ( ( G e. CMnd /\ G e. TopMnd ) -> G e. Mnd )
50 2 37 mndidcl
 |-  ( G e. Mnd -> ( 0g ` G ) e. B )
51 49 50 syl
 |-  ( ( G e. CMnd /\ G e. TopMnd ) -> ( 0g ` G ) e. B )
52 47 43 51 cnmptc
 |-  ( ( G e. CMnd /\ G e. TopMnd ) -> ( x e. ( B ^m (/) ) |-> ( 0g ` G ) ) e. ( ( Xt_ ` (/) ) Cn J ) )
53 40 52 eqeltrid
 |-  ( ( G e. CMnd /\ G e. TopMnd ) -> ( x e. ( B ^m (/) ) |-> ( G gsum x ) ) e. ( ( Xt_ ` (/) ) Cn J ) )
54 oveq2
 |-  ( x = w -> ( G gsum x ) = ( G gsum w ) )
55 54 cbvmptv
 |-  ( x e. ( B ^m ( y u. { z } ) ) |-> ( G gsum x ) ) = ( w e. ( B ^m ( y u. { z } ) ) |-> ( G gsum w ) )
56 eqid
 |-  ( +g ` G ) = ( +g ` G )
57 simpl1l
 |-  ( ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) /\ w e. ( B ^m ( y u. { z } ) ) ) -> G e. CMnd )
58 simp2l
 |-  ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> y e. Fin )
59 snfi
 |-  { z } e. Fin
60 unfi
 |-  ( ( y e. Fin /\ { z } e. Fin ) -> ( y u. { z } ) e. Fin )
61 58 59 60 sylancl
 |-  ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> ( y u. { z } ) e. Fin )
62 61 adantr
 |-  ( ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) /\ w e. ( B ^m ( y u. { z } ) ) ) -> ( y u. { z } ) e. Fin )
63 elmapi
 |-  ( w e. ( B ^m ( y u. { z } ) ) -> w : ( y u. { z } ) --> B )
64 63 adantl
 |-  ( ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) /\ w e. ( B ^m ( y u. { z } ) ) ) -> w : ( y u. { z } ) --> B )
65 fvexd
 |-  ( ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) /\ w e. ( B ^m ( y u. { z } ) ) ) -> ( 0g ` G ) e. _V )
66 64 62 65 fdmfifsupp
 |-  ( ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) /\ w e. ( B ^m ( y u. { z } ) ) ) -> w finSupp ( 0g ` G ) )
67 simpl2r
 |-  ( ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) /\ w e. ( B ^m ( y u. { z } ) ) ) -> -. z e. y )
68 disjsn
 |-  ( ( y i^i { z } ) = (/) <-> -. z e. y )
69 67 68 sylibr
 |-  ( ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) /\ w e. ( B ^m ( y u. { z } ) ) ) -> ( y i^i { z } ) = (/) )
70 eqidd
 |-  ( ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) /\ w e. ( B ^m ( y u. { z } ) ) ) -> ( y u. { z } ) = ( y u. { z } ) )
71 2 37 56 57 62 64 66 69 70 gsumsplit
 |-  ( ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) /\ w e. ( B ^m ( y u. { z } ) ) ) -> ( G gsum w ) = ( ( G gsum ( w |` y ) ) ( +g ` G ) ( G gsum ( w |` { z } ) ) ) )
72 71 mpteq2dva
 |-  ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> ( w e. ( B ^m ( y u. { z } ) ) |-> ( G gsum w ) ) = ( w e. ( B ^m ( y u. { z } ) ) |-> ( ( G gsum ( w |` y ) ) ( +g ` G ) ( G gsum ( w |` { z } ) ) ) ) )
73 55 72 syl5eq
 |-  ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> ( x e. ( B ^m ( y u. { z } ) ) |-> ( G gsum x ) ) = ( w e. ( B ^m ( y u. { z } ) ) |-> ( ( G gsum ( w |` y ) ) ( +g ` G ) ( G gsum ( w |` { z } ) ) ) ) )
74 simp1r
 |-  ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> G e. TopMnd )
75 74 42 syl
 |-  ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> J e. ( TopOn ` B ) )
76 eqid
 |-  ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) = ( Xt_ ` ( ( y u. { z } ) X. { J } ) )
77 76 pttoponconst
 |-  ( ( ( y u. { z } ) e. Fin /\ J e. ( TopOn ` B ) ) -> ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) e. ( TopOn ` ( B ^m ( y u. { z } ) ) ) )
78 61 75 77 syl2anc
 |-  ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) e. ( TopOn ` ( B ^m ( y u. { z } ) ) ) )
79 toponuni
 |-  ( ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) e. ( TopOn ` ( B ^m ( y u. { z } ) ) ) -> ( B ^m ( y u. { z } ) ) = U. ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) )
80 78 79 syl
 |-  ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> ( B ^m ( y u. { z } ) ) = U. ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) )
81 80 mpteq1d
 |-  ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> ( w e. ( B ^m ( y u. { z } ) ) |-> ( w |` y ) ) = ( w e. U. ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) |-> ( w |` y ) ) )
82 topontop
 |-  ( J e. ( TopOn ` B ) -> J e. Top )
83 74 42 82 3syl
 |-  ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> J e. Top )
84 fconst6g
 |-  ( J e. Top -> ( ( y u. { z } ) X. { J } ) : ( y u. { z } ) --> Top )
85 83 84 syl
 |-  ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> ( ( y u. { z } ) X. { J } ) : ( y u. { z } ) --> Top )
86 ssun1
 |-  y C_ ( y u. { z } )
87 86 a1i
 |-  ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> y C_ ( y u. { z } ) )
88 eqid
 |-  U. ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) = U. ( Xt_ ` ( ( y u. { z } ) X. { J } ) )
89 xpssres
 |-  ( y C_ ( y u. { z } ) -> ( ( ( y u. { z } ) X. { J } ) |` y ) = ( y X. { J } ) )
90 86 89 ax-mp
 |-  ( ( ( y u. { z } ) X. { J } ) |` y ) = ( y X. { J } )
91 90 eqcomi
 |-  ( y X. { J } ) = ( ( ( y u. { z } ) X. { J } ) |` y )
92 91 fveq2i
 |-  ( Xt_ ` ( y X. { J } ) ) = ( Xt_ ` ( ( ( y u. { z } ) X. { J } ) |` y ) )
93 88 76 92 ptrescn
 |-  ( ( ( y u. { z } ) e. Fin /\ ( ( y u. { z } ) X. { J } ) : ( y u. { z } ) --> Top /\ y C_ ( y u. { z } ) ) -> ( w e. U. ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) |-> ( w |` y ) ) e. ( ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) Cn ( Xt_ ` ( y X. { J } ) ) ) )
94 61 85 87 93 syl3anc
 |-  ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> ( w e. U. ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) |-> ( w |` y ) ) e. ( ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) Cn ( Xt_ ` ( y X. { J } ) ) ) )
95 81 94 eqeltrd
 |-  ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> ( w e. ( B ^m ( y u. { z } ) ) |-> ( w |` y ) ) e. ( ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) Cn ( Xt_ ` ( y X. { J } ) ) ) )
96 eqid
 |-  ( Xt_ ` ( y X. { J } ) ) = ( Xt_ ` ( y X. { J } ) )
97 96 pttoponconst
 |-  ( ( y e. Fin /\ J e. ( TopOn ` B ) ) -> ( Xt_ ` ( y X. { J } ) ) e. ( TopOn ` ( B ^m y ) ) )
98 58 75 97 syl2anc
 |-  ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> ( Xt_ ` ( y X. { J } ) ) e. ( TopOn ` ( B ^m y ) ) )
99 simp3
 |-  ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) )
100 oveq2
 |-  ( x = ( w |` y ) -> ( G gsum x ) = ( G gsum ( w |` y ) ) )
101 78 95 98 99 100 cnmpt11
 |-  ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> ( w e. ( B ^m ( y u. { z } ) ) |-> ( G gsum ( w |` y ) ) ) e. ( ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) Cn J ) )
102 64 feqmptd
 |-  ( ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) /\ w e. ( B ^m ( y u. { z } ) ) ) -> w = ( k e. ( y u. { z } ) |-> ( w ` k ) ) )
103 102 reseq1d
 |-  ( ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) /\ w e. ( B ^m ( y u. { z } ) ) ) -> ( w |` { z } ) = ( ( k e. ( y u. { z } ) |-> ( w ` k ) ) |` { z } ) )
104 ssun2
 |-  { z } C_ ( y u. { z } )
105 resmpt
 |-  ( { z } C_ ( y u. { z } ) -> ( ( k e. ( y u. { z } ) |-> ( w ` k ) ) |` { z } ) = ( k e. { z } |-> ( w ` k ) ) )
106 104 105 ax-mp
 |-  ( ( k e. ( y u. { z } ) |-> ( w ` k ) ) |` { z } ) = ( k e. { z } |-> ( w ` k ) )
107 103 106 eqtrdi
 |-  ( ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) /\ w e. ( B ^m ( y u. { z } ) ) ) -> ( w |` { z } ) = ( k e. { z } |-> ( w ` k ) ) )
108 107 oveq2d
 |-  ( ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) /\ w e. ( B ^m ( y u. { z } ) ) ) -> ( G gsum ( w |` { z } ) ) = ( G gsum ( k e. { z } |-> ( w ` k ) ) ) )
109 cmnmnd
 |-  ( G e. CMnd -> G e. Mnd )
110 57 109 syl
 |-  ( ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) /\ w e. ( B ^m ( y u. { z } ) ) ) -> G e. Mnd )
111 vex
 |-  z e. _V
112 111 a1i
 |-  ( ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) /\ w e. ( B ^m ( y u. { z } ) ) ) -> z e. _V )
113 vsnid
 |-  z e. { z }
114 elun2
 |-  ( z e. { z } -> z e. ( y u. { z } ) )
115 113 114 mp1i
 |-  ( ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) /\ w e. ( B ^m ( y u. { z } ) ) ) -> z e. ( y u. { z } ) )
116 64 115 ffvelrnd
 |-  ( ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) /\ w e. ( B ^m ( y u. { z } ) ) ) -> ( w ` z ) e. B )
117 fveq2
 |-  ( k = z -> ( w ` k ) = ( w ` z ) )
118 2 117 gsumsn
 |-  ( ( G e. Mnd /\ z e. _V /\ ( w ` z ) e. B ) -> ( G gsum ( k e. { z } |-> ( w ` k ) ) ) = ( w ` z ) )
119 110 112 116 118 syl3anc
 |-  ( ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) /\ w e. ( B ^m ( y u. { z } ) ) ) -> ( G gsum ( k e. { z } |-> ( w ` k ) ) ) = ( w ` z ) )
120 108 119 eqtrd
 |-  ( ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) /\ w e. ( B ^m ( y u. { z } ) ) ) -> ( G gsum ( w |` { z } ) ) = ( w ` z ) )
121 120 mpteq2dva
 |-  ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> ( w e. ( B ^m ( y u. { z } ) ) |-> ( G gsum ( w |` { z } ) ) ) = ( w e. ( B ^m ( y u. { z } ) ) |-> ( w ` z ) ) )
122 80 mpteq1d
 |-  ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> ( w e. ( B ^m ( y u. { z } ) ) |-> ( w ` z ) ) = ( w e. U. ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) |-> ( w ` z ) ) )
123 113 114 mp1i
 |-  ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> z e. ( y u. { z } ) )
124 88 76 ptpjcn
 |-  ( ( ( y u. { z } ) e. Fin /\ ( ( y u. { z } ) X. { J } ) : ( y u. { z } ) --> Top /\ z e. ( y u. { z } ) ) -> ( w e. U. ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) |-> ( w ` z ) ) e. ( ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) Cn ( ( ( y u. { z } ) X. { J } ) ` z ) ) )
125 61 85 123 124 syl3anc
 |-  ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> ( w e. U. ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) |-> ( w ` z ) ) e. ( ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) Cn ( ( ( y u. { z } ) X. { J } ) ` z ) ) )
126 122 125 eqeltrd
 |-  ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> ( w e. ( B ^m ( y u. { z } ) ) |-> ( w ` z ) ) e. ( ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) Cn ( ( ( y u. { z } ) X. { J } ) ` z ) ) )
127 fvconst2g
 |-  ( ( J e. Top /\ z e. ( y u. { z } ) ) -> ( ( ( y u. { z } ) X. { J } ) ` z ) = J )
128 83 123 127 syl2anc
 |-  ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> ( ( ( y u. { z } ) X. { J } ) ` z ) = J )
129 128 oveq2d
 |-  ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> ( ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) Cn ( ( ( y u. { z } ) X. { J } ) ` z ) ) = ( ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) Cn J ) )
130 126 129 eleqtrd
 |-  ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> ( w e. ( B ^m ( y u. { z } ) ) |-> ( w ` z ) ) e. ( ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) Cn J ) )
131 121 130 eqeltrd
 |-  ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> ( w e. ( B ^m ( y u. { z } ) ) |-> ( G gsum ( w |` { z } ) ) ) e. ( ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) Cn J ) )
132 1 56 74 78 101 131 cnmpt1plusg
 |-  ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> ( w e. ( B ^m ( y u. { z } ) ) |-> ( ( G gsum ( w |` y ) ) ( +g ` G ) ( G gsum ( w |` { z } ) ) ) ) e. ( ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) Cn J ) )
133 73 132 eqeltrd
 |-  ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> ( x e. ( B ^m ( y u. { z } ) ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) Cn J ) )
134 133 3expia
 |-  ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) ) -> ( ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) -> ( x e. ( B ^m ( y u. { z } ) ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) Cn J ) ) )
135 134 expcom
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( ( G e. CMnd /\ G e. TopMnd ) -> ( ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) -> ( x e. ( B ^m ( y u. { z } ) ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) Cn J ) ) ) )
136 135 a2d
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( ( ( G e. CMnd /\ G e. TopMnd ) -> ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> ( ( G e. CMnd /\ G e. TopMnd ) -> ( x e. ( B ^m ( y u. { z } ) ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) Cn J ) ) ) )
137 11 18 25 32 53 136 findcard2s
 |-  ( A e. Fin -> ( ( G e. CMnd /\ G e. TopMnd ) -> ( x e. ( B ^m A ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( A X. { J } ) ) Cn J ) ) )
138 137 com12
 |-  ( ( G e. CMnd /\ G e. TopMnd ) -> ( A e. Fin -> ( x e. ( B ^m A ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( A X. { J } ) ) Cn J ) ) )
139 138 3impia
 |-  ( ( G e. CMnd /\ G e. TopMnd /\ A e. Fin ) -> ( x e. ( B ^m A ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( A X. { J } ) ) Cn J ) )
140 42 82 syl
 |-  ( G e. TopMnd -> J e. Top )
141 xkopt
 |-  ( ( J e. Top /\ A e. Fin ) -> ( J ^ko ~P A ) = ( Xt_ ` ( A X. { J } ) ) )
142 140 141 sylan
 |-  ( ( G e. TopMnd /\ A e. Fin ) -> ( J ^ko ~P A ) = ( Xt_ ` ( A X. { J } ) ) )
143 142 3adant1
 |-  ( ( G e. CMnd /\ G e. TopMnd /\ A e. Fin ) -> ( J ^ko ~P A ) = ( Xt_ ` ( A X. { J } ) ) )
144 143 oveq1d
 |-  ( ( G e. CMnd /\ G e. TopMnd /\ A e. Fin ) -> ( ( J ^ko ~P A ) Cn J ) = ( ( Xt_ ` ( A X. { J } ) ) Cn J ) )
145 139 144 eleqtrrd
 |-  ( ( G e. CMnd /\ G e. TopMnd /\ A e. Fin ) -> ( x e. ( B ^m A ) |-> ( G gsum x ) ) e. ( ( J ^ko ~P A ) Cn J ) )