Metamath Proof Explorer

Theorem mulgsubcl

Description: Closure of the group multiple (exponentiation) operation in a subgroup. (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 )
mulgnn0subcl.z 
|- .0. = ( 0g ` G )
mulgnn0subcl.c 
|- ( ph -> .0. e. S )
mulgsubcl.i 
|- I = ( invg ` G )
mulgsubcl.c 
|- ( ( ph /\ x e. S ) -> ( I ` x ) e. S )
Assertion mulgsubcl 
|- ( ( ph /\ N e. ZZ /\ 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 mulgnn0subcl.z 
 |-  .0. = ( 0g ` G )
8 mulgnn0subcl.c 
 |-  ( ph -> .0. e. S )
9 mulgsubcl.i 
 |-  I = ( invg ` G )
10 mulgsubcl.c 
 |-  ( ( ph /\ x e. S ) -> ( I ` x ) e. S )
11 1 2 3 4 5 6 7 8 mulgnn0subcl 
 |-  ( ( ph /\ N e. NN0 /\ X e. S ) -> ( N .x. X ) e. S )
12 11 3expa 
 |-  ( ( ( ph /\ N e. NN0 ) /\ X e. S ) -> ( N .x. X ) e. S )
13 12 an32s 
 |-  ( ( ( ph /\ X e. S ) /\ N e. NN0 ) -> ( N .x. X ) e. S )
14 13 3adantl2 
 |-  ( ( ( ph /\ N e. ZZ /\ X e. S ) /\ N e. NN0 ) -> ( N .x. X ) e. S )
15 simp2 
 |-  ( ( ph /\ N e. ZZ /\ X e. S ) -> N e. ZZ )
16 15 adantr 
 |-  ( ( ( ph /\ N e. ZZ /\ X e. S ) /\ -u N e. NN ) -> N e. ZZ )
17 16 zcnd 
 |-  ( ( ( ph /\ N e. ZZ /\ X e. S ) /\ -u N e. NN ) -> N e. CC )
18 17 negnegd 
 |-  ( ( ( ph /\ N e. ZZ /\ X e. S ) /\ -u N e. NN ) -> -u -u N = N )
19 18 oveq1d 
 |-  ( ( ( ph /\ N e. ZZ /\ X e. S ) /\ -u N e. NN ) -> ( -u -u N .x. X ) = ( N .x. X ) )
20 id 
 |-  ( -u N e. NN -> -u N e. NN )
21 5 3ad2ant1 
 |-  ( ( ph /\ N e. ZZ /\ X e. S ) -> S C_ B )
22 simp3 
 |-  ( ( ph /\ N e. ZZ /\ X e. S ) -> X e. S )
23 21 22 sseldd 
 |-  ( ( ph /\ N e. ZZ /\ X e. S ) -> X e. B )
24 1 2 9 mulgnegnn 
 |-  ( ( -u N e. NN /\ X e. B ) -> ( -u -u N .x. X ) = ( I ` ( -u N .x. X ) ) )
25 20 23 24 syl2anr 
 |-  ( ( ( ph /\ N e. ZZ /\ X e. S ) /\ -u N e. NN ) -> ( -u -u N .x. X ) = ( I ` ( -u N .x. X ) ) )
26 19 25 eqtr3d 
 |-  ( ( ( ph /\ N e. ZZ /\ X e. S ) /\ -u N e. NN ) -> ( N .x. X ) = ( I ` ( -u N .x. X ) ) )
27 fveq2 
 |-  ( x = ( -u N .x. X ) -> ( I ` x ) = ( I ` ( -u N .x. X ) ) )
28 27 eleq1d 
 |-  ( x = ( -u N .x. X ) -> ( ( I ` x ) e. S <-> ( I ` ( -u N .x. X ) ) e. S ) )
29 10 ralrimiva 
 |-  ( ph -> A. x e. S ( I ` x ) e. S )
30 29 3ad2ant1 
 |-  ( ( ph /\ N e. ZZ /\ X e. S ) -> A. x e. S ( I ` x ) e. S )
31 30 adantr 
 |-  ( ( ( ph /\ N e. ZZ /\ X e. S ) /\ -u N e. NN ) -> A. x e. S ( I ` x ) e. S )
32 1 2 3 4 5 6 mulgnnsubcl 
 |-  ( ( ph /\ -u N e. NN /\ X e. S ) -> ( -u N .x. X ) e. S )
33 32 3expa 
 |-  ( ( ( ph /\ -u N e. NN ) /\ X e. S ) -> ( -u N .x. X ) e. S )
34 33 an32s 
 |-  ( ( ( ph /\ X e. S ) /\ -u N e. NN ) -> ( -u N .x. X ) e. S )
35 34 3adantl2 
 |-  ( ( ( ph /\ N e. ZZ /\ X e. S ) /\ -u N e. NN ) -> ( -u N .x. X ) e. S )
36 28 31 35 rspcdva 
 |-  ( ( ( ph /\ N e. ZZ /\ X e. S ) /\ -u N e. NN ) -> ( I ` ( -u N .x. X ) ) e. S )
37 26 36 eqeltrd 
 |-  ( ( ( ph /\ N e. ZZ /\ X e. S ) /\ -u N e. NN ) -> ( N .x. X ) e. S )
38 37 adantrl 
 |-  ( ( ( ph /\ N e. ZZ /\ X e. S ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( N .x. X ) e. S )
39 elznn0nn 
 |-  ( N e. ZZ <-> ( N e. NN0 \/ ( N e. RR /\ -u N e. NN ) ) )
40 15 39 sylib 
 |-  ( ( ph /\ N e. ZZ /\ X e. S ) -> ( N e. NN0 \/ ( N e. RR /\ -u N e. NN ) ) )
41 14 38 40 mpjaodan 
 |-  ( ( ph /\ N e. ZZ /\ X e. S ) -> ( N .x. X ) e. S )