Theorem subgcld

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

	Ref	Expression
Hypotheses	subgcld.1	⊢ + = ( +g ‘ 𝐺 )
	subgcld.2	⊢ ( 𝜑 → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
	subgcld.3	⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
	subgcld.4	⊢ ( 𝜑 → 𝑌 ∈ 𝑆 )
Assertion	subgcld	⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		subgcld.1	⊢ + = ( +g ‘ 𝐺 )
2		subgcld.2	⊢ ( 𝜑 → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
3		subgcld.3	⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
4		subgcld.4	⊢ ( 𝜑 → 𝑌 ∈ 𝑆 )
5	1	subgcl	⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → ( 𝑋 + 𝑌 ) ∈ 𝑆 )
6	2 3 4 5	syl3anc	⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ 𝑆 )