Theorem grpcld

Description: Closure of the operation of a group. (Contributed by SN, 29-Jul-2024)

	Ref	Expression
Hypotheses	grpcld.b	|- B = ( Base ` G )
	grpcld.p	|- .+ = ( +g ` G )
	grpcld.r	|- ( ph -> G e. Grp )
	grpcld.x	|- ( ph -> X e. B )
	grpcld.y	|- ( ph -> Y e. B )
Assertion	grpcld	|- ( ph -> ( X .+ Y ) e. B )

Proof

Step	Hyp	Ref	Expression
1		grpcld.b	|- B = ( Base ` G )
2		grpcld.p	|- .+ = ( +g ` G )
3		grpcld.r	|- ( ph -> G e. Grp )
4		grpcld.x	|- ( ph -> X e. B )
5		grpcld.y	|- ( ph -> Y e. B )
6	1 2	grpcl	|- ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( X .+ Y ) e. B )
7	3 4 5 6	syl3anc	|- ( ph -> ( X .+ Y ) e. B )