Theorem mulg0

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

	Ref	Expression
Hypotheses	mulg0.b	$$⊢B={\mathrm{Base}}_G$$
	mulg0.o	$$⊢\underset{\dot{}}{0}=0_G$$
	mulg0.t	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
Assertion	mulg0	$$⊢X\in B\to 0\underset{\dot{}}{·}X=\underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		mulg0.b	$$⊢B={\mathrm{Base}}_G$$
2		mulg0.o	$$⊢\underset{\dot{}}{0}=0_G$$
3		mulg0.t	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
4		0z	$$⊢0\in \mathbb{Z}$$
5		eqid	$$⊢{+}_G={+}_G$$
6		eqid	$$⊢{inv}_g\left(G\right)={inv}_g\left(G\right)$$
7		eqid	$$⊢seq1\left({+}_G,\left(\mathbb{N}\times \left\{X\right\}\right)\right)=seq1\left({+}_G,\left(\mathbb{N}\times \left\{X\right\}\right)\right)$$
8	1 5 2 6 3 7	mulgval	$$⊢\left(0\in \mathbb{Z}\wedge X\in B\right)\to 0\underset{\dot{}}{·}X=if\left(0=0,\underset{\dot{}}{0},if\left(0<0,seq1\left({+}_G,\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(0\right),{inv}_g\left(G\right)\left(seq1\left({+}_G,\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(-0\right)\right)\right)\right)$$
9		eqid	$$⊢0=0$$
10	9	iftruei	$$⊢if\left(0=0,\underset{\dot{}}{0},if\left(0<0,seq1\left({+}_G,\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(0\right),{inv}_g\left(G\right)\left(seq1\left({+}_G,\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(-0\right)\right)\right)\right)=\underset{\dot{}}{0}$$
11	8 10	syl6eq	$$⊢\left(0\in \mathbb{Z}\wedge X\in B\right)\to 0\underset{\dot{}}{·}X=\underset{\dot{}}{0}$$
12	4 11	mpan	$$⊢X\in B\to 0\underset{\dot{}}{·}X=\underset{\dot{}}{0}$$