Metamath Proof Explorer

Theorem tgpsubcn

Description: In a topological group, the "subtraction" (or "division") is continuous. Axiom GT' of BourbakiTop1 p. III.1. (Contributed by FL, 21-Jun-2010) (Revised by Mario Carneiro, 19-Mar-2015)

Ref Expression
Hypotheses tgpsubcn.2 
|- J = ( TopOpen ` G )
tgpsubcn.3 
|- .- = ( -g ` G )
Assertion tgpsubcn 
|- ( G e. TopGrp -> .- e. ( ( J tX J ) Cn J ) )

Proof

Step Hyp Ref Expression
1 tgpsubcn.2 
 |-  J = ( TopOpen ` G )
2 tgpsubcn.3 
 |-  .- = ( -g ` G )
3 eqid 
 |-  ( Base ` G ) = ( Base ` G )
4 eqid 
 |-  ( +g ` G ) = ( +g ` G )
5 eqid 
 |-  ( invg ` G ) = ( invg ` G )
6 3 4 5 2 grpsubfval 
 |-  .- = ( x e. ( Base ` G ) , y e. ( Base ` G ) |-> ( x ( +g ` G ) ( ( invg ` G ) ` y ) ) )
7 tgptmd 
 |-  ( G e. TopGrp -> G e. TopMnd )
8 1 3 tgptopon 
 |-  ( G e. TopGrp -> J e. ( TopOn ` ( Base ` G ) ) )
9 8 8 cnmpt1st 
 |-  ( G e. TopGrp -> ( x e. ( Base ` G ) , y e. ( Base ` G ) |-> x ) e. ( ( J tX J ) Cn J ) )
10 8 8 cnmpt2nd 
 |-  ( G e. TopGrp -> ( x e. ( Base ` G ) , y e. ( Base ` G ) |-> y ) e. ( ( J tX J ) Cn J ) )
11 1 5 tgpinv 
 |-  ( G e. TopGrp -> ( invg ` G ) e. ( J Cn J ) )
12 8 8 10 11 cnmpt21f 
 |-  ( G e. TopGrp -> ( x e. ( Base ` G ) , y e. ( Base ` G ) |-> ( ( invg ` G ) ` y ) ) e. ( ( J tX J ) Cn J ) )
13 1 4 7 8 8 9 12 cnmpt2plusg 
 |-  ( G e. TopGrp -> ( x e. ( Base ` G ) , y e. ( Base ` G ) |-> ( x ( +g ` G ) ( ( invg ` G ) ` y ) ) ) e. ( ( J tX J ) Cn J ) )
14 6 13 eqeltrid 
 |-  ( G e. TopGrp -> .- e. ( ( J tX J ) Cn J ) )