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

Metamath Proof Explorer

Theorem subm0

Description: Submonoids have the same identity. (Contributed by Mario Carneiro, 7-Mar-2015)

Ref Expression
Hypotheses submmnd.h 
|- H = ( M |`s S )
subm0.z 
|- .0. = ( 0g ` M )
Assertion subm0 
|- ( S e. ( SubMnd ` M ) -> .0. = ( 0g ` H ) )

Proof

Step Hyp Ref Expression
1 submmnd.h 
 |-  H = ( M |`s S )
2 subm0.z 
 |-  .0. = ( 0g ` M )
3 submrcl 
 |-  ( S e. ( SubMnd ` M ) -> M e. Mnd )
4 1 submmnd 
 |-  ( S e. ( SubMnd ` M ) -> H e. Mnd )
5 eqid 
 |-  ( Base ` M ) = ( Base ` M )
6 5 submss 
 |-  ( S e. ( SubMnd ` M ) -> S C_ ( Base ` M ) )
7 2 subm0cl 
 |-  ( S e. ( SubMnd ` M ) -> .0. e. S )
8 5 2 1 submnd0 
 |-  ( ( ( M e. Mnd /\ H e. Mnd ) /\ ( S C_ ( Base ` M ) /\ .0. e. S ) ) -> .0. = ( 0g ` H ) )
9 3 4 6 7 8 syl22anc 
 |-  ( S e. ( SubMnd ` M ) -> .0. = ( 0g ` H ) )