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 B = Base R
subgmulgcld.x · ˙ = R
subgmulgcld.r φ R Grp
subgmulgcld.a φ A S
subgmulgcld.s φ S SubGrp R
subgmulgcld.z φ Z
Assertion subgmulgcld φ Z · ˙ A S

Proof

Step Hyp Ref Expression
1 subgmulgcld.b B = Base R
2 subgmulgcld.x · ˙ = R
3 subgmulgcld.r φ R Grp
4 subgmulgcld.a φ A S
5 subgmulgcld.s φ S SubGrp R
6 subgmulgcld.z φ Z
7 eqid Base R 𝑠 S = Base R 𝑠 S
8 eqid R 𝑠 S = R 𝑠 S
9 eqid R 𝑠 S = R 𝑠 S
10 9 subggrp S SubGrp R R 𝑠 S Grp
11 5 10 syl φ R 𝑠 S Grp
12 1 subgss S SubGrp R S B
13 9 1 ressbas2 S B S = Base R 𝑠 S
14 5 12 13 3syl φ S = Base R 𝑠 S
15 4 14 eleqtrd φ A Base R 𝑠 S
16 7 8 11 6 15 mulgcld φ Z R 𝑠 S A Base R 𝑠 S
17 2 9 8 subgmulg S SubGrp R Z A S Z · ˙ A = Z R 𝑠 S A
18 5 6 4 17 syl3anc φ Z · ˙ A = Z R 𝑠 S A
19 16 18 14 3eltr4d φ Z · ˙ A S