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 ) |
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 ) |