Metamath Proof Explorer

Theorem subcmn

Description: A submonoid of a commutative monoid is also commutative. (Contributed by Mario Carneiro, 10-Jan-2015)

Ref Expression
Hypothesis subgabl.h 
|- H = ( G |`s S )
Assertion subcmn 
|- ( ( G e. CMnd /\ H e. Mnd ) -> H e. CMnd )

Proof

Step Hyp Ref Expression
1 subgabl.h 
 |-  H = ( G |`s S )
2 eqidd 
 |-  ( ( G e. CMnd /\ H e. Mnd ) -> ( Base ` H ) = ( Base ` H ) )
3 eqid 
 |-  ( Base ` H ) = ( Base ` H )
4 eqid 
 |-  ( 0g ` H ) = ( 0g ` H )
5 3 4 mndidcl 
 |-  ( H e. Mnd -> ( 0g ` H ) e. ( Base ` H ) )
6 n0i 
 |-  ( ( 0g ` H ) e. ( Base ` H ) -> -. ( Base ` H ) = (/) )
7 5 6 syl 
 |-  ( H e. Mnd -> -. ( Base ` H ) = (/) )
8 reldmress 
 |-  Rel dom |`s
9 8 ovprc2 
 |-  ( -. S e. _V -> ( G |`s S ) = (/) )
10 1 9 syl5eq 
 |-  ( -. S e. _V -> H = (/) )
11 10 fveq2d 
 |-  ( -. S e. _V -> ( Base ` H ) = ( Base ` (/) ) )
12 base0 
 |-  (/) = ( Base ` (/) )
13 11 12 eqtr4di 
 |-  ( -. S e. _V -> ( Base ` H ) = (/) )
14 7 13 nsyl2 
 |-  ( H e. Mnd -> S e. _V )
15 14 adantl 
 |-  ( ( G e. CMnd /\ H e. Mnd ) -> S e. _V )
16 eqid 
 |-  ( +g ` G ) = ( +g ` G )
17 1 16 ressplusg 
 |-  ( S e. _V -> ( +g ` G ) = ( +g ` H ) )
18 15 17 syl 
 |-  ( ( G e. CMnd /\ H e. Mnd ) -> ( +g ` G ) = ( +g ` H ) )
19 simpr 
 |-  ( ( G e. CMnd /\ H e. Mnd ) -> H e. Mnd )
20 simpl 
 |-  ( ( G e. CMnd /\ H e. Mnd ) -> G e. CMnd )
21 eqid 
 |-  ( Base ` G ) = ( Base ` G )
22 1 21 ressbasss 
 |-  ( Base ` H ) C_ ( Base ` G )
23 22 sseli 
 |-  ( x e. ( Base ` H ) -> x e. ( Base ` G ) )
24 22 sseli 
 |-  ( y e. ( Base ` H ) -> y e. ( Base ` G ) )
25 21 16 cmncom 
 |-  ( ( G e. CMnd /\ x e. ( Base ` G ) /\ y e. ( Base ` G ) ) -> ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) )
26 20 23 24 25 syl3an 
 |-  ( ( ( G e. CMnd /\ H e. Mnd ) /\ x e. ( Base ` H ) /\ y e. ( Base ` H ) ) -> ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) )
27 2 18 19 26 iscmnd 
 |-  ( ( G e. CMnd /\ H e. Mnd ) -> H e. CMnd )