Metamath Proof Explorer

Theorem mulgnnsubcl

Description: Closure of the group multiple (exponentiation) operation in a subsemigroup. (Contributed by Mario Carneiro, 10-Jan-2015)

Ref Expression
Hypotheses mulgnnsubcl.b 
|- B = ( Base ` G )
mulgnnsubcl.t 
|- .x. = ( .g ` G )
mulgnnsubcl.p 
|- .+ = ( +g ` G )
mulgnnsubcl.g 
|- ( ph -> G e. V )
mulgnnsubcl.s 
|- ( ph -> S C_ B )
mulgnnsubcl.c 
|- ( ( ph /\ x e. S /\ y e. S ) -> ( x .+ y ) e. S )
Assertion mulgnnsubcl 
|- ( ( ph /\ N e. NN /\ X e. S ) -> ( N .x. X ) e. S )

Proof

Step Hyp Ref Expression
1 mulgnnsubcl.b 
 |-  B = ( Base ` G )
2 mulgnnsubcl.t 
 |-  .x. = ( .g ` G )
3 mulgnnsubcl.p 
 |-  .+ = ( +g ` G )
4 mulgnnsubcl.g 
 |-  ( ph -> G e. V )
5 mulgnnsubcl.s 
 |-  ( ph -> S C_ B )
6 mulgnnsubcl.c 
 |-  ( ( ph /\ x e. S /\ y e. S ) -> ( x .+ y ) e. S )
7 simp2 
 |-  ( ( ph /\ N e. NN /\ X e. S ) -> N e. NN )
8 5 3ad2ant1 
 |-  ( ( ph /\ N e. NN /\ X e. S ) -> S C_ B )
9 simp3 
 |-  ( ( ph /\ N e. NN /\ X e. S ) -> X e. S )
10 8 9 sseldd 
 |-  ( ( ph /\ N e. NN /\ X e. S ) -> X e. B )
11 eqid 
 |-  seq 1 ( .+ , ( NN X. { X } ) ) = seq 1 ( .+ , ( NN X. { X } ) )
12 1 3 2 11 mulgnn 
 |-  ( ( N e. NN /\ X e. B ) -> ( N .x. X ) = ( seq 1 ( .+ , ( NN X. { X } ) ) ` N ) )
13 7 10 12 syl2anc 
 |-  ( ( ph /\ N e. NN /\ X e. S ) -> ( N .x. X ) = ( seq 1 ( .+ , ( NN X. { X } ) ) ` N ) )
14 nnuz 
 |-  NN = ( ZZ>= ` 1 )
15 7 14 eleqtrdi 
 |-  ( ( ph /\ N e. NN /\ X e. S ) -> N e. ( ZZ>= ` 1 ) )
16 elfznn 
 |-  ( x e. ( 1 ... N ) -> x e. NN )
17 fvconst2g 
 |-  ( ( X e. S /\ x e. NN ) -> ( ( NN X. { X } ) ` x ) = X )
18 9 16 17 syl2an 
 |-  ( ( ( ph /\ N e. NN /\ X e. S ) /\ x e. ( 1 ... N ) ) -> ( ( NN X. { X } ) ` x ) = X )
19 simpl3 
 |-  ( ( ( ph /\ N e. NN /\ X e. S ) /\ x e. ( 1 ... N ) ) -> X e. S )
20 18 19 eqeltrd 
 |-  ( ( ( ph /\ N e. NN /\ X e. S ) /\ x e. ( 1 ... N ) ) -> ( ( NN X. { X } ) ` x ) e. S )
21 6 3expb 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )
22 21 3ad2antl1 
 |-  ( ( ( ph /\ N e. NN /\ X e. S ) /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )
23 15 20 22 seqcl 
 |-  ( ( ph /\ N e. NN /\ X e. S ) -> ( seq 1 ( .+ , ( NN X. { X } ) ) ` N ) e. S )
24 13 23 eqeltrd 
 |-  ( ( ph /\ N e. NN /\ X e. S ) -> ( N .x. X ) e. S )