Metamath Proof Explorer


Theorem mulgcld

Description: Deduction associated with mulgcl . (Contributed by Rohan Ridenour, 3-Aug-2023)

Ref Expression
Hypotheses mulgcld.1
|- B = ( Base ` G )
mulgcld.2
|- .x. = ( .g ` G )
mulgcld.3
|- ( ph -> G e. Grp )
mulgcld.4
|- ( ph -> N e. ZZ )
mulgcld.5
|- ( ph -> X e. B )
Assertion mulgcld
|- ( ph -> ( N .x. X ) e. B )

Proof

Step Hyp Ref Expression
1 mulgcld.1
 |-  B = ( Base ` G )
2 mulgcld.2
 |-  .x. = ( .g ` G )
3 mulgcld.3
 |-  ( ph -> G e. Grp )
4 mulgcld.4
 |-  ( ph -> N e. ZZ )
5 mulgcld.5
 |-  ( ph -> X e. B )
6 1 2 mulgcl
 |-  ( ( G e. Grp /\ N e. ZZ /\ X e. B ) -> ( N .x. X ) e. B )
7 3 4 5 6 syl3anc
 |-  ( ph -> ( N .x. X ) e. B )