This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 · 𝑋 ) ∈ 𝐵 )