Theorem subgmulgcld

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

	Ref	Expression
Hypotheses	subgmulgcld.b	$$⊢B={\mathrm{Base}}_R$$
	subgmulgcld.x	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	subgmulgcld.r	$$⊢\phi \to R\in \mathrm{Grp}$$
	subgmulgcld.a	$$⊢\phi \to A\in S$$
	subgmulgcld.s	$$⊢\phi \to S\in \mathrm{SubGrp}\left(R\right)$$
	subgmulgcld.z	$$⊢\phi \to Z\in \mathbb{Z}$$
Assertion	subgmulgcld	$$⊢\phi \to Z\underset{\dot{}}{·}A\in S$$

Proof

Step	Hyp	Ref	Expression
1		subgmulgcld.b	$$⊢B={\mathrm{Base}}_R$$
2		subgmulgcld.x	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
3		subgmulgcld.r	$$⊢\phi \to R\in \mathrm{Grp}$$
4		subgmulgcld.a	$$⊢\phi \to A\in S$$
5		subgmulgcld.s	$$⊢\phi \to S\in \mathrm{SubGrp}\left(R\right)$$
6		subgmulgcld.z	$$⊢\phi \to Z\in \mathbb{Z}$$
7		eqid	$$⊢{\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}S\right)}={\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}S\right)}$$
8		eqid	$$⊢{\cdot }_{\left(R{\upharpoonright }_{𝑠}S\right)}={\cdot }_{\left(R{\upharpoonright }_{𝑠}S\right)}$$
9		eqid	$$⊢R{\upharpoonright }_{𝑠}S=R{\upharpoonright }_{𝑠}S$$
10	9	subggrp	$$⊢S\in \mathrm{SubGrp}\left(R\right)\to R{\upharpoonright }_{𝑠}S\in \mathrm{Grp}$$
11	5 10	syl	$$⊢\phi \to R{\upharpoonright }_{𝑠}S\in \mathrm{Grp}$$
12	1	subgss	$$⊢S\in \mathrm{SubGrp}\left(R\right)\to S\subseteq B$$
13	9 1	ressbas2	$$⊢S\subseteq B\to S={\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}S\right)}$$
14	5 12 13	3syl	$$⊢\phi \to S={\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}S\right)}$$
15	4 14	eleqtrd	$$⊢\phi \to A\in {\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}S\right)}$$
16	7 8 11 6 15	mulgcld	$$⊢\phi \to Z{\cdot }_{\left(R{\upharpoonright }_{𝑠}S\right)}A\in {\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}S\right)}$$
17	2 9 8	subgmulg	$$⊢\left(S\in \mathrm{SubGrp}\left(R\right)\wedge Z\in \mathbb{Z}\wedge A\in S\right)\to Z\underset{\dot{}}{·}A=Z{\cdot }_{\left(R{\upharpoonright }_{𝑠}S\right)}A$$
18	5 6 4 17	syl3anc	$$⊢\phi \to Z\underset{\dot{}}{·}A=Z{\cdot }_{\left(R{\upharpoonright }_{𝑠}S\right)}A$$
19	16 18 14	3eltr4d	$$⊢\phi \to Z\underset{\dot{}}{·}A\in S$$