Theorem submcld

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

	Ref	Expression
Hypotheses	submcld.1	$$⊢\underset{\dot{}}{+}={+}_M$$
	submcld.2	$$⊢\phi \to S\in \mathrm{SubMnd}\left(M\right)$$
	submcld.3	$$⊢\phi \to X\in S$$
	submcld.4	$$⊢\phi \to Y\in S$$
Assertion	submcld	$$⊢\phi \to X\underset{\dot{}}{+}Y\in S$$

Proof

Step	Hyp	Ref	Expression
1		submcld.1	$$⊢\underset{\dot{}}{+}={+}_M$$
2		submcld.2	$$⊢\phi \to S\in \mathrm{SubMnd}\left(M\right)$$
3		submcld.3	$$⊢\phi \to X\in S$$
4		submcld.4	$$⊢\phi \to Y\in S$$
5	1	submcl	$$⊢\left(S\in \mathrm{SubMnd}\left(M\right)\wedge X\in S\wedge Y\in S\right)\to X\underset{\dot{}}{+}Y\in S$$
6	2 3 4 5	syl3anc	$$⊢\phi \to X\underset{\dot{}}{+}Y\in S$$