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

Metamath Proof Explorer

Theorem submcl

Description: Submonoids are closed under the monoid operation. (Contributed by Mario Carneiro, 10-Mar-2015)

Ref Expression
Hypothesis submcl.p 
|- .+ = ( +g ` M )
Assertion submcl 
|- ( ( S e. ( SubMnd ` M ) /\ X e. S /\ Y e. S ) -> ( X .+ Y ) e. S )

Proof

Step Hyp Ref Expression
1 submcl.p 
 |-  .+ = ( +g ` M )
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 issubm 
 |-  ( M e. Mnd -> ( S e. ( SubMnd ` M ) <-> ( S C_ ( Base ` M ) /\ ( 0g ` M ) e. S /\ A. x e. S A. y e. S ( x .+ y ) e. S ) ) )
6 2 5 syl 
 |-  ( S e. ( SubMnd ` M ) -> ( S e. ( SubMnd ` M ) <-> ( S C_ ( Base ` M ) /\ ( 0g ` M ) e. S /\ A. x e. S A. y e. S ( x .+ y ) e. S ) ) )
7 6 ibi 
 |-  ( S e. ( SubMnd ` M ) -> ( S C_ ( Base ` M ) /\ ( 0g ` M ) e. S /\ A. x e. S A. y e. S ( x .+ y ) e. S ) )
8 7 simp3d 
 |-  ( S e. ( SubMnd ` M ) -> A. x e. S A. y e. S ( x .+ y ) e. S )
9 ovrspc2v 
 |-  ( ( ( X e. S /\ Y e. S ) /\ A. x e. S A. y e. S ( x .+ y ) e. S ) -> ( X .+ Y ) e. S )
10 8 9 sylan2 
 |-  ( ( ( X e. S /\ Y e. S ) /\ S e. ( SubMnd ` M ) ) -> ( X .+ Y ) e. S )
11 10 ancoms 
 |-  ( ( S e. ( SubMnd ` M ) /\ ( X e. S /\ Y e. S ) ) -> ( X .+ Y ) e. S )
12 11 3impb 
 |-  ( ( S e. ( SubMnd ` M ) /\ X e. S /\ Y e. S ) -> ( X .+ Y ) e. S )