Theorem subgcld

Description: A subgroup is closed under group operation. (Contributed by Thierry Arnoux, 3-Jun-2025)

	Ref	Expression
Hypotheses	subgcld.1	$$⊢\underset{\dot{}}{+}={+}_G$$
	subgcld.2	$$⊢\phi \to S\in \mathrm{SubGrp}\left(G\right)$$
	subgcld.3	$$⊢\phi \to X\in S$$
	subgcld.4	$$⊢\phi \to Y\in S$$
Assertion	subgcld	$$⊢\phi \to X\underset{\dot{}}{+}Y\in S$$

Proof

Step	Hyp	Ref	Expression
1		subgcld.1	$$⊢\underset{\dot{}}{+}={+}_G$$
2		subgcld.2	$$⊢\phi \to S\in \mathrm{SubGrp}\left(G\right)$$
3		subgcld.3	$$⊢\phi \to X\in S$$
4		subgcld.4	$$⊢\phi \to Y\in S$$
5	1	subgcl	$$⊢\left(S\in \mathrm{SubGrp}\left(G\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$$