This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 |`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 )