This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 eqtrid 
 |-  ( ( ( 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 ffvelcdmd 
 |-  ( ( ( ( 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 ) )