Metamath Proof Explorer


Theorem tsmsval2

Description: Definition of the topological group sum(s) of a collection F ( x ) of values in the group with index set A . (Contributed by Mario Carneiro, 2-Sep-2015)

Ref Expression
Hypotheses tsmsval.b B = Base G
tsmsval.j J = TopOpen G
tsmsval.s S = 𝒫 A Fin
tsmsval.l L = ran z S y S | z y
tsmsval.g φ G V
tsmsval2.f φ F W
tsmsval2.a φ dom F = A
Assertion tsmsval2 φ G tsums F = J fLimf S filGen L y S G F y

Proof

Step Hyp Ref Expression
1 tsmsval.b B = Base G
2 tsmsval.j J = TopOpen G
3 tsmsval.s S = 𝒫 A Fin
4 tsmsval.l L = ran z S y S | z y
5 tsmsval.g φ G V
6 tsmsval2.f φ F W
7 tsmsval2.a φ dom F = A
8 df-tsms tsums = w V , f V 𝒫 dom f Fin / s TopOpen w fLimf s filGen ran z s y s | z y y s w f y
9 8 a1i φ tsums = w V , f V 𝒫 dom f Fin / s TopOpen w fLimf s filGen ran z s y s | z y y s w f y
10 vex f V
11 10 dmex dom f V
12 11 pwex 𝒫 dom f V
13 12 inex1 𝒫 dom f Fin V
14 13 a1i φ w = G f = F 𝒫 dom f Fin V
15 simplrl φ w = G f = F s = 𝒫 dom f Fin w = G
16 15 fveq2d φ w = G f = F s = 𝒫 dom f Fin TopOpen w = TopOpen G
17 16 2 eqtr4di φ w = G f = F s = 𝒫 dom f Fin TopOpen w = J
18 id s = 𝒫 dom f Fin s = 𝒫 dom f Fin
19 simprr φ w = G f = F f = F
20 19 dmeqd φ w = G f = F dom f = dom F
21 7 adantr φ w = G f = F dom F = A
22 20 21 eqtrd φ w = G f = F dom f = A
23 22 pweqd φ w = G f = F 𝒫 dom f = 𝒫 A
24 23 ineq1d φ w = G f = F 𝒫 dom f Fin = 𝒫 A Fin
25 24 3 eqtr4di φ w = G f = F 𝒫 dom f Fin = S
26 18 25 sylan9eqr φ w = G f = F s = 𝒫 dom f Fin s = S
27 26 rabeqdv φ w = G f = F s = 𝒫 dom f Fin y s | z y = y S | z y
28 26 27 mpteq12dv φ w = G f = F s = 𝒫 dom f Fin z s y s | z y = z S y S | z y
29 28 rneqd φ w = G f = F s = 𝒫 dom f Fin ran z s y s | z y = ran z S y S | z y
30 29 4 eqtr4di φ w = G f = F s = 𝒫 dom f Fin ran z s y s | z y = L
31 26 30 oveq12d φ w = G f = F s = 𝒫 dom f Fin s filGen ran z s y s | z y = S filGen L
32 17 31 oveq12d φ w = G f = F s = 𝒫 dom f Fin TopOpen w fLimf s filGen ran z s y s | z y = J fLimf S filGen L
33 simplrr φ w = G f = F s = 𝒫 dom f Fin f = F
34 33 reseq1d φ w = G f = F s = 𝒫 dom f Fin f y = F y
35 15 34 oveq12d φ w = G f = F s = 𝒫 dom f Fin w f y = G F y
36 26 35 mpteq12dv φ w = G f = F s = 𝒫 dom f Fin y s w f y = y S G F y
37 32 36 fveq12d φ w = G f = F s = 𝒫 dom f Fin TopOpen w fLimf s filGen ran z s y s | z y y s w f y = J fLimf S filGen L y S G F y
38 14 37 csbied φ w = G f = F 𝒫 dom f Fin / s TopOpen w fLimf s filGen ran z s y s | z y y s w f y = J fLimf S filGen L y S G F y
39 5 elexd φ G V
40 6 elexd φ F V
41 fvexd φ J fLimf S filGen L y S G F y V
42 9 38 39 40 41 ovmpod φ G tsums F = J fLimf S filGen L y S G F y