Metamath Proof Explorer


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 ( 𝜑 → ( 𝑍 · 𝐴 ) ∈ 𝑆 )