Metamath Proof Explorer


Theorem mulgcl

Description: Closure of the group multiple (exponentiation) operation. (Contributed by Mario Carneiro, 11-Dec-2014)

Ref Expression
Hypotheses mulgnncl.b โŠข ๐ต = ( Base โ€˜ ๐บ )
mulgnncl.t โŠข ยท = ( .g โ€˜ ๐บ )
Assertion mulgcl ( ( ๐บ โˆˆ Grp โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต ) โ†’ ( ๐‘ ยท ๐‘‹ ) โˆˆ ๐ต )

Proof

Step Hyp Ref Expression
1 mulgnncl.b โŠข ๐ต = ( Base โ€˜ ๐บ )
2 mulgnncl.t โŠข ยท = ( .g โ€˜ ๐บ )
3 eqid โŠข ( +g โ€˜ ๐บ ) = ( +g โ€˜ ๐บ )
4 id โŠข ( ๐บ โˆˆ Grp โ†’ ๐บ โˆˆ Grp )
5 ssidd โŠข ( ๐บ โˆˆ Grp โ†’ ๐ต โІ ๐ต )
6 1 3 grpcl โŠข ( ( ๐บ โˆˆ Grp โˆง ๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ต ) โ†’ ( ๐‘ฅ ( +g โ€˜ ๐บ ) ๐‘ฆ ) โˆˆ ๐ต )
7 eqid โŠข ( 0g โ€˜ ๐บ ) = ( 0g โ€˜ ๐บ )
8 1 7 grpidcl โŠข ( ๐บ โˆˆ Grp โ†’ ( 0g โ€˜ ๐บ ) โˆˆ ๐ต )
9 eqid โŠข ( invg โ€˜ ๐บ ) = ( invg โ€˜ ๐บ )
10 1 9 grpinvcl โŠข ( ( ๐บ โˆˆ Grp โˆง ๐‘ฅ โˆˆ ๐ต ) โ†’ ( ( invg โ€˜ ๐บ ) โ€˜ ๐‘ฅ ) โˆˆ ๐ต )
11 1 2 3 4 5 6 7 8 9 10 mulgsubcl โŠข ( ( ๐บ โˆˆ Grp โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต ) โ†’ ( ๐‘ ยท ๐‘‹ ) โˆˆ ๐ต )