Metamath Proof Explorer

Theorem mulgnn0p1

Description: Group multiple (exponentiation) operation at a successor, extended to NN0 . (Contributed by Mario Carneiro, 11-Dec-2014)

Ref Expression
Hypotheses mulgnn0p1.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
mulgnn0p1.t ⊢ · = ( .g ‘ 𝐺 )
mulgnn0p1.p ⊢ + = ( +g ‘ 𝐺 )
Assertion mulgnn0p1 ( ( 𝐺 ∈ Mnd ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑁 + 1 ) · 𝑋 ) = ( ( 𝑁 · 𝑋 ) + 𝑋 ) )

Proof

Step Hyp Ref Expression
1 mulgnn0p1.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 mulgnn0p1.t ⊢ · = ( .g ‘ 𝐺 )
3 mulgnn0p1.p ⊢ + = ( +g ‘ 𝐺 )
4 simpr ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℕ )
5 simpl3 ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ ) → 𝑋 ∈ 𝐵 )
6 1 2 3 mulgnnp1 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑁 + 1 ) · 𝑋 ) = ( ( 𝑁 · 𝑋 ) + 𝑋 ) )
7 4 5 6 syl2anc ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ ) → ( ( 𝑁 + 1 ) · 𝑋 ) = ( ( 𝑁 · 𝑋 ) + 𝑋 ) )
8 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
9 1 3 8 mndlid ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵 ) → ( ( 0g ‘ 𝐺 ) + 𝑋 ) = 𝑋 )
10 1 8 2 mulg0 ⊢ ( 𝑋 ∈ 𝐵 → ( 0 · 𝑋 ) = ( 0g ‘ 𝐺 ) )
11 10 adantl ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵 ) → ( 0 · 𝑋 ) = ( 0g ‘ 𝐺 ) )
12 11 oveq1d ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵 ) → ( ( 0 · 𝑋 ) + 𝑋 ) = ( ( 0g ‘ 𝐺 ) + 𝑋 ) )
13 1 2 mulg1 ⊢ ( 𝑋 ∈ 𝐵 → ( 1 · 𝑋 ) = 𝑋 )
14 13 adantl ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵 ) → ( 1 · 𝑋 ) = 𝑋 )
15 9 12 14 3eqtr4rd ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵 ) → ( 1 · 𝑋 ) = ( ( 0 · 𝑋 ) + 𝑋 ) )
16 15 3adant2 ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) → ( 1 · 𝑋 ) = ( ( 0 · 𝑋 ) + 𝑋 ) )
17 oveq1 ⊢ ( 𝑁 = 0 → ( 𝑁 + 1 ) = ( 0 + 1 ) )
18 1e0p1 ⊢ 1 = ( 0 + 1 )
19 17 18 eqtr4di ⊢ ( 𝑁 = 0 → ( 𝑁 + 1 ) = 1 )
20 19 oveq1d ⊢ ( 𝑁 = 0 → ( ( 𝑁 + 1 ) · 𝑋 ) = ( 1 · 𝑋 ) )
21 oveq1 ⊢ ( 𝑁 = 0 → ( 𝑁 · 𝑋 ) = ( 0 · 𝑋 ) )
22 21 oveq1d ⊢ ( 𝑁 = 0 → ( ( 𝑁 · 𝑋 ) + 𝑋 ) = ( ( 0 · 𝑋 ) + 𝑋 ) )
23 20 22 eqeq12d ⊢ ( 𝑁 = 0 → ( ( ( 𝑁 + 1 ) · 𝑋 ) = ( ( 𝑁 · 𝑋 ) + 𝑋 ) ↔ ( 1 · 𝑋 ) = ( ( 0 · 𝑋 ) + 𝑋 ) ) )
24 16 23 syl5ibrcom ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 = 0 → ( ( 𝑁 + 1 ) · 𝑋 ) = ( ( 𝑁 · 𝑋 ) + 𝑋 ) ) )
25 24 imp ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 = 0 ) → ( ( 𝑁 + 1 ) · 𝑋 ) = ( ( 𝑁 · 𝑋 ) + 𝑋 ) )
26 simp2 ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) → 𝑁 ∈ ℕ0 )
27 elnn0 ⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
28 26 27 sylib ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
29 7 25 28 mpjaodan ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑁 + 1 ) · 𝑋 ) = ( ( 𝑁 · 𝑋 ) + 𝑋 ) )