Metamath Proof Explorer

Theorem mulgnnsubcl

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

Ref Expression
Hypotheses mulgnnsubcl.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
mulgnnsubcl.t ⊢ · = ( .g ‘ 𝐺 )
mulgnnsubcl.p ⊢ + = ( +g ‘ 𝐺 )
mulgnnsubcl.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
mulgnnsubcl.s ⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
mulgnnsubcl.c ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
Assertion mulgnnsubcl ( ( 𝜑 ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝑆 ) → ( 𝑁 · 𝑋 ) ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 mulgnnsubcl.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 mulgnnsubcl.t ⊢ · = ( .g ‘ 𝐺 )
3 mulgnnsubcl.p ⊢ + = ( +g ‘ 𝐺 )
4 mulgnnsubcl.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
5 mulgnnsubcl.s ⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
6 mulgnnsubcl.c ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
7 simp2 ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝑆 ) → 𝑁 ∈ ℕ )
8 5 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝑆 ) → 𝑆 ⊆ 𝐵 )
9 simp3 ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝑆 ) → 𝑋 ∈ 𝑆 )
10 8 9 sseldd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝑆 ) → 𝑋 ∈ 𝐵 )
11 eqid ⊢ seq 1 ( + , ( ℕ × { 𝑋 } ) ) = seq 1 ( + , ( ℕ × { 𝑋 } ) )
12 1 3 2 11 mulgnn ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 · 𝑋 ) = ( seq 1 ( + , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) )
13 7 10 12 syl2anc ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝑆 ) → ( 𝑁 · 𝑋 ) = ( seq 1 ( + , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) )
14 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
15 7 14 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝑆 ) → 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
16 elfznn ⊢ ( 𝑥 ∈ ( 1 ... 𝑁 ) → 𝑥 ∈ ℕ )
17 fvconst2g ⊢ ( ( 𝑋 ∈ 𝑆 ∧ 𝑥 ∈ ℕ ) → ( ( ℕ × { 𝑋 } ) ‘ 𝑥 ) = 𝑋 )
18 9 16 17 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) → ( ( ℕ × { 𝑋 } ) ‘ 𝑥 ) = 𝑋 )
19 simpl3 ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) → 𝑋 ∈ 𝑆 )
20 18 19 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) → ( ( ℕ × { 𝑋 } ) ‘ 𝑥 ) ∈ 𝑆 )
21 6 3expb ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
22 21 3ad2antl1 ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
23 15 20 22 seqcl ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝑆 ) → ( seq 1 ( + , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) ∈ 𝑆 )
24 13 23 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝑆 ) → ( 𝑁 · 𝑋 ) ∈ 𝑆 )