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

Theorem mulgnn0subcl 16783
 Description: Closure of the group multiple (exponentiation) operation in a submonoid. (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
Assertion
Ref Expression
mulgnn0subcl
Distinct variable groups:   ,,   ,,   ,,   ,,   ,,   ,,   ,   ,,
Allowed substitution hints:   ()   (,)   (,)

Proof of Theorem mulgnn0subcl
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
71, 2, 3, 4, 5, 6mulgnnsubcl 16782 . . . . 5
873expa 1209 . . . 4
98an32s 814 . . 3
11 oveq1 6302 . . . 4
1253ad2ant1 1030 . . . . . 6
13 simp3 1011 . . . . . 6
1412, 13sseldd 3435 . . . . 5
15 mulgnn0subcl.z . . . . . 6
161, 15, 2mulg0 16775 . . . . 5
1714, 16syl 17 . . . 4
1811, 17sylan9eqr 2509 . . 3
19 mulgnn0subcl.c . . . . 5
20193ad2ant1 1030 . . . 4