Theorem subgcld

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

	Ref	Expression
Hypotheses	subgcld.1	|- .+ = ( +g ` G )
	subgcld.2	|- ( ph -> S e. ( SubGrp ` G ) )
	subgcld.3	|- ( ph -> X e. S )
	subgcld.4	|- ( ph -> Y e. S )
Assertion	subgcld	|- ( ph -> ( X .+ Y ) e. S )

Proof

Step	Hyp	Ref	Expression
1		subgcld.1	|- .+ = ( +g ` G )
2		subgcld.2	|- ( ph -> S e. ( SubGrp ` G ) )
3		subgcld.3	|- ( ph -> X e. S )
4		subgcld.4	|- ( ph -> Y e. S )
5	1	subgcl	|- ( ( S e. ( SubGrp ` G ) /\ X e. S /\ Y e. S ) -> ( X .+ Y ) e. S )
6	2 3 4 5	syl3anc	|- ( ph -> ( X .+ Y ) e. S )