This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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