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

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 = ( ~P A i^i Fin )
tsmsval.l 
|- L = ran ( z e. S |-> { y e. S | z C_ y } )
tsmsval.g 
|- ( ph -> G e. V )
tsmsval2.f 
|- ( ph -> F e. W )
tsmsval2.a 
|- ( ph -> dom F = A )
Assertion tsmsval2 
|- ( ph -> ( G tsums F ) = ( ( J fLimf ( S filGen L ) ) ` ( y e. S |-> ( G gsum ( F |` y ) ) ) ) )

Proof

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