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 B = Base G
mulgnn0p1.t · ˙ = G
mulgnn0p1.p + ˙ = + G
Assertion mulgnn0p1 G Mnd N 0 X B N + 1 · ˙ X = N · ˙ X + ˙ X

Proof

Step Hyp Ref Expression
1 mulgnn0p1.b B = Base G
2 mulgnn0p1.t · ˙ = G
3 mulgnn0p1.p + ˙ = + G
4 simpr G Mnd N 0 X B N N
5 simpl3 G Mnd N 0 X B N X B
6 1 2 3 mulgnnp1 N X B N + 1 · ˙ X = N · ˙ X + ˙ X
7 4 5 6 syl2anc G Mnd N 0 X B N N + 1 · ˙ X = N · ˙ X + ˙ X
8 eqid 0 G = 0 G
9 1 3 8 mndlid G Mnd X B 0 G + ˙ X = X
10 1 8 2 mulg0 X B 0 · ˙ X = 0 G
11 10 adantl G Mnd X B 0 · ˙ X = 0 G
12 11 oveq1d G Mnd X B 0 · ˙ X + ˙ X = 0 G + ˙ X
13 1 2 mulg1 X B 1 · ˙ X = X
14 13 adantl G Mnd X B 1 · ˙ X = X
15 9 12 14 3eqtr4rd G Mnd X B 1 · ˙ X = 0 · ˙ X + ˙ X
16 15 3adant2 G Mnd N 0 X B 1 · ˙ X = 0 · ˙ X + ˙ X
17 oveq1 N = 0 N + 1 = 0 + 1
18 1e0p1 1 = 0 + 1
19 17 18 eqtr4di N = 0 N + 1 = 1
20 19 oveq1d N = 0 N + 1 · ˙ X = 1 · ˙ X
21 oveq1 N = 0 N · ˙ X = 0 · ˙ X
22 21 oveq1d N = 0 N · ˙ X + ˙ X = 0 · ˙ X + ˙ X
23 20 22 eqeq12d N = 0 N + 1 · ˙ X = N · ˙ X + ˙ X 1 · ˙ X = 0 · ˙ X + ˙ X
24 16 23 syl5ibrcom G Mnd N 0 X B N = 0 N + 1 · ˙ X = N · ˙ X + ˙ X
25 24 imp G Mnd N 0 X B N = 0 N + 1 · ˙ X = N · ˙ X + ˙ X
26 simp2 G Mnd N 0 X B N 0
27 elnn0 N 0 N N = 0
28 26 27 sylib G Mnd N 0 X B N N = 0
29 7 25 28 mpjaodan G Mnd N 0 X B N + 1 · ˙ X = N · ˙ X + ˙ X