Metamath Proof Explorer

Theorem mulgnnp1

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

Ref Expression
Hypotheses mulg1.b 
|- B = ( Base ` G )
mulg1.m 
|- .x. = ( .g ` G )
mulgnnp1.p 
|- .+ = ( +g ` G )
Assertion mulgnnp1 
|- ( ( N e. NN /\ X e. B ) -> ( ( N + 1 ) .x. X ) = ( ( N .x. X ) .+ X ) )

Proof

Step Hyp Ref Expression
1 mulg1.b 
 |-  B = ( Base ` G )
2 mulg1.m 
 |-  .x. = ( .g ` G )
3 mulgnnp1.p 
 |-  .+ = ( +g ` G )
4 simpl 
 |-  ( ( N e. NN /\ X e. B ) -> N e. NN )
5 nnuz 
 |-  NN = ( ZZ>= ` 1 )
6 4 5 eleqtrdi 
 |-  ( ( N e. NN /\ X e. B ) -> N e. ( ZZ>= ` 1 ) )
7 seqp1 
 |-  ( N e. ( ZZ>= ` 1 ) -> ( seq 1 ( .+ , ( NN X. { X } ) ) ` ( N + 1 ) ) = ( ( seq 1 ( .+ , ( NN X. { X } ) ) ` N ) .+ ( ( NN X. { X } ) ` ( N + 1 ) ) ) )
8 6 7 syl 
 |-  ( ( N e. NN /\ X e. B ) -> ( seq 1 ( .+ , ( NN X. { X } ) ) ` ( N + 1 ) ) = ( ( seq 1 ( .+ , ( NN X. { X } ) ) ` N ) .+ ( ( NN X. { X } ) ` ( N + 1 ) ) ) )
9 id 
 |-  ( X e. B -> X e. B )
10 peano2nn 
 |-  ( N e. NN -> ( N + 1 ) e. NN )
11 fvconst2g 
 |-  ( ( X e. B /\ ( N + 1 ) e. NN ) -> ( ( NN X. { X } ) ` ( N + 1 ) ) = X )
12 9 10 11 syl2anr 
 |-  ( ( N e. NN /\ X e. B ) -> ( ( NN X. { X } ) ` ( N + 1 ) ) = X )
13 12 oveq2d 
 |-  ( ( N e. NN /\ X e. B ) -> ( ( seq 1 ( .+ , ( NN X. { X } ) ) ` N ) .+ ( ( NN X. { X } ) ` ( N + 1 ) ) ) = ( ( seq 1 ( .+ , ( NN X. { X } ) ) ` N ) .+ X ) )
14 8 13 eqtrd 
 |-  ( ( N e. NN /\ X e. B ) -> ( seq 1 ( .+ , ( NN X. { X } ) ) ` ( N + 1 ) ) = ( ( seq 1 ( .+ , ( NN X. { X } ) ) ` N ) .+ X ) )
15 eqid 
 |-  seq 1 ( .+ , ( NN X. { X } ) ) = seq 1 ( .+ , ( NN X. { X } ) )
16 1 3 2 15 mulgnn 
 |-  ( ( ( N + 1 ) e. NN /\ X e. B ) -> ( ( N + 1 ) .x. X ) = ( seq 1 ( .+ , ( NN X. { X } ) ) ` ( N + 1 ) ) )
17 10 16 sylan 
 |-  ( ( N e. NN /\ X e. B ) -> ( ( N + 1 ) .x. X ) = ( seq 1 ( .+ , ( NN X. { X } ) ) ` ( N + 1 ) ) )
18 1 3 2 15 mulgnn 
 |-  ( ( N e. NN /\ X e. B ) -> ( N .x. X ) = ( seq 1 ( .+ , ( NN X. { X } ) ) ` N ) )
19 18 oveq1d 
 |-  ( ( N e. NN /\ X e. B ) -> ( ( N .x. X ) .+ X ) = ( ( seq 1 ( .+ , ( NN X. { X } ) ) ` N ) .+ X ) )
20 14 17 19 3eqtr4d 
 |-  ( ( N e. NN /\ X e. B ) -> ( ( N + 1 ) .x. X ) = ( ( N .x. X ) .+ X ) )