This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mulgnn0subcl

Description: Closure of the group multiple (exponentiation) operation in a submonoid. (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 )
Assertion mulgnn0subcl 
|- ( ( ph /\ N e. NN0 /\ 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 1 2 3 4 5 6 mulgnnsubcl 
 |-  ( ( ph /\ N e. NN /\ X e. S ) -> ( N .x. X ) e. S )
10 9 3expa 
 |-  ( ( ( ph /\ N e. NN ) /\ X e. S ) -> ( N .x. X ) e. S )
11 10 an32s 
 |-  ( ( ( ph /\ X e. S ) /\ N e. NN ) -> ( N .x. X ) e. S )
12 11 3adantl2 
 |-  ( ( ( ph /\ N e. NN0 /\ X e. S ) /\ N e. NN ) -> ( N .x. X ) e. S )
13 oveq1 
 |-  ( N = 0 -> ( N .x. X ) = ( 0 .x. X ) )
14 5 3ad2ant1 
 |-  ( ( ph /\ N e. NN0 /\ X e. S ) -> S C_ B )
15 simp3 
 |-  ( ( ph /\ N e. NN0 /\ X e. S ) -> X e. S )
16 14 15 sseldd 
 |-  ( ( ph /\ N e. NN0 /\ X e. S ) -> X e. B )
17 1 7 2 mulg0 
 |-  ( X e. B -> ( 0 .x. X ) = .0. )
18 16 17 syl 
 |-  ( ( ph /\ N e. NN0 /\ X e. S ) -> ( 0 .x. X ) = .0. )
19 13 18 sylan9eqr 
 |-  ( ( ( ph /\ N e. NN0 /\ X e. S ) /\ N = 0 ) -> ( N .x. X ) = .0. )
20 8 3ad2ant1 
 |-  ( ( ph /\ N e. NN0 /\ X e. S ) -> .0. e. S )
21 20 adantr 
 |-  ( ( ( ph /\ N e. NN0 /\ X e. S ) /\ N = 0 ) -> .0. e. S )
22 19 21 eqeltrd 
 |-  ( ( ( ph /\ N e. NN0 /\ X e. S ) /\ N = 0 ) -> ( N .x. X ) e. S )
23 simp2 
 |-  ( ( ph /\ N e. NN0 /\ X e. S ) -> N e. NN0 )
24 elnn0 
 |-  ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
25 23 24 sylib 
 |-  ( ( ph /\ N e. NN0 /\ X e. S ) -> ( N e. NN \/ N = 0 ) )
26 12 22 25 mpjaodan 
 |-  ( ( ph /\ N e. NN0 /\ X e. S ) -> ( N .x. X ) e. S )