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

Metamath Proof Explorer

Theorem subgmulgcl

Description: Closure of the group multiple (exponentiation) operation in a subgroup. (Contributed by Mario Carneiro, 13-Jan-2015)

Ref Expression
Hypothesis subgmulgcl.t ⊢ · = ( .g ‘ 𝐺 )
Assertion subgmulgcl ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) → ( 𝑁 · 𝑋 ) ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 subgmulgcl.t ⊢ · = ( .g ‘ 𝐺 )
2 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
3 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
4 subgrcl ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
5 2 subgss ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
6 3 subgcl ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 )
7 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
8 7 subg0cl ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( 0g ‘ 𝐺 ) ∈ 𝑆 )
9 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
10 9 subginvcl ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑆 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝑆 )
11 2 1 3 4 5 6 7 8 9 10 mulgsubcl ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) → ( 𝑁 · 𝑋 ) ∈ 𝑆 )