Metamath Proof Explorer

Theorem submgmcl

Description: Submagmas are closed under the monoid operation. (Contributed by AV, 26-Feb-2020)

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

Proof

Step Hyp Ref Expression
1 submgmcl.p 
 |-  .+ = ( +g ` M )
2 submgmrcl 
 |-  ( S e. ( SubMgm ` M ) -> M e. Mgm )
3 eqid 
 |-  ( Base ` M ) = ( Base ` M )
4 3 1 issubmgm 
 |-  ( M e. Mgm -> ( S e. ( SubMgm ` M ) <-> ( S C_ ( Base ` M ) /\ A. x e. S A. y e. S ( x .+ y ) e. S ) ) )
5 2 4 syl 
 |-  ( S e. ( SubMgm ` M ) -> ( S e. ( SubMgm ` M ) <-> ( S C_ ( Base ` M ) /\ A. x e. S A. y e. S ( x .+ y ) e. S ) ) )
6 5 ibi 
 |-  ( S e. ( SubMgm ` M ) -> ( S C_ ( Base ` M ) /\ A. x e. S A. y e. S ( x .+ y ) e. S ) )
7 6 simprd 
 |-  ( S e. ( SubMgm ` M ) -> A. x e. S A. y e. S ( x .+ y ) e. S )
8 ovrspc2v 
 |-  ( ( ( X e. S /\ Y e. S ) /\ A. x e. S A. y e. S ( x .+ y ) e. S ) -> ( X .+ Y ) e. S )
9 7 8 sylan2 
 |-  ( ( ( X e. S /\ Y e. S ) /\ S e. ( SubMgm ` M ) ) -> ( X .+ Y ) e. S )
10 9 ancoms 
 |-  ( ( S e. ( SubMgm ` M ) /\ ( X e. S /\ Y e. S ) ) -> ( X .+ Y ) e. S )
11 10 3impb 
 |-  ( ( S e. ( SubMgm ` M ) /\ X e. S /\ Y e. S ) -> ( X .+ Y ) e. S )