Theorem mulgnn

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

	Ref	Expression
Hypotheses	mulgnn.b	$$⊢B={\mathrm{Base}}_G$$
	mulgnn.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	mulgnn.t	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
	mulgnn.s	$$⊢S=seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{X\right\}\right)\right)$$
Assertion	mulgnn	$$⊢\left(N\in \mathbb{N}\wedge X\in B\right)\to N\underset{\dot{}}{·}X=S\left(N\right)$$

Proof

Step	Hyp	Ref	Expression
1		mulgnn.b	$$⊢B={\mathrm{Base}}_G$$
2		mulgnn.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		mulgnn.t	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
4		mulgnn.s	$$⊢S=seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{X\right\}\right)\right)$$
5		nnz	$$⊢N\in \mathbb{N}\to N\in \mathbb{Z}$$
6		eqid	$$⊢0_G=0_G$$
7		eqid	$$⊢{inv}_g\left(G\right)={inv}_g\left(G\right)$$
8	1 2 6 7 3 4	mulgval	$$⊢\left(N\in \mathbb{Z}\wedge X\in B\right)\to N\underset{\dot{}}{·}X=if\left(N=0,0_G,if\left(0<N,S\left(N\right),{inv}_g\left(G\right)\left(S\left(-N\right)\right)\right)\right)$$
9	5 8	sylan	$$⊢\left(N\in \mathbb{N}\wedge X\in B\right)\to N\underset{\dot{}}{·}X=if\left(N=0,0_G,if\left(0<N,S\left(N\right),{inv}_g\left(G\right)\left(S\left(-N\right)\right)\right)\right)$$
10		nnne0	$$⊢N\in \mathbb{N}\to N\ne 0$$
11	10	neneqd	$$⊢N\in \mathbb{N}\to \neg N=0$$
12	11	iffalsed	$$⊢N\in \mathbb{N}\to if\left(N=0,0_G,if\left(0<N,S\left(N\right),{inv}_g\left(G\right)\left(S\left(-N\right)\right)\right)\right)=if\left(0<N,S\left(N\right),{inv}_g\left(G\right)\left(S\left(-N\right)\right)\right)$$
13		nngt0	$$⊢N\in \mathbb{N}\to 0<N$$
14	13	iftrued	$$⊢N\in \mathbb{N}\to if\left(0<N,S\left(N\right),{inv}_g\left(G\right)\left(S\left(-N\right)\right)\right)=S\left(N\right)$$
15	12 14	eqtrd	$$⊢N\in \mathbb{N}\to if\left(N=0,0_G,if\left(0<N,S\left(N\right),{inv}_g\left(G\right)\left(S\left(-N\right)\right)\right)\right)=S\left(N\right)$$
16	15	adantr	$$⊢\left(N\in \mathbb{N}\wedge X\in B\right)\to if\left(N=0,0_G,if\left(0<N,S\left(N\right),{inv}_g\left(G\right)\left(S\left(-N\right)\right)\right)\right)=S\left(N\right)$$
17	9 16	eqtrd	$$⊢\left(N\in \mathbb{N}\wedge X\in B\right)\to N\underset{\dot{}}{·}X=S\left(N\right)$$