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 CMnd G TopMnd A Fin x B A G x J ^ ko 𝒫 A Cn J

Proof

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