cntzspan

Description: If the generators commute, the generated monoid is commutative. (Contributed by Mario Carneiro, 25-Apr-2016)

	Ref	Expression
Hypotheses	cntzspan.z	$⊢ Z = Cntz (G)$
	cntzspan.k	$⊢ K = mrCls (SubMnd (G))$
	cntzspan.h	$⊢ H = G ↾_{𝑠} K (S)$
Assertion	cntzspan	$⊢ (G \in Mnd \land S \subseteq Z (S)) \to H \in CMnd$

Proof

Step	Hyp	Ref	Expression
1		cntzspan.z	$⊢ Z = Cntz (G)$
2		cntzspan.k	$⊢ K = mrCls (SubMnd (G))$
3		cntzspan.h	$⊢ H = G ↾_{𝑠} K (S)$
4		eqid	$⊢ {Base}_{G} = {Base}_{G}$
5	4	submacs	$⊢ G \in Mnd \to SubMnd (G) \in ACS ({Base}_{G})$
6	5	adantr	$⊢ (G \in Mnd \land S \subseteq Z (S)) \to SubMnd (G) \in ACS ({Base}_{G})$
7	6	acsmred	$⊢ (G \in Mnd \land S \subseteq Z (S)) \to SubMnd (G) \in Moore ({Base}_{G})$
8		simpr	$⊢ (G \in Mnd \land S \subseteq Z (S)) \to S \subseteq Z (S)$
9	4 1	cntzssv	$⊢ Z (S) \subseteq {Base}_{G}$
10	8 9	sstrdi	$⊢ (G \in Mnd \land S \subseteq Z (S)) \to S \subseteq {Base}_{G}$
11	4 1	cntzsubm	$⊢ (G \in Mnd \land S \subseteq {Base}_{G}) \to Z (S) \in SubMnd (G)$
12	10 11	syldan	$⊢ (G \in Mnd \land S \subseteq Z (S)) \to Z (S) \in SubMnd (G)$
13	2	mrcsscl	$⊢ (SubMnd (G) \in Moore ({Base}_{G}) \land S \subseteq Z (S) \land Z (S) \in SubMnd (G)) \to K (S) \subseteq Z (S)$
14	7 8 12 13	syl3anc	$⊢ (G \in Mnd \land S \subseteq Z (S)) \to K (S) \subseteq Z (S)$
15	7 2	mrcssvd	$⊢ (G \in Mnd \land S \subseteq Z (S)) \to K (S) \subseteq {Base}_{G}$
16	4 1	cntzrec	$⊢ (K (S) \subseteq {Base}_{G} \land S \subseteq {Base}_{G}) \to (K (S) \subseteq Z (S) \leftrightarrow S \subseteq Z (K (S)))$
17	15 10 16	syl2anc	$⊢ (G \in Mnd \land S \subseteq Z (S)) \to (K (S) \subseteq Z (S) \leftrightarrow S \subseteq Z (K (S)))$
18	14 17	mpbid	$⊢ (G \in Mnd \land S \subseteq Z (S)) \to S \subseteq Z (K (S))$
19	4 1	cntzsubm	$⊢ (G \in Mnd \land K (S) \subseteq {Base}_{G}) \to Z (K (S)) \in SubMnd (G)$
20	15 19	syldan	$⊢ (G \in Mnd \land S \subseteq Z (S)) \to Z (K (S)) \in SubMnd (G)$
21	2	mrcsscl	$⊢ (SubMnd (G) \in Moore ({Base}_{G}) \land S \subseteq Z (K (S)) \land Z (K (S)) \in SubMnd (G)) \to K (S) \subseteq Z (K (S))$
22	7 18 20 21	syl3anc	$⊢ (G \in Mnd \land S \subseteq Z (S)) \to K (S) \subseteq Z (K (S))$
23	2	mrccl	$⊢ (SubMnd (G) \in Moore ({Base}_{G}) \land S \subseteq {Base}_{G}) \to K (S) \in SubMnd (G)$
24	7 10 23	syl2anc	$⊢ (G \in Mnd \land S \subseteq Z (S)) \to K (S) \in SubMnd (G)$
25	3 1	submcmn2	$⊢ K (S) \in SubMnd (G) \to (H \in CMnd \leftrightarrow K (S) \subseteq Z (K (S)))$
26	24 25	syl	$⊢ (G \in Mnd \land S \subseteq Z (S)) \to (H \in CMnd \leftrightarrow K (S) \subseteq Z (K (S)))$
27	22 26	mpbird	$⊢ (G \in Mnd \land S \subseteq Z (S)) \to H \in CMnd$

Metamath Proof Explorer

Theorem cntzspan

Proof