Metamath Proof Explorer

Theorem cnmpt1plusg

Description: Continuity of the group sum; analogue of cnmpt12f which cannot be used directly because +g is not a function. (Contributed by Mario Carneiro, 23-Aug-2015)

Ref Expression
Hypotheses tgpcn.j 
|- J = ( TopOpen ` G )
cnmpt1plusg.p 
|- .+ = ( +g ` G )
cnmpt1plusg.g 
|- ( ph -> G e. TopMnd )
cnmpt1plusg.k 
|- ( ph -> K e. ( TopOn ` X ) )
cnmpt1plusg.a 
|- ( ph -> ( x e. X |-> A ) e. ( K Cn J ) )
cnmpt1plusg.b 
|- ( ph -> ( x e. X |-> B ) e. ( K Cn J ) )
Assertion cnmpt1plusg 
|- ( ph -> ( x e. X |-> ( A .+ B ) ) e. ( K Cn J ) )

Proof

Step Hyp Ref Expression
1 tgpcn.j 
 |-  J = ( TopOpen ` G )
2 cnmpt1plusg.p 
 |-  .+ = ( +g ` G )
3 cnmpt1plusg.g 
 |-  ( ph -> G e. TopMnd )
4 cnmpt1plusg.k 
 |-  ( ph -> K e. ( TopOn ` X ) )
5 cnmpt1plusg.a 
 |-  ( ph -> ( x e. X |-> A ) e. ( K Cn J ) )
6 cnmpt1plusg.b 
 |-  ( ph -> ( x e. X |-> B ) e. ( K Cn J ) )
7 eqid 
 |-  ( Base ` G ) = ( Base ` G )
8 1 7 tmdtopon 
 |-  ( G e. TopMnd -> J e. ( TopOn ` ( Base ` G ) ) )
9 3 8 syl 
 |-  ( ph -> J e. ( TopOn ` ( Base ` G ) ) )
10 cnf2 
 |-  ( ( K e. ( TopOn ` X ) /\ J e. ( TopOn ` ( Base ` G ) ) /\ ( x e. X |-> A ) e. ( K Cn J ) ) -> ( x e. X |-> A ) : X --> ( Base ` G ) )
11 4 9 5 10 syl3anc 
 |-  ( ph -> ( x e. X |-> A ) : X --> ( Base ` G ) )
12 11 fvmptelcdm 
 |-  ( ( ph /\ x e. X ) -> A e. ( Base ` G ) )
13 cnf2 
 |-  ( ( K e. ( TopOn ` X ) /\ J e. ( TopOn ` ( Base ` G ) ) /\ ( x e. X |-> B ) e. ( K Cn J ) ) -> ( x e. X |-> B ) : X --> ( Base ` G ) )
14 4 9 6 13 syl3anc 
 |-  ( ph -> ( x e. X |-> B ) : X --> ( Base ` G ) )
15 14 fvmptelcdm 
 |-  ( ( ph /\ x e. X ) -> B e. ( Base ` G ) )
16 eqid 
 |-  ( +f ` G ) = ( +f ` G )
17 7 2 16 plusfval 
 |-  ( ( A e. ( Base ` G ) /\ B e. ( Base ` G ) ) -> ( A ( +f ` G ) B ) = ( A .+ B ) )
18 12 15 17 syl2anc 
 |-  ( ( ph /\ x e. X ) -> ( A ( +f ` G ) B ) = ( A .+ B ) )
19 18 mpteq2dva 
 |-  ( ph -> ( x e. X |-> ( A ( +f ` G ) B ) ) = ( x e. X |-> ( A .+ B ) ) )
20 1 16 tmdcn 
 |-  ( G e. TopMnd -> ( +f ` G ) e. ( ( J tX J ) Cn J ) )
21 3 20 syl 
 |-  ( ph -> ( +f ` G ) e. ( ( J tX J ) Cn J ) )
22 4 5 6 21 cnmpt12f 
 |-  ( ph -> ( x e. X |-> ( A ( +f ` G ) B ) ) e. ( K Cn J ) )
23 19 22 eqeltrrd 
 |-  ( ph -> ( x e. X |-> ( A .+ B ) ) e. ( K Cn J ) )