Theorem submcld

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

	Ref	Expression
Hypotheses	submcld.1	⊢ + = ( +g ‘ 𝑀 )
	submcld.2	⊢ ( 𝜑 → 𝑆 ∈ ( SubMnd ‘ 𝑀 ) )
	submcld.3	⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
	submcld.4	⊢ ( 𝜑 → 𝑌 ∈ 𝑆 )
Assertion	submcld	⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		submcld.1	⊢ + = ( +g ‘ 𝑀 )
2		submcld.2	⊢ ( 𝜑 → 𝑆 ∈ ( SubMnd ‘ 𝑀 ) )
3		submcld.3	⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
4		submcld.4	⊢ ( 𝜑 → 𝑌 ∈ 𝑆 )
5	1	submcl	⊢ ( ( 𝑆 ∈ ( SubMnd ‘ 𝑀 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → ( 𝑋 + 𝑌 ) ∈ 𝑆 )
6	2 3 4 5	syl3anc	⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ 𝑆 )