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 𝐽 ) )