subgmulgcld

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

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

Metamath Proof Explorer