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 |`s ( K ` S ) )
Assertion	cntzspan	|- ( ( G e. Mnd /\ S C_ ( Z ` S ) ) -> H e. CMnd )

Proof

Step	Hyp	Ref	Expression
1		cntzspan.z	|- Z = ( Cntz ` G )
2		cntzspan.k	|- K = ( mrCls ` ( SubMnd ` G ) )
3		cntzspan.h	|- H = ( G |`s ( K ` S ) )
4		eqid	|- ( Base ` G ) = ( Base ` G )
5	4	submacs	|- ( G e. Mnd -> ( SubMnd ` G ) e. ( ACS ` ( Base ` G ) ) )
6	5	adantr	|- ( ( G e. Mnd /\ S C_ ( Z ` S ) ) -> ( SubMnd ` G ) e. ( ACS ` ( Base ` G ) ) )
7	6	acsmred	|- ( ( G e. Mnd /\ S C_ ( Z ` S ) ) -> ( SubMnd ` G ) e. ( Moore ` ( Base ` G ) ) )
8		simpr	|- ( ( G e. Mnd /\ S C_ ( Z ` S ) ) -> S C_ ( Z ` S ) )
9	4 1	cntzssv	|- ( Z ` S ) C_ ( Base ` G )
10	8 9	sstrdi	|- ( ( G e. Mnd /\ S C_ ( Z ` S ) ) -> S C_ ( Base ` G ) )
11	4 1	cntzsubm	|- ( ( G e. Mnd /\ S C_ ( Base ` G ) ) -> ( Z ` S ) e. ( SubMnd ` G ) )
12	10 11	syldan	|- ( ( G e. Mnd /\ S C_ ( Z ` S ) ) -> ( Z ` S ) e. ( SubMnd ` G ) )
13	2	mrcsscl	|- ( ( ( SubMnd ` G ) e. ( Moore ` ( Base ` G ) ) /\ S C_ ( Z ` S ) /\ ( Z ` S ) e. ( SubMnd ` G ) ) -> ( K ` S ) C_ ( Z ` S ) )
14	7 8 12 13	syl3anc	|- ( ( G e. Mnd /\ S C_ ( Z ` S ) ) -> ( K ` S ) C_ ( Z ` S ) )
15	7 2	mrcssvd	|- ( ( G e. Mnd /\ S C_ ( Z ` S ) ) -> ( K ` S ) C_ ( Base ` G ) )
16	4 1	cntzrec	|- ( ( ( K ` S ) C_ ( Base ` G ) /\ S C_ ( Base ` G ) ) -> ( ( K ` S ) C_ ( Z ` S ) <-> S C_ ( Z ` ( K ` S ) ) ) )
17	15 10 16	syl2anc	|- ( ( G e. Mnd /\ S C_ ( Z ` S ) ) -> ( ( K ` S ) C_ ( Z ` S ) <-> S C_ ( Z ` ( K ` S ) ) ) )
18	14 17	mpbid	|- ( ( G e. Mnd /\ S C_ ( Z ` S ) ) -> S C_ ( Z ` ( K ` S ) ) )
19	4 1	cntzsubm	|- ( ( G e. Mnd /\ ( K ` S ) C_ ( Base ` G ) ) -> ( Z ` ( K ` S ) ) e. ( SubMnd ` G ) )
20	15 19	syldan	|- ( ( G e. Mnd /\ S C_ ( Z ` S ) ) -> ( Z ` ( K ` S ) ) e. ( SubMnd ` G ) )
21	2	mrcsscl	|- ( ( ( SubMnd ` G ) e. ( Moore ` ( Base ` G ) ) /\ S C_ ( Z ` ( K ` S ) ) /\ ( Z ` ( K ` S ) ) e. ( SubMnd ` G ) ) -> ( K ` S ) C_ ( Z ` ( K ` S ) ) )
22	7 18 20 21	syl3anc	|- ( ( G e. Mnd /\ S C_ ( Z ` S ) ) -> ( K ` S ) C_ ( Z ` ( K ` S ) ) )
23	2	mrccl	|- ( ( ( SubMnd ` G ) e. ( Moore ` ( Base ` G ) ) /\ S C_ ( Base ` G ) ) -> ( K ` S ) e. ( SubMnd ` G ) )
24	7 10 23	syl2anc	|- ( ( G e. Mnd /\ S C_ ( Z ` S ) ) -> ( K ` S ) e. ( SubMnd ` G ) )
25	3 1	submcmn2	|- ( ( K ` S ) e. ( SubMnd ` G ) -> ( H e. CMnd <-> ( K ` S ) C_ ( Z ` ( K ` S ) ) ) )
26	24 25	syl	|- ( ( G e. Mnd /\ S C_ ( Z ` S ) ) -> ( H e. CMnd <-> ( K ` S ) C_ ( Z ` ( K ` S ) ) ) )
27	22 26	mpbird	|- ( ( G e. Mnd /\ S C_ ( Z ` S ) ) -> H e. CMnd )