Metamath Proof Explorer

Theorem 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 ∈ Mnd ∧ S ⊆ Z ⁡ S → H ∈ 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 ∈ Mnd → SubMnd ⁡ G ∈ ACS ⁡ Base G
6 5 adantr ⊢ G ∈ Mnd ∧ S ⊆ Z ⁡ S → SubMnd ⁡ G ∈ ACS ⁡ Base G
7 6 acsmred ⊢ G ∈ Mnd ∧ S ⊆ Z ⁡ S → SubMnd ⁡ G ∈ Moore ⁡ Base G
8 simpr ⊢ G ∈ Mnd ∧ S ⊆ Z ⁡ S → S ⊆ Z ⁡ S
9 4 1 cntzssv ⊢ Z ⁡ S ⊆ Base G
10 8 9 sstrdi ⊢ G ∈ Mnd ∧ S ⊆ Z ⁡ S → S ⊆ Base G
11 4 1 cntzsubm ⊢ G ∈ Mnd ∧ S ⊆ Base G → Z ⁡ S ∈ SubMnd ⁡ G
12 10 11 syldan ⊢ G ∈ Mnd ∧ S ⊆ Z ⁡ S → Z ⁡ S ∈ SubMnd ⁡ G
13 2 mrcsscl ⊢ SubMnd ⁡ G ∈ Moore ⁡ Base G ∧ S ⊆ Z ⁡ S ∧ Z ⁡ S ∈ SubMnd ⁡ G → K ⁡ S ⊆ Z ⁡ S
14 7 8 12 13 syl3anc ⊢ G ∈ Mnd ∧ S ⊆ Z ⁡ S → K ⁡ S ⊆ Z ⁡ S
15 7 2 mrcssvd ⊢ G ∈ Mnd ∧ S ⊆ Z ⁡ S → K ⁡ S ⊆ Base G
16 4 1 cntzrec ⊢ K ⁡ S ⊆ Base G ∧ S ⊆ Base G → K ⁡ S ⊆ Z ⁡ S ↔ S ⊆ Z ⁡ K ⁡ S
17 15 10 16 syl2anc ⊢ G ∈ Mnd ∧ S ⊆ Z ⁡ S → K ⁡ S ⊆ Z ⁡ S ↔ S ⊆ Z ⁡ K ⁡ S
18 14 17 mpbid ⊢ G ∈ Mnd ∧ S ⊆ Z ⁡ S → S ⊆ Z ⁡ K ⁡ S
19 4 1 cntzsubm ⊢ G ∈ Mnd ∧ K ⁡ S ⊆ Base G → Z ⁡ K ⁡ S ∈ SubMnd ⁡ G
20 15 19 syldan ⊢ G ∈ Mnd ∧ S ⊆ Z ⁡ S → Z ⁡ K ⁡ S ∈ SubMnd ⁡ G
21 2 mrcsscl ⊢ SubMnd ⁡ G ∈ Moore ⁡ Base G ∧ S ⊆ Z ⁡ K ⁡ S ∧ Z ⁡ K ⁡ S ∈ SubMnd ⁡ G → K ⁡ S ⊆ Z ⁡ K ⁡ S
22 7 18 20 21 syl3anc ⊢ G ∈ Mnd ∧ S ⊆ Z ⁡ S → K ⁡ S ⊆ Z ⁡ K ⁡ S
23 2 mrccl ⊢ SubMnd ⁡ G ∈ Moore ⁡ Base G ∧ S ⊆ Base G → K ⁡ S ∈ SubMnd ⁡ G
24 7 10 23 syl2anc ⊢ G ∈ Mnd ∧ S ⊆ Z ⁡ S → K ⁡ S ∈ SubMnd ⁡ G
25 3 1 submcmn2 ⊢ K ⁡ S ∈ SubMnd ⁡ G → H ∈ CMnd ↔ K ⁡ S ⊆ Z ⁡ K ⁡ S
26 24 25 syl ⊢ G ∈ Mnd ∧ S ⊆ Z ⁡ S → H ∈ CMnd ↔ K ⁡ S ⊆ Z ⁡ K ⁡ S
27 22 26 mpbird ⊢ G ∈ Mnd ∧ S ⊆ Z ⁡ S → H ∈ CMnd