submtmd

Description: A submonoid of a topological monoid is a topological monoid. (Contributed by Mario Carneiro, 6-Oct-2015)

		Ref	Expression
	Hypothesis	subgtgp.h	$⊢ H = G ↾_{𝑠} S$
	Assertion	submtmd	$⊢ (G \in TopMnd \land S \in SubMnd (G)) \to H \in TopMnd$

Proof

Step	Hyp	Ref	Expression
1		subgtgp.h	$⊢ H = G ↾_{𝑠} S$
2	1	submmnd	$⊢ S \in SubMnd (G) \to H \in Mnd$
3	2	adantl	$⊢ (G \in TopMnd \land S \in SubMnd (G)) \to H \in Mnd$
4		tmdtps	$⊢ G \in TopMnd \to G \in TopSp$
5		resstps	$⊢ (G \in TopSp \land S \in SubMnd (G)) \to G ↾_{𝑠} S \in TopSp$
6	4 5	sylan	$⊢ (G \in TopMnd \land S \in SubMnd (G)) \to G ↾_{𝑠} S \in TopSp$
7	1 6	eqeltrid	$⊢ (G \in TopMnd \land S \in SubMnd (G)) \to H \in TopSp$
8		eqid	$⊢ {Base}_{H} = {Base}_{H}$
9		eqid	$⊢ +_{H} = +_{H}$
10		eqid	$⊢ +_{𝑓} (H) = +_{𝑓} (H)$
11	8 9 10	plusffval	$⊢ +_{𝑓} (H) = (x \in {Base}_{H}, y \in {Base}_{H} ⟼ x +_{H} y)$
12	1	submbas	$⊢ S \in SubMnd (G) \to S = {Base}_{H}$
13	12	adantl	$⊢ (G \in TopMnd \land S \in SubMnd (G)) \to S = {Base}_{H}$
14		eqid	$⊢ +_{G} = +_{G}$
15	1 14	ressplusg	$⊢ S \in SubMnd (G) \to +_{G} = +_{H}$
16	15	adantl	$⊢ (G \in TopMnd \land S \in SubMnd (G)) \to +_{G} = +_{H}$
17	16	oveqd	$⊢ (G \in TopMnd \land S \in SubMnd (G)) \to x +_{G} y = x +_{H} y$
18	13 13 17	mpoeq123dv	$⊢ (G \in TopMnd \land S \in SubMnd (G)) \to (x \in S, y \in S ⟼ x +_{G} y) = (x \in {Base}_{H}, y \in {Base}_{H} ⟼ x +_{H} y)$
19	11 18	eqtr4id	$⊢ (G \in TopMnd \land S \in SubMnd (G)) \to +_{𝑓} (H) = (x \in S, y \in S ⟼ x +_{G} y)$
20		eqid	$⊢ TopOpen (G) ↾_{𝑡} S = TopOpen (G) ↾_{𝑡} S$
21		eqid	$⊢ TopOpen (G) = TopOpen (G)$
22		eqid	$⊢ {Base}_{G} = {Base}_{G}$
23	21 22	tmdtopon	$⊢ G \in TopMnd \to TopOpen (G) \in TopOn ({Base}_{G})$
24	23	adantr	$⊢ (G \in TopMnd \land S \in SubMnd (G)) \to TopOpen (G) \in TopOn ({Base}_{G})$
25	22	submss	$⊢ S \in SubMnd (G) \to S \subseteq {Base}_{G}$
26	25	adantl	$⊢ (G \in TopMnd \land S \in SubMnd (G)) \to S \subseteq {Base}_{G}$
27		eqid	$⊢ +_{𝑓} (G) = +_{𝑓} (G)$
28	22 14 27	plusffval	$⊢ +_{𝑓} (G) = (x \in {Base}_{G}, y \in {Base}_{G} ⟼ x +_{G} y)$
29	21 27	tmdcn	$⊢ G \in TopMnd \to +_{𝑓} (G) \in ((TopOpen (G) \times_{t} TopOpen (G)) Cn TopOpen (G))$
30	28 29	eqeltrrid	$⊢ G \in TopMnd \to (x \in {Base}_{G}, y \in {Base}_{G} ⟼ x +_{G} y) \in ((TopOpen (G) \times_{t} TopOpen (G)) Cn TopOpen (G))$
31	30	adantr	$⊢ (G \in TopMnd \land S \in SubMnd (G)) \to (x \in {Base}_{G}, y \in {Base}_{G} ⟼ x +_{G} y) \in ((TopOpen (G) \times_{t} TopOpen (G)) Cn TopOpen (G))$
32	20 24 26 20 24 26 31	cnmpt2res	$⊢ (G \in TopMnd \land S \in SubMnd (G)) \to (x \in S, y \in S ⟼ x +_{G} y) \in (((TopOpen (G) ↾_{𝑡} S) \times_{t} (TopOpen (G) ↾_{𝑡} S)) Cn TopOpen (G))$
33	19 32	eqeltrd	$⊢ (G \in TopMnd \land S \in SubMnd (G)) \to +_{𝑓} (H) \in (((TopOpen (G) ↾_{𝑡} S) \times_{t} (TopOpen (G) ↾_{𝑡} S)) Cn TopOpen (G))$
34	8 10	mndplusf	$⊢ H \in Mnd \to +_{𝑓} (H) : {Base}_{H} \times {Base}_{H} ⟶ {Base}_{H}$
35		frn	$⊢ +_{𝑓} (H) : {Base}_{H} \times {Base}_{H} ⟶ {Base}_{H} \to ran +_{𝑓} (H) \subseteq {Base}_{H}$
36	3 34 35	3syl	$⊢ (G \in TopMnd \land S \in SubMnd (G)) \to ran +_{𝑓} (H) \subseteq {Base}_{H}$
37	36 13	sseqtrrd	$⊢ (G \in TopMnd \land S \in SubMnd (G)) \to ran +_{𝑓} (H) \subseteq S$
38		cnrest2	$⊢ (TopOpen (G) \in TopOn ({Base}_{G}) \land ran +_{𝑓} (H) \subseteq S \land S \subseteq {Base}_{G}) \to (+_{𝑓} (H) \in (((TopOpen (G) ↾_{𝑡} S) \times_{t} (TopOpen (G) ↾_{𝑡} S)) Cn TopOpen (G)) \leftrightarrow +_{𝑓} (H) \in (((TopOpen (G) ↾_{𝑡} S) \times_{t} (TopOpen (G) ↾_{𝑡} S)) Cn (TopOpen (G) ↾_{𝑡} S)))$
39	24 37 26 38	syl3anc	$⊢ (G \in TopMnd \land S \in SubMnd (G)) \to (+_{𝑓} (H) \in (((TopOpen (G) ↾_{𝑡} S) \times_{t} (TopOpen (G) ↾_{𝑡} S)) Cn TopOpen (G)) \leftrightarrow +_{𝑓} (H) \in (((TopOpen (G) ↾_{𝑡} S) \times_{t} (TopOpen (G) ↾_{𝑡} S)) Cn (TopOpen (G) ↾_{𝑡} S)))$
40	33 39	mpbid	$⊢ (G \in TopMnd \land S \in SubMnd (G)) \to +_{𝑓} (H) \in (((TopOpen (G) ↾_{𝑡} S) \times_{t} (TopOpen (G) ↾_{𝑡} S)) Cn (TopOpen (G) ↾_{𝑡} S))$
41	1 21	resstopn	$⊢ TopOpen (G) ↾_{𝑡} S = TopOpen (H)$
42	10 41	istmd	$⊢ H \in TopMnd \leftrightarrow (H \in Mnd \land H \in TopSp \land +_{𝑓} (H) \in (((TopOpen (G) ↾_{𝑡} S) \times_{t} (TopOpen (G) ↾_{𝑡} S)) Cn (TopOpen (G) ↾_{𝑡} S)))$
43	3 7 40 42	syl3anbrc	$⊢ (G \in TopMnd \land S \in SubMnd (G)) \to H \in TopMnd$

Metamath Proof Explorer

Theorem submtmd

Proof