Theorem tmdlactcn 24048

Description: The left group action of element 𝐴 in a topological monoid 𝐺 is a continuous function. (Contributed by FL, 18-Mar-2008.) (Revised by Mario Carneiro, 14-Aug-2015.)

Hypotheses

Ref	Expression
tgplacthmeo.1	⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ (𝐴 + 𝑥))
tgplacthmeo.2	⊢ 𝑋 = (Base‘𝐺)
tgplacthmeo.3	⊢ + = (+g‘𝐺)
tgplacthmeo.4	⊢ 𝐽 = (TopOpen‘𝐺)

Assertion

Ref	Expression
tmdlactcn	⊢ ((𝐺 ∈ TopMnd ∧ 𝐴 ∈ 𝑋) → 𝐹 ∈ (𝐽 Cn 𝐽))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐺   𝑥,𝐽   𝑥, +   𝑥,𝑋

Allowed substitution hint:   𝐹(𝑥)

Proof of Theorem tmdlactcn

Step	Hyp	Ref	Expression
1		tgplacthmeo.1	. 2 ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ (𝐴 + 𝑥))
2		tgplacthmeo.4	. . 3 ⊢ 𝐽 = (TopOpen‘𝐺)
3		tgplacthmeo.3	. . 3 ⊢ + = (+g‘𝐺)
4		simpl 482	. . 3 ⊢ ((𝐺 ∈ TopMnd ∧ 𝐴 ∈ 𝑋) → 𝐺 ∈ TopMnd)
5		tgplacthmeo.2	. . . . 5 ⊢ 𝑋 = (Base‘𝐺)
6	2, 5	tmdtopon 24027	. . . 4 ⊢ (𝐺 ∈ TopMnd → 𝐽 ∈ (TopOn‘𝑋))
7	6	adantr 480	. . 3 ⊢ ((𝐺 ∈ TopMnd ∧ 𝐴 ∈ 𝑋) → 𝐽 ∈ (TopOn‘𝑋))
8		simpr 484	. . . 4 ⊢ ((𝐺 ∈ TopMnd ∧ 𝐴 ∈ 𝑋) → 𝐴 ∈ 𝑋)
9	7, 7, 8	cnmptc 23608	. . 3 ⊢ ((𝐺 ∈ TopMnd ∧ 𝐴 ∈ 𝑋) → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐽 Cn 𝐽))
10	7	cnmptid 23607	. . 3 ⊢ ((𝐺 ∈ TopMnd ∧ 𝐴 ∈ 𝑋) → (𝑥 ∈ 𝑋 ↦ 𝑥) ∈ (𝐽 Cn 𝐽))
11	2, 3, 4, 7, 9, 10	cnmpt1plusg 24033	. 2 ⊢ ((𝐺 ∈ TopMnd ∧ 𝐴 ∈ 𝑋) → (𝑥 ∈ 𝑋 ↦ (𝐴 + 𝑥)) ∈ (𝐽 Cn 𝐽))
12	1, 11	eqeltrid 2840	1 ⊢ ((𝐺 ∈ TopMnd ∧ 𝐴 ∈ 𝑋) → 𝐹 ∈ (𝐽 Cn 𝐽))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113   ↦ cmpt 5179  ‘cfv 6492  (class class class)co 7358  Basecbs 17138  +_gcplusg 17179  TopOpenctopn 17343  TopOnctopon 22856   Cn ccn 23170  TopMndctmd 24016

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7361  df-oprab 7362  df-mpo 7363  df-1st 7933  df-2nd 7934  df-map 8767  df-topgen 17365  df-plusf 18566  df-top 22840  df-topon 22857  df-topsp 22879  df-bases 22892  df-cn 23173  df-cnp 23174  df-tx 23508  df-tmd 24018

This theorem is referenced by:  tgplacthmeo  24049  ghmcnp  24061