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