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

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

Proof of Theorem mulgnnsubcl
StepHypRef Expression
1 simp2 958 . . 3
2 mulgnnsubcl.s . . . . 5
323ad2ant1 978 . . . 4
4 simp3 959 . . . 4
53, 4sseldd 3341 . . 3
6 mulgnnsubcl.b . . . 4
7 mulgnnsubcl.p . . . 4
8 mulgnnsubcl.t . . . 4 .g
9 eqid 2435 . . . 4
106, 7, 8, 9mulgnn 14888 . . 3
111, 5, 10syl2anc 643 . 2
12 nnuz 10513 . . . 4
131, 12syl6eleq 2525 . . 3
14 elfznn 11072 . . . . 5
15 fvconst2g 5937 . . . . 5
164, 14, 15syl2an 464 . . . 4
17 simpl3 962 . . . 4
1816, 17eqeltrd 2509 . . 3
19 mulgnnsubcl.c . . . . 5
20193expb 1154 . . . 4