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
Assertion tgpsubcn ⊢ G ∈ TopGrp → - ˙ ∈ J × t J Cn J

Proof

Step Hyp Ref Expression
1 tgpsubcn.2 ⊢ J = TopOpen ⁡ G
2 tgpsubcn.3 ⊢ - ˙ = - G
3 eqid ⊢ Base G = Base G
4 eqid ⊢ + G = + G
5 eqid ⊢ inv g ⁡ G = inv g ⁡ G
6 3 4 5 2 grpsubfval ⊢ - ˙ = x ∈ Base G , y ∈ Base G ⟼ x + G inv g ⁡ G ⁡ y
7 tgptmd ⊢ G ∈ TopGrp → G ∈ TopMnd
8 1 3 tgptopon ⊢ G ∈ TopGrp → J ∈ TopOn ⁡ Base G
9 8 8 cnmpt1st ⊢ G ∈ TopGrp → x ∈ Base G , y ∈ Base G ⟼ x ∈ J × t J Cn J
10 8 8 cnmpt2nd ⊢ G ∈ TopGrp → x ∈ Base G , y ∈ Base G ⟼ y ∈ J × t J Cn J
11 1 5 tgpinv ⊢ G ∈ TopGrp → inv g ⁡ G ∈ J Cn J
12 8 8 10 11 cnmpt21f ⊢ G ∈ TopGrp → x ∈ Base G , y ∈ Base G ⟼ inv g ⁡ G ⁡ y ∈ J × t J Cn J
13 1 4 7 8 8 9 12 cnmpt2plusg ⊢ G ∈ TopGrp → x ∈ Base G , y ∈ Base G ⟼ x + G inv g ⁡ G ⁡ y ∈ J × t J Cn J
14 6 13 eqeltrid ⊢ G ∈ TopGrp → - ˙ ∈ J × t J Cn J