Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  mulgsubcl Structured version   Unicode version

Theorem mulgsubcl 14906
 Description: Closure of the group multiple (exponentiation) operation in a subgroup. (Contributed by Mario Carneiro, 10-Jan-2015.)
Hypotheses
Ref Expression
mulgnnsubcl.b
mulgnnsubcl.t .g
mulgnnsubcl.p
mulgnnsubcl.g
mulgnnsubcl.s
mulgnnsubcl.c
mulgnn0subcl.z
mulgnn0subcl.c
mulgsubcl.i
mulgsubcl.c
Assertion
Ref Expression
mulgsubcl
Distinct variable groups:   ,,   ,,   ,,   ,   ,,   ,,   ,,   ,   ,,
Allowed substitution hints:   ()   ()   (,)   (,)

Proof of Theorem mulgsubcl
StepHypRef Expression
1 mulgnnsubcl.b . . . . . 6
2 mulgnnsubcl.t . . . . . 6 .g
3 mulgnnsubcl.p . . . . . 6
4 mulgnnsubcl.g . . . . . 6
5 mulgnnsubcl.s . . . . . 6
6 mulgnnsubcl.c . . . . . 6
7 mulgnn0subcl.z . . . . . 6
8 mulgnn0subcl.c . . . . . 6
91, 2, 3, 4, 5, 6, 7, 8mulgnn0subcl 14905 . . . . 5
1093expa 1154 . . . 4
1110an32s 781 . . 3
13 simp2 959 . . . . . . . . 9
1413adantr 453 . . . . . . . 8
1514zcnd 10378 . . . . . . 7
1615negnegd 9404 . . . . . 6
1716oveq1d 6098 . . . . 5
18 id 21 . . . . . 6
1953ad2ant1 979 . . . . . . 7
20 simp3 960 . . . . . . 7
2119, 20sseldd 3351 . . . . . 6
22 mulgsubcl.i . . . . . . 7
231, 2, 22mulgnegnn 14902 . . . . . 6
2418, 21, 23syl2anr 466 . . . . 5
2517, 24eqtr3d 2472 . . . 4
261, 2, 3, 4, 5, 6mulgnnsubcl 14904 . . . . . . . 8
27263expa 1154 . . . . . . 7
2827an32s 781 . . . . . 6
29283adantl2 1115 . . . . 5
30 mulgsubcl.c . . . . . . . 8
3130ralrimiva 2791 . . . . . . 7
32313ad2ant1 979 . . . . . 6
3332adantr 453 . . . . 5
34 fveq2 5730 . . . . . . 7
3534eleq1d 2504 . . . . . 6
3635rspcv 3050 . . . . 5
3729, 33, 36sylc 59 . . . 4
3825, 37eqeltrd 2512 . . 3