Description: Closure of the group multiple (exponentiation) operation for a positive multiplier in a magma. (Contributed by Mario Carneiro, 11-Dec-2014) (Revised by AV, 29-Aug-2021)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | mulgnncl.b | |- B = ( Base ` G ) |
|
| mulgnncl.t | |- .x. = ( .g ` G ) |
||
| Assertion | mulgnncl | |- ( ( G e. Mgm /\ N e. NN /\ X e. B ) -> ( N .x. X ) e. B ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mulgnncl.b | |- B = ( Base ` G ) |
|
| 2 | mulgnncl.t | |- .x. = ( .g ` G ) |
|
| 3 | eqid | |- ( +g ` G ) = ( +g ` G ) |
|
| 4 | id | |- ( G e. Mgm -> G e. Mgm ) |
|
| 5 | ssidd | |- ( G e. Mgm -> B C_ B ) |
|
| 6 | 1 3 | mgmcl | |- ( ( G e. Mgm /\ x e. B /\ y e. B ) -> ( x ( +g ` G ) y ) e. B ) |
| 7 | 1 2 3 4 5 6 | mulgnnsubcl | |- ( ( G e. Mgm /\ N e. NN /\ X e. B ) -> ( N .x. X ) e. B ) |