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 
|- B = ( Base ` R )
subgmulgcld.x 
|- .x. = ( .g ` R )
subgmulgcld.r 
|- ( ph -> R e. Grp )
subgmulgcld.a 
|- ( ph -> A e. S )
subgmulgcld.s 
|- ( ph -> S e. ( SubGrp ` R ) )
subgmulgcld.z 
|- ( ph -> Z e. ZZ )
Assertion subgmulgcld 
|- ( ph -> ( Z .x. A ) e. S )

Proof

Step Hyp Ref Expression
1 subgmulgcld.b 
 |-  B = ( Base ` R )
2 subgmulgcld.x 
 |-  .x. = ( .g ` R )
3 subgmulgcld.r 
 |-  ( ph -> R e. Grp )
4 subgmulgcld.a 
 |-  ( ph -> A e. S )
5 subgmulgcld.s 
 |-  ( ph -> S e. ( SubGrp ` R ) )
6 subgmulgcld.z 
 |-  ( ph -> Z e. ZZ )
7 eqid 
 |-  ( Base ` ( R |`s S ) ) = ( Base ` ( R |`s S ) )
8 eqid 
 |-  ( .g ` ( R |`s S ) ) = ( .g ` ( R |`s S ) )
9 eqid 
 |-  ( R |`s S ) = ( R |`s S )
10 9 subggrp 
 |-  ( S e. ( SubGrp ` R ) -> ( R |`s S ) e. Grp )
11 5 10 syl 
 |-  ( ph -> ( R |`s S ) e. Grp )
12 1 subgss 
 |-  ( S e. ( SubGrp ` R ) -> S C_ B )
13 9 1 ressbas2 
 |-  ( S C_ B -> S = ( Base ` ( R |`s S ) ) )
14 5 12 13 3syl 
 |-  ( ph -> S = ( Base ` ( R |`s S ) ) )
15 4 14 eleqtrd 
 |-  ( ph -> A e. ( Base ` ( R |`s S ) ) )
16 7 8 11 6 15 mulgcld 
 |-  ( ph -> ( Z ( .g ` ( R |`s S ) ) A ) e. ( Base ` ( R |`s S ) ) )
17 2 9 8 subgmulg 
 |-  ( ( S e. ( SubGrp ` R ) /\ Z e. ZZ /\ A e. S ) -> ( Z .x. A ) = ( Z ( .g ` ( R |`s S ) ) A ) )
18 5 6 4 17 syl3anc 
 |-  ( ph -> ( Z .x. A ) = ( Z ( .g ` ( R |`s S ) ) A ) )
19 16 18 14 3eltr4d 
 |-  ( ph -> ( Z .x. A ) e. S )