Metamath Proof Explorer


Theorem mulg0

Description: Group multiple (exponentiation) operation at zero. (Contributed by Mario Carneiro, 11-Dec-2014)

Ref Expression
Hypotheses mulg0.b B=BaseG
mulg0.o 0˙=0G
mulg0.t ·˙=G
Assertion mulg0 XB0·˙X=0˙

Proof

Step Hyp Ref Expression
1 mulg0.b B=BaseG
2 mulg0.o 0˙=0G
3 mulg0.t ·˙=G
4 0z 0
5 eqid +G=+G
6 eqid invgG=invgG
7 eqid seq1+G×X=seq1+G×X
8 1 5 2 6 3 7 mulgval 0XB0·˙X=if0=00˙if0<0seq1+G×X0invgGseq1+G×X0
9 eqid 0=0
10 9 iftruei if0=00˙if0<0seq1+G×X0invgGseq1+G×X0=0˙
11 8 10 eqtrdi 0XB0·˙X=0˙
12 4 11 mpan XB0·˙X=0˙