Metamath Proof Explorer

Theorem mulgp1

Description: Group multiple (exponentiation) operation at a successor, extended to ZZ . (Contributed by Mario Carneiro, 11-Dec-2014)

Ref Expression
Hypotheses mulgnndir.b 
|- B = ( Base ` G )
mulgnndir.t 
|- .x. = ( .g ` G )
mulgnndir.p 
|- .+ = ( +g ` G )
Assertion mulgp1 
|- ( ( G e. Grp /\ N e. ZZ /\ X e. B ) -> ( ( N + 1 ) .x. X ) = ( ( N .x. X ) .+ X ) )

Proof

Step Hyp Ref Expression
1 mulgnndir.b 
 |-  B = ( Base ` G )
2 mulgnndir.t 
 |-  .x. = ( .g ` G )
3 mulgnndir.p 
 |-  .+ = ( +g ` G )
4 1z 
 |-  1 e. ZZ
5 1 2 3 mulgdir 
 |-  ( ( G e. Grp /\ ( N e. ZZ /\ 1 e. ZZ /\ X e. B ) ) -> ( ( N + 1 ) .x. X ) = ( ( N .x. X ) .+ ( 1 .x. X ) ) )
6 4 5 mp3anr2 
 |-  ( ( G e. Grp /\ ( N e. ZZ /\ X e. B ) ) -> ( ( N + 1 ) .x. X ) = ( ( N .x. X ) .+ ( 1 .x. X ) ) )
7 6 3impb 
 |-  ( ( G e. Grp /\ N e. ZZ /\ X e. B ) -> ( ( N + 1 ) .x. X ) = ( ( N .x. X ) .+ ( 1 .x. X ) ) )
8 1 2 mulg1 
 |-  ( X e. B -> ( 1 .x. X ) = X )
9 8 3ad2ant3 
 |-  ( ( G e. Grp /\ N e. ZZ /\ X e. B ) -> ( 1 .x. X ) = X )
10 9 oveq2d 
 |-  ( ( G e. Grp /\ N e. ZZ /\ X e. B ) -> ( ( N .x. X ) .+ ( 1 .x. X ) ) = ( ( N .x. X ) .+ X ) )
11 7 10 eqtrd 
 |-  ( ( G e. Grp /\ N e. ZZ /\ X e. B ) -> ( ( N + 1 ) .x. X ) = ( ( N .x. X ) .+ X ) )