Metamath Proof Explorer

Theorem cnmpt2plusg

Description: Continuity of the group sum; analogue of cnmpt22f 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 ) )
cnmpt2plusg.l 
|- ( ph -> L e. ( TopOn ` Y ) )
cnmpt2plusg.a 
|- ( ph -> ( x e. X , y e. Y |-> A ) e. ( ( K tX L ) Cn J ) )
cnmpt2plusg.b 
|- ( ph -> ( x e. X , y e. Y |-> B ) e. ( ( K tX L ) Cn J ) )
Assertion cnmpt2plusg 
|- ( ph -> ( x e. X , y e. Y |-> ( A .+ B ) ) e. ( ( K tX L ) 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 cnmpt2plusg.l 
 |-  ( ph -> L e. ( TopOn ` Y ) )
6 cnmpt2plusg.a 
 |-  ( ph -> ( x e. X , y e. Y |-> A ) e. ( ( K tX L ) Cn J ) )
7 cnmpt2plusg.b 
 |-  ( ph -> ( x e. X , y e. Y |-> B ) e. ( ( K tX L ) Cn J ) )
8 txtopon 
 |-  ( ( K e. ( TopOn ` X ) /\ L e. ( TopOn ` Y ) ) -> ( K tX L ) e. ( TopOn ` ( X X. Y ) ) )
9 4 5 8 syl2anc 
 |-  ( ph -> ( K tX L ) e. ( TopOn ` ( X X. Y ) ) )
10 eqid 
 |-  ( Base ` G ) = ( Base ` G )
11 1 10 tmdtopon 
 |-  ( G e. TopMnd -> J e. ( TopOn ` ( Base ` G ) ) )
12 3 11 syl 
 |-  ( ph -> J e. ( TopOn ` ( Base ` G ) ) )
13 cnf2 
 |-  ( ( ( K tX L ) e. ( TopOn ` ( X X. Y ) ) /\ J e. ( TopOn ` ( Base ` G ) ) /\ ( x e. X , y e. Y |-> A ) e. ( ( K tX L ) Cn J ) ) -> ( x e. X , y e. Y |-> A ) : ( X X. Y ) --> ( Base ` G ) )
14 9 12 6 13 syl3anc 
 |-  ( ph -> ( x e. X , y e. Y |-> A ) : ( X X. Y ) --> ( Base ` G ) )
15 eqid 
 |-  ( x e. X , y e. Y |-> A ) = ( x e. X , y e. Y |-> A )
16 15 fmpo 
 |-  ( A. x e. X A. y e. Y A e. ( Base ` G ) <-> ( x e. X , y e. Y |-> A ) : ( X X. Y ) --> ( Base ` G ) )
17 14 16 sylibr 
 |-  ( ph -> A. x e. X A. y e. Y A e. ( Base ` G ) )
18 17 r19.21bi 
 |-  ( ( ph /\ x e. X ) -> A. y e. Y A e. ( Base ` G ) )
19 18 r19.21bi 
 |-  ( ( ( ph /\ x e. X ) /\ y e. Y ) -> A e. ( Base ` G ) )
20 19 3impa 
 |-  ( ( ph /\ x e. X /\ y e. Y ) -> A e. ( Base ` G ) )
21 cnf2 
 |-  ( ( ( K tX L ) e. ( TopOn ` ( X X. Y ) ) /\ J e. ( TopOn ` ( Base ` G ) ) /\ ( x e. X , y e. Y |-> B ) e. ( ( K tX L ) Cn J ) ) -> ( x e. X , y e. Y |-> B ) : ( X X. Y ) --> ( Base ` G ) )
22 9 12 7 21 syl3anc 
 |-  ( ph -> ( x e. X , y e. Y |-> B ) : ( X X. Y ) --> ( Base ` G ) )
23 eqid 
 |-  ( x e. X , y e. Y |-> B ) = ( x e. X , y e. Y |-> B )
24 23 fmpo 
 |-  ( A. x e. X A. y e. Y B e. ( Base ` G ) <-> ( x e. X , y e. Y |-> B ) : ( X X. Y ) --> ( Base ` G ) )
25 22 24 sylibr 
 |-  ( ph -> A. x e. X A. y e. Y B e. ( Base ` G ) )
26 25 r19.21bi 
 |-  ( ( ph /\ x e. X ) -> A. y e. Y B e. ( Base ` G ) )
27 26 r19.21bi 
 |-  ( ( ( ph /\ x e. X ) /\ y e. Y ) -> B e. ( Base ` G ) )
28 27 3impa 
 |-  ( ( ph /\ x e. X /\ y e. Y ) -> B e. ( Base ` G ) )
29 eqid 
 |-  ( +f ` G ) = ( +f ` G )
30 10 2 29 plusfval 
 |-  ( ( A e. ( Base ` G ) /\ B e. ( Base ` G ) ) -> ( A ( +f ` G ) B ) = ( A .+ B ) )
31 20 28 30 syl2anc 
 |-  ( ( ph /\ x e. X /\ y e. Y ) -> ( A ( +f ` G ) B ) = ( A .+ B ) )
32 31 mpoeq3dva 
 |-  ( ph -> ( x e. X , y e. Y |-> ( A ( +f ` G ) B ) ) = ( x e. X , y e. Y |-> ( A .+ B ) ) )
33 1 29 tmdcn 
 |-  ( G e. TopMnd -> ( +f ` G ) e. ( ( J tX J ) Cn J ) )
34 3 33 syl 
 |-  ( ph -> ( +f ` G ) e. ( ( J tX J ) Cn J ) )
35 4 5 6 7 34 cnmpt22f 
 |-  ( ph -> ( x e. X , y e. Y |-> ( A ( +f ` G ) B ) ) e. ( ( K tX L ) Cn J ) )
36 32 35 eqeltrrd 
 |-  ( ph -> ( x e. X , y e. Y |-> ( A .+ B ) ) e. ( ( K tX L ) Cn J ) )