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

Metamath Proof Explorer

Theorem mulgnn0subcl

Description: Closure of the group multiple (exponentiation) operation in a submonoid. (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 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
mulgnn0subcl.z ⊢ 0 = ( 0g ‘ 𝐺 )
mulgnn0subcl.c ⊢ ( 𝜑 → 0 ∈ 𝑆 )
Assertion mulgnn0subcl ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) → ( 𝑁 · 𝑋 ) ∈ 𝑆 )

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 mulgnn0subcl.z ⊢ 0 = ( 0g ‘ 𝐺 )
8 mulgnn0subcl.c ⊢ ( 𝜑 → 0 ∈ 𝑆 )
9 1 2 3 4 5 6 mulgnnsubcl ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝑆 ) → ( 𝑁 · 𝑋 ) ∈ 𝑆 )
10 9 3expa ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) ∧ 𝑋 ∈ 𝑆 ) → ( 𝑁 · 𝑋 ) ∈ 𝑆 )
11 10 an32s ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑁 ∈ ℕ ) → ( 𝑁 · 𝑋 ) ∈ 𝑆 )
12 11 3adantl2 ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑁 ∈ ℕ ) → ( 𝑁 · 𝑋 ) ∈ 𝑆 )
13 oveq1 ⊢ ( 𝑁 = 0 → ( 𝑁 · 𝑋 ) = ( 0 · 𝑋 ) )
14 5 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) → 𝑆 ⊆ 𝐵 )
15 simp3 ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) → 𝑋 ∈ 𝑆 )
16 14 15 sseldd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) → 𝑋 ∈ 𝐵 )
17 1 7 2 mulg0 ⊢ ( 𝑋 ∈ 𝐵 → ( 0 · 𝑋 ) = 0 )
18 16 17 syl ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) → ( 0 · 𝑋 ) = 0 )
19 13 18 sylan9eqr ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑁 = 0 ) → ( 𝑁 · 𝑋 ) = 0 )
20 8 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) → 0 ∈ 𝑆 )
21 20 adantr ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑁 = 0 ) → 0 ∈ 𝑆 )
22 19 21 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑁 = 0 ) → ( 𝑁 · 𝑋 ) ∈ 𝑆 )
23 simp2 ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) → 𝑁 ∈ ℕ0 )
24 elnn0 ⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
25 23 24 sylib ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) → ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
26 12 22 25 mpjaodan ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) → ( 𝑁 · 𝑋 ) ∈ 𝑆 )