Metamath Proof Explorer

Theorem submmnd

Description: Submonoids are themselves monoids under the given operation. (Contributed by Mario Carneiro, 7-Mar-2015)

Ref Expression
Hypothesis submmnd.h 
|- H = ( M |`s S )
Assertion submmnd 
|- ( S e. ( SubMnd ` M ) -> H e. Mnd )

Proof

Step Hyp Ref Expression
1 submmnd.h 
 |-  H = ( M |`s S )
2 submrcl 
 |-  ( S e. ( SubMnd ` M ) -> M e. Mnd )
3 eqid 
 |-  ( Base ` M ) = ( Base ` M )
4 eqid 
 |-  ( 0g ` M ) = ( 0g ` M )
5 3 4 1 issubm2 
 |-  ( M e. Mnd -> ( S e. ( SubMnd ` M ) <-> ( S C_ ( Base ` M ) /\ ( 0g ` M ) e. S /\ H e. Mnd ) ) )
6 2 5 syl 
 |-  ( S e. ( SubMnd ` M ) -> ( S e. ( SubMnd ` M ) <-> ( S C_ ( Base ` M ) /\ ( 0g ` M ) e. S /\ H e. Mnd ) ) )
7 6 ibi 
 |-  ( S e. ( SubMnd ` M ) -> ( S C_ ( Base ` M ) /\ ( 0g ` M ) e. S /\ H e. Mnd ) )
8 7 simp3d 
 |-  ( S e. ( SubMnd ` M ) -> H e. Mnd )