Theorem subgmulgcld

Description: Closure of the group multiple within a subgroup. (Contributed by Thierry Arnoux, 5-Oct-2025)

	Ref	Expression
Hypotheses	subgmulgcld.b	|- B = ( Base ` R )
	subgmulgcld.x	|- .x. = ( .g ` R )
	subgmulgcld.r	|- ( ph -> R e. Grp )
	subgmulgcld.a	|- ( ph -> A e. S )
	subgmulgcld.s	|- ( ph -> S e. ( SubGrp ` R ) )
	subgmulgcld.z	|- ( ph -> Z e. ZZ )
Assertion	subgmulgcld	|- ( ph -> ( Z .x. A ) e. S )

Proof

Step	Hyp	Ref	Expression
1		subgmulgcld.b	|- B = ( Base ` R )
2		subgmulgcld.x	|- .x. = ( .g ` R )
3		subgmulgcld.r	|- ( ph -> R e. Grp )
4		subgmulgcld.a	|- ( ph -> A e. S )
5		subgmulgcld.s	|- ( ph -> S e. ( SubGrp ` R ) )
6		subgmulgcld.z	|- ( ph -> Z e. ZZ )
7		eqid	|- ( Base ` ( R |`s S ) ) = ( Base ` ( R |`s S ) )
8		eqid	|- ( .g ` ( R |`s S ) ) = ( .g ` ( R |`s S ) )
9		eqid	|- ( R |`s S ) = ( R |`s S )
10	9	subggrp	|- ( S e. ( SubGrp ` R ) -> ( R |`s S ) e. Grp )
11	5 10	syl	|- ( ph -> ( R |`s S ) e. Grp )
12	1	subgss	|- ( S e. ( SubGrp ` R ) -> S C_ B )
13	9 1	ressbas2	|- ( S C_ B -> S = ( Base ` ( R |`s S ) ) )
14	5 12 13	3syl	|- ( ph -> S = ( Base ` ( R |`s S ) ) )
15	4 14	eleqtrd	|- ( ph -> A e. ( Base ` ( R |`s S ) ) )
16	7 8 11 6 15	mulgcld	|- ( ph -> ( Z ( .g ` ( R |`s S ) ) A ) e. ( Base ` ( R |`s S ) ) )
17	2 9 8	subgmulg	|- ( ( S e. ( SubGrp ` R ) /\ Z e. ZZ /\ A e. S ) -> ( Z .x. A ) = ( Z ( .g ` ( R |`s S ) ) A ) )
18	5 6 4 17	syl3anc	|- ( ph -> ( Z .x. A ) = ( Z ( .g ` ( R |`s S ) ) A ) )
19	16 18 14	3eltr4d	|- ( ph -> ( Z .x. A ) e. S )