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

Theorem mulgnn0subcl 14893
 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 14892 . . . . 5
873expa 1153 . . . 4
98an32s 780 . . 3
11 oveq1 6080 . . . 4
1253ad2ant1 978 . . . . . 6
13 simp3 959 . . . . . 6
1412, 13sseldd 3341 . . . . 5
15 mulgnn0subcl.z . . . . . 6
161, 15, 2mulg0 14885 . . . . 5
1714, 16syl 16 . . . 4
1811, 17sylan9eqr 2489 . . 3
19 mulgnn0subcl.c . . . . 5
20193ad2ant1 978 . . . 4