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 ⊢ 𝑍 = ( Cntz ‘ 𝐺 )
cntzspan.k ⊢ 𝐾 = ( mrCls ‘ ( SubMnd ‘ 𝐺 ) )
cntzspan.h ⊢ 𝐻 = ( 𝐺 ↾s ( 𝐾 ‘ 𝑆 ) )
Assertion cntzspan ( ( 𝐺 ∈ Mnd ∧ 𝑆 ⊆ ( 𝑍 ‘ 𝑆 ) ) → 𝐻 ∈ CMnd )

Proof

Step Hyp Ref Expression
1 cntzspan.z ⊢ 𝑍 = ( Cntz ‘ 𝐺 )
2 cntzspan.k ⊢ 𝐾 = ( mrCls ‘ ( SubMnd ‘ 𝐺 ) )
3 cntzspan.h ⊢ 𝐻 = ( 𝐺 ↾s ( 𝐾 ‘ 𝑆 ) )
4 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
5 4 submacs ⊢ ( 𝐺 ∈ Mnd → ( SubMnd ‘ 𝐺 ) ∈ ( ACS ‘ ( Base ‘ 𝐺 ) ) )
6 5 adantr ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑆 ⊆ ( 𝑍 ‘ 𝑆 ) ) → ( SubMnd ‘ 𝐺 ) ∈ ( ACS ‘ ( Base ‘ 𝐺 ) ) )
7 6 acsmred ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑆 ⊆ ( 𝑍 ‘ 𝑆 ) ) → ( SubMnd ‘ 𝐺 ) ∈ ( Moore ‘ ( Base ‘ 𝐺 ) ) )
8 simpr ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑆 ⊆ ( 𝑍 ‘ 𝑆 ) ) → 𝑆 ⊆ ( 𝑍 ‘ 𝑆 ) )
9 4 1 cntzssv ⊢ ( 𝑍 ‘ 𝑆 ) ⊆ ( Base ‘ 𝐺 )
10 8 9 sstrdi ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑆 ⊆ ( 𝑍 ‘ 𝑆 ) ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
11 4 1 cntzsubm ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑆 ⊆ ( Base ‘ 𝐺 ) ) → ( 𝑍 ‘ 𝑆 ) ∈ ( SubMnd ‘ 𝐺 ) )
12 10 11 syldan ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑆 ⊆ ( 𝑍 ‘ 𝑆 ) ) → ( 𝑍 ‘ 𝑆 ) ∈ ( SubMnd ‘ 𝐺 ) )
13 2 mrcsscl ⊢ ( ( ( SubMnd ‘ 𝐺 ) ∈ ( Moore ‘ ( Base ‘ 𝐺 ) ) ∧ 𝑆 ⊆ ( 𝑍 ‘ 𝑆 ) ∧ ( 𝑍 ‘ 𝑆 ) ∈ ( SubMnd ‘ 𝐺 ) ) → ( 𝐾 ‘ 𝑆 ) ⊆ ( 𝑍 ‘ 𝑆 ) )
14 7 8 12 13 syl3anc ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑆 ⊆ ( 𝑍 ‘ 𝑆 ) ) → ( 𝐾 ‘ 𝑆 ) ⊆ ( 𝑍 ‘ 𝑆 ) )
15 7 2 mrcssvd ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑆 ⊆ ( 𝑍 ‘ 𝑆 ) ) → ( 𝐾 ‘ 𝑆 ) ⊆ ( Base ‘ 𝐺 ) )
16 4 1 cntzrec ⊢ ( ( ( 𝐾 ‘ 𝑆 ) ⊆ ( Base ‘ 𝐺 ) ∧ 𝑆 ⊆ ( Base ‘ 𝐺 ) ) → ( ( 𝐾 ‘ 𝑆 ) ⊆ ( 𝑍 ‘ 𝑆 ) ↔ 𝑆 ⊆ ( 𝑍 ‘ ( 𝐾 ‘ 𝑆 ) ) ) )
17 15 10 16 syl2anc ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑆 ⊆ ( 𝑍 ‘ 𝑆 ) ) → ( ( 𝐾 ‘ 𝑆 ) ⊆ ( 𝑍 ‘ 𝑆 ) ↔ 𝑆 ⊆ ( 𝑍 ‘ ( 𝐾 ‘ 𝑆 ) ) ) )
18 14 17 mpbid ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑆 ⊆ ( 𝑍 ‘ 𝑆 ) ) → 𝑆 ⊆ ( 𝑍 ‘ ( 𝐾 ‘ 𝑆 ) ) )
19 4 1 cntzsubm ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝐾 ‘ 𝑆 ) ⊆ ( Base ‘ 𝐺 ) ) → ( 𝑍 ‘ ( 𝐾 ‘ 𝑆 ) ) ∈ ( SubMnd ‘ 𝐺 ) )
20 15 19 syldan ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑆 ⊆ ( 𝑍 ‘ 𝑆 ) ) → ( 𝑍 ‘ ( 𝐾 ‘ 𝑆 ) ) ∈ ( SubMnd ‘ 𝐺 ) )
21 2 mrcsscl ⊢ ( ( ( SubMnd ‘ 𝐺 ) ∈ ( Moore ‘ ( Base ‘ 𝐺 ) ) ∧ 𝑆 ⊆ ( 𝑍 ‘ ( 𝐾 ‘ 𝑆 ) ) ∧ ( 𝑍 ‘ ( 𝐾 ‘ 𝑆 ) ) ∈ ( SubMnd ‘ 𝐺 ) ) → ( 𝐾 ‘ 𝑆 ) ⊆ ( 𝑍 ‘ ( 𝐾 ‘ 𝑆 ) ) )
22 7 18 20 21 syl3anc ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑆 ⊆ ( 𝑍 ‘ 𝑆 ) ) → ( 𝐾 ‘ 𝑆 ) ⊆ ( 𝑍 ‘ ( 𝐾 ‘ 𝑆 ) ) )
23 2 mrccl ⊢ ( ( ( SubMnd ‘ 𝐺 ) ∈ ( Moore ‘ ( Base ‘ 𝐺 ) ) ∧ 𝑆 ⊆ ( Base ‘ 𝐺 ) ) → ( 𝐾 ‘ 𝑆 ) ∈ ( SubMnd ‘ 𝐺 ) )
24 7 10 23 syl2anc ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑆 ⊆ ( 𝑍 ‘ 𝑆 ) ) → ( 𝐾 ‘ 𝑆 ) ∈ ( SubMnd ‘ 𝐺 ) )
25 3 1 submcmn2 ⊢ ( ( 𝐾 ‘ 𝑆 ) ∈ ( SubMnd ‘ 𝐺 ) → ( 𝐻 ∈ CMnd ↔ ( 𝐾 ‘ 𝑆 ) ⊆ ( 𝑍 ‘ ( 𝐾 ‘ 𝑆 ) ) ) )
26 24 25 syl ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑆 ⊆ ( 𝑍 ‘ 𝑆 ) ) → ( 𝐻 ∈ CMnd ↔ ( 𝐾 ‘ 𝑆 ) ⊆ ( 𝑍 ‘ ( 𝐾 ‘ 𝑆 ) ) ) )
27 22 26 mpbird ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑆 ⊆ ( 𝑍 ‘ 𝑆 ) ) → 𝐻 ∈ CMnd )