Metamath Proof Explorer

Theorem mulgnn0p1

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

Ref Expression
Hypotheses mulgnn0p1.b 
|- B = ( Base ` G )
mulgnn0p1.t 
|- .x. = ( .g ` G )
mulgnn0p1.p 
|- .+ = ( +g ` G )
Assertion mulgnn0p1 
|- ( ( G e. Mnd /\ N e. NN0 /\ X e. B ) -> ( ( N + 1 ) .x. X ) = ( ( N .x. X ) .+ X ) )

Proof

Step Hyp Ref Expression
1 mulgnn0p1.b 
 |-  B = ( Base ` G )
2 mulgnn0p1.t 
 |-  .x. = ( .g ` G )
3 mulgnn0p1.p 
 |-  .+ = ( +g ` G )
4 simpr 
 |-  ( ( ( G e. Mnd /\ N e. NN0 /\ X e. B ) /\ N e. NN ) -> N e. NN )
5 simpl3 
 |-  ( ( ( G e. Mnd /\ N e. NN0 /\ X e. B ) /\ N e. NN ) -> X e. B )
6 1 2 3 mulgnnp1 
 |-  ( ( N e. NN /\ X e. B ) -> ( ( N + 1 ) .x. X ) = ( ( N .x. X ) .+ X ) )
7 4 5 6 syl2anc 
 |-  ( ( ( G e. Mnd /\ N e. NN0 /\ X e. B ) /\ N e. NN ) -> ( ( N + 1 ) .x. X ) = ( ( N .x. X ) .+ X ) )
8 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
9 1 3 8 mndlid 
 |-  ( ( G e. Mnd /\ X e. B ) -> ( ( 0g ` G ) .+ X ) = X )
10 1 8 2 mulg0 
 |-  ( X e. B -> ( 0 .x. X ) = ( 0g ` G ) )
11 10 adantl 
 |-  ( ( G e. Mnd /\ X e. B ) -> ( 0 .x. X ) = ( 0g ` G ) )
12 11 oveq1d 
 |-  ( ( G e. Mnd /\ X e. B ) -> ( ( 0 .x. X ) .+ X ) = ( ( 0g ` G ) .+ X ) )
13 1 2 mulg1 
 |-  ( X e. B -> ( 1 .x. X ) = X )
14 13 adantl 
 |-  ( ( G e. Mnd /\ X e. B ) -> ( 1 .x. X ) = X )
15 9 12 14 3eqtr4rd 
 |-  ( ( G e. Mnd /\ X e. B ) -> ( 1 .x. X ) = ( ( 0 .x. X ) .+ X ) )
16 15 3adant2 
 |-  ( ( G e. Mnd /\ N e. NN0 /\ X e. B ) -> ( 1 .x. X ) = ( ( 0 .x. X ) .+ X ) )
17 oveq1 
 |-  ( N = 0 -> ( N + 1 ) = ( 0 + 1 ) )
18 1e0p1 
 |-  1 = ( 0 + 1 )
19 17 18 eqtr4di 
 |-  ( N = 0 -> ( N + 1 ) = 1 )
20 19 oveq1d 
 |-  ( N = 0 -> ( ( N + 1 ) .x. X ) = ( 1 .x. X ) )
21 oveq1 
 |-  ( N = 0 -> ( N .x. X ) = ( 0 .x. X ) )
22 21 oveq1d 
 |-  ( N = 0 -> ( ( N .x. X ) .+ X ) = ( ( 0 .x. X ) .+ X ) )
23 20 22 eqeq12d 
 |-  ( N = 0 -> ( ( ( N + 1 ) .x. X ) = ( ( N .x. X ) .+ X ) <-> ( 1 .x. X ) = ( ( 0 .x. X ) .+ X ) ) )
24 16 23 syl5ibrcom 
 |-  ( ( G e. Mnd /\ N e. NN0 /\ X e. B ) -> ( N = 0 -> ( ( N + 1 ) .x. X ) = ( ( N .x. X ) .+ X ) ) )
25 24 imp 
 |-  ( ( ( G e. Mnd /\ N e. NN0 /\ X e. B ) /\ N = 0 ) -> ( ( N + 1 ) .x. X ) = ( ( N .x. X ) .+ X ) )
26 simp2 
 |-  ( ( G e. Mnd /\ N e. NN0 /\ X e. B ) -> N e. NN0 )
27 elnn0 
 |-  ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
28 26 27 sylib 
 |-  ( ( G e. Mnd /\ N e. NN0 /\ X e. B ) -> ( N e. NN \/ N = 0 ) )
29 7 25 28 mpjaodan 
 |-  ( ( G e. Mnd /\ N e. NN0 /\ X e. B ) -> ( ( N + 1 ) .x. X ) = ( ( N .x. X ) .+ X ) )