Theorem subgmulgcld

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

	Ref	Expression
Hypotheses	subgmulgcld.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	subgmulgcld.x	⊢ · = ( .g ‘ 𝑅 )
	subgmulgcld.r	⊢ ( 𝜑 → 𝑅 ∈ Grp )
	subgmulgcld.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
	subgmulgcld.s	⊢ ( 𝜑 → 𝑆 ∈ ( SubGrp ‘ 𝑅 ) )
	subgmulgcld.z	⊢ ( 𝜑 → 𝑍 ∈ ℤ )
Assertion	subgmulgcld	⊢ ( 𝜑 → ( 𝑍 · 𝐴 ) ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		subgmulgcld.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		subgmulgcld.x	⊢ · = ( .g ‘ 𝑅 )
3		subgmulgcld.r	⊢ ( 𝜑 → 𝑅 ∈ Grp )
4		subgmulgcld.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
5		subgmulgcld.s	⊢ ( 𝜑 → 𝑆 ∈ ( SubGrp ‘ 𝑅 ) )
6		subgmulgcld.z	⊢ ( 𝜑 → 𝑍 ∈ ℤ )
7		eqid	⊢ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) = ( Base ‘ ( 𝑅 ↾s 𝑆 ) )
8		eqid	⊢ ( .g ‘ ( 𝑅 ↾s 𝑆 ) ) = ( .g ‘ ( 𝑅 ↾s 𝑆 ) )
9		eqid	⊢ ( 𝑅 ↾s 𝑆 ) = ( 𝑅 ↾s 𝑆 )
10	9	subggrp	⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝑅 ) → ( 𝑅 ↾s 𝑆 ) ∈ Grp )
11	5 10	syl	⊢ ( 𝜑 → ( 𝑅 ↾s 𝑆 ) ∈ Grp )
12	1	subgss	⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝑅 ) → 𝑆 ⊆ 𝐵 )
13	9 1	ressbas2	⊢ ( 𝑆 ⊆ 𝐵 → 𝑆 = ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) )
14	5 12 13	3syl	⊢ ( 𝜑 → 𝑆 = ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) )
15	4 14	eleqtrd	⊢ ( 𝜑 → 𝐴 ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) )
16	7 8 11 6 15	mulgcld	⊢ ( 𝜑 → ( 𝑍 ( .g ‘ ( 𝑅 ↾s 𝑆 ) ) 𝐴 ) ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) )
17	2 9 8	subgmulg	⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ∧ 𝑍 ∈ ℤ ∧ 𝐴 ∈ 𝑆 ) → ( 𝑍 · 𝐴 ) = ( 𝑍 ( .g ‘ ( 𝑅 ↾s 𝑆 ) ) 𝐴 ) )
18	5 6 4 17	syl3anc	⊢ ( 𝜑 → ( 𝑍 · 𝐴 ) = ( 𝑍 ( .g ‘ ( 𝑅 ↾s 𝑆 ) ) 𝐴 ) )
19	16 18 14	3eltr4d	⊢ ( 𝜑 → ( 𝑍 · 𝐴 ) ∈ 𝑆 )