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 𝐽 = ( TopOpen ‘ 𝐺 )
tgpsubcn.3 = ( -g𝐺 )
Assertion tgpsubcn ( 𝐺 ∈ TopGrp → ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )

Proof

Step Hyp Ref Expression
1 tgpsubcn.2 𝐽 = ( TopOpen ‘ 𝐺 )
2 tgpsubcn.3 = ( -g𝐺 )
3 eqid ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
4 eqid ( +g𝐺 ) = ( +g𝐺 )
5 eqid ( invg𝐺 ) = ( invg𝐺 )
6 3 4 5 2 grpsubfval = ( 𝑥 ∈ ( Base ‘ 𝐺 ) , 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( 𝑥 ( +g𝐺 ) ( ( invg𝐺 ) ‘ 𝑦 ) ) )
7 tgptmd ( 𝐺 ∈ TopGrp → 𝐺 ∈ TopMnd )
8 1 3 tgptopon ( 𝐺 ∈ TopGrp → 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) )
9 8 8 cnmpt1st ( 𝐺 ∈ TopGrp → ( 𝑥 ∈ ( Base ‘ 𝐺 ) , 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ 𝑥 ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
10 8 8 cnmpt2nd ( 𝐺 ∈ TopGrp → ( 𝑥 ∈ ( Base ‘ 𝐺 ) , 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ 𝑦 ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
11 1 5 tgpinv ( 𝐺 ∈ TopGrp → ( invg𝐺 ) ∈ ( 𝐽 Cn 𝐽 ) )
12 8 8 10 11 cnmpt21f ( 𝐺 ∈ TopGrp → ( 𝑥 ∈ ( Base ‘ 𝐺 ) , 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( ( invg𝐺 ) ‘ 𝑦 ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
13 1 4 7 8 8 9 12 cnmpt2plusg ( 𝐺 ∈ TopGrp → ( 𝑥 ∈ ( Base ‘ 𝐺 ) , 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( 𝑥 ( +g𝐺 ) ( ( invg𝐺 ) ‘ 𝑦 ) ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
14 6 13 eqeltrid ( 𝐺 ∈ TopGrp → ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )