Theorem submcld

Description: Submonoids are closed under the monoid operation. (Contributed by Thierry Arnoux, 4-May-2025)

	Ref	Expression
Hypotheses	submcld.1	|- .+ = ( +g ` M )
	submcld.2	|- ( ph -> S e. ( SubMnd ` M ) )
	submcld.3	|- ( ph -> X e. S )
	submcld.4	|- ( ph -> Y e. S )
Assertion	submcld	|- ( ph -> ( X .+ Y ) e. S )

Proof

Step	Hyp	Ref	Expression
1		submcld.1	|- .+ = ( +g ` M )
2		submcld.2	|- ( ph -> S e. ( SubMnd ` M ) )
3		submcld.3	|- ( ph -> X e. S )
4		submcld.4	|- ( ph -> Y e. S )
5	1	submcl	|- ( ( S e. ( SubMnd ` M ) /\ X e. S /\ Y e. S ) -> ( X .+ Y ) e. S )
6	2 3 4 5	syl3anc	|- ( ph -> ( X .+ Y ) e. S )