This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database BASIC ALGEBRAIC STRUCTURES Groups Group multiple operation mulgnncl
Description: Closure of the group multiple (exponentiation) operation for a positive
multiplier in a magma. (Contributed by Mario Carneiro , 11-Dec-2014)
(Revised by AV , 29-Aug-2021)
Ref
Expression
Hypotheses
mulgnncl.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
mulgnncl.t ⊢ · = ( .g ‘ 𝐺 )
Assertion
mulgnncl ⊢ ( ( 𝐺 ∈ Mgm ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 · 𝑋 ) ∈ 𝐵 )
Proof
Step
Hyp
Ref
Expression
1
mulgnncl.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2
mulgnncl.t ⊢ · = ( .g ‘ 𝐺 )
3
eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
4
id ⊢ ( 𝐺 ∈ Mgm → 𝐺 ∈ Mgm )
5
ssidd ⊢ ( 𝐺 ∈ Mgm → 𝐵 ⊆ 𝐵 )
6
1 3
mgmcl ⊢ ( ( 𝐺 ∈ Mgm ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝐵 )
7
1 2 3 4 5 6
mulgnnsubcl ⊢ ( ( 𝐺 ∈ Mgm ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 · 𝑋 ) ∈ 𝐵 )