Theorem indistgp 24226

Description: Any group equipped with the indiscrete topology is a topological group. (Contributed by Mario Carneiro, 14-Aug-2015.)

Hypotheses

Ref	Expression
distgp.1	⊢ 𝐵 = (Base‘𝐺)
distgp.2	⊢ 𝐽 = (TopOpen‘𝐺)

Assertion

Ref	Expression
indistgp	⊢ ((𝐺 ∈ Grp ∧ 𝐽 = {∅, 𝐵}) → 𝐺 ∈ TopGrp)

Proof of Theorem indistgp

Step	Hyp	Ref	Expression
1		simpl 487	. 2 ⊢ ((𝐺 ∈ Grp ∧ 𝐽 = {∅, 𝐵}) → 𝐺 ∈ Grp)
2		simpr 489	. . . 4 ⊢ ((𝐺 ∈ Grp ∧ 𝐽 = {∅, 𝐵}) → 𝐽 = {∅, 𝐵})
3		distgp.1	. . . . . 6 ⊢ 𝐵 = (Base‘𝐺)
4	3	fvexi 6896	. . . . 5 ⊢ 𝐵 ∈ V
5		indistopon 23127	. . . . 5 ⊢ (𝐵 ∈ V → {∅, 𝐵} ∈ (TopOn‘𝐵))
6	4, 5	ax-mp 5	. . . 4 ⊢ {∅, 𝐵} ∈ (TopOn‘𝐵)
7	2, 6	eqeltrdi 2877	. . 3 ⊢ ((𝐺 ∈ Grp ∧ 𝐽 = {∅, 𝐵}) → 𝐽 ∈ (TopOn‘𝐵))
8		distgp.2	. . . 4 ⊢ 𝐽 = (TopOpen‘𝐺)
9	3, 8	istps 23060	. . 3 ⊢ (𝐺 ∈ TopSp ↔ 𝐽 ∈ (TopOn‘𝐵))
10	7, 9	sylibr 237	. 2 ⊢ ((𝐺 ∈ Grp ∧ 𝐽 = {∅, 𝐵}) → 𝐺 ∈ TopSp)
11		eqid 2769	. . . . . 6 ⊢ (-g‘𝐺) = (-g‘𝐺)
12	3, 11	grpsubf 19085	. . . . 5 ⊢ (𝐺 ∈ Grp → (-g‘𝐺):(𝐵 × 𝐵)⟶𝐵)
13	12	adantr 485	. . . 4 ⊢ ((𝐺 ∈ Grp ∧ 𝐽 = {∅, 𝐵}) → (-g‘𝐺):(𝐵 × 𝐵)⟶𝐵)
14	4, 4	xpex 7752	. . . . 5 ⊢ (𝐵 × 𝐵) ∈ V
15	4, 14	elmap 8869	. . . 4 ⊢ ((-g‘𝐺) ∈ (𝐵 ↑m (𝐵 × 𝐵)) ↔ (-g‘𝐺):(𝐵 × 𝐵)⟶𝐵)
16	13, 15	sylibr 237	. . 3 ⊢ ((𝐺 ∈ Grp ∧ 𝐽 = {∅, 𝐵}) → (-g‘𝐺) ∈ (𝐵 ↑m (𝐵 × 𝐵)))
17	2	oveq2d 7427	. . . 4 ⊢ ((𝐺 ∈ Grp ∧ 𝐽 = {∅, 𝐵}) → ((𝐽 ×t 𝐽) Cn 𝐽) = ((𝐽 ×t 𝐽) Cn {∅, 𝐵}))
18		txtopon 23717	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝐵) ∧ 𝐽 ∈ (TopOn‘𝐵)) → (𝐽 ×t 𝐽) ∈ (TopOn‘(𝐵 × 𝐵)))
19	7, 7, 18	syl2anc 595	. . . . 5 ⊢ ((𝐺 ∈ Grp ∧ 𝐽 = {∅, 𝐵}) → (𝐽 ×t 𝐽) ∈ (TopOn‘(𝐵 × 𝐵)))
20		cnindis 23418	. . . . 5 ⊢ (((𝐽 ×t 𝐽) ∈ (TopOn‘(𝐵 × 𝐵)) ∧ 𝐵 ∈ V) → ((𝐽 ×t 𝐽) Cn {∅, 𝐵}) = (𝐵 ↑m (𝐵 × 𝐵)))
21	19, 4, 20	sylancl 597	. . . 4 ⊢ ((𝐺 ∈ Grp ∧ 𝐽 = {∅, 𝐵}) → ((𝐽 ×t 𝐽) Cn {∅, 𝐵}) = (𝐵 ↑m (𝐵 × 𝐵)))
22	17, 21	eqtrd 2804	. . 3 ⊢ ((𝐺 ∈ Grp ∧ 𝐽 = {∅, 𝐵}) → ((𝐽 ×t 𝐽) Cn 𝐽) = (𝐵 ↑m (𝐵 × 𝐵)))
23	16, 22	eleqtrrd 2872	. 2 ⊢ ((𝐺 ∈ Grp ∧ 𝐽 = {∅, 𝐵}) → (-g‘𝐺) ∈ ((𝐽 ×t 𝐽) Cn 𝐽))
24	8, 11	istgp2 24217	. 2 ⊢ (𝐺 ∈ TopGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ TopSp ∧ (-g‘𝐺) ∈ ((𝐽 ×t 𝐽) Cn 𝐽)))
25	1, 10, 23, 24	syl3anbrc 1360	1 ⊢ ((𝐺 ∈ Grp ∧ 𝐽 = {∅, 𝐵}) → 𝐺 ∈ TopGrp)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567   ∈ wcel 2149  Vcvv 3461  ∅c0 4292  {cpr 4594   × cxp 5660  ⟶wf 6533  ‘cfv 6537  (class class class)co 7411   ↑_m cmap 8824  Basecbs 17269  TopOpenctopn 17474  Grpcgrp 19000  -_gcsg 19002  TopOnctopon 23036  TopSpctps 23058   Cn ccn 23350   ×_t ctx 23686  TopGrpctgp 24197

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5259  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rmo 3375  df-reu 3376  df-rab 3423  df-v 3463  df-sbc 3752  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4491  df-pw 4567  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7368  df-ov 7414  df-oprab 7415  df-mpo 7416  df-1st 7986  df-2nd 7987  df-map 8826  df-0g 17494  df-topgen 17496  df-plusf 18697  df-mgm 18698  df-sgrp 18777  df-mnd 18793  df-grp 19003  df-minusg 19004  df-sbg 19005  df-top 23020  df-topon 23037  df-topsp 23059  df-bases 23072  df-cn 23353  df-cnp 23354  df-tx 23688  df-tmd 24198  df-tgp 24199

This theorem is referenced by: (None)