Theorem mulgnegnn

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

	Ref	Expression
Hypotheses	mulg1.b	$$⊢B={\mathrm{Base}}_G$$
	mulg1.m	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
	mulgnegnn.i	$$⊢I={inv}_g\left(G\right)$$
Assertion	mulgnegnn	$$⊢\left(N\in \mathbb{N}\wedge X\in B\right)\to \mathrm{-<mi\; mathcolor="\#808">N</mi>}\underset{\dot{}}{·}X=I\left(N\underset{\dot{}}{·}X\right)$$

Proof

Step	Hyp	Ref	Expression
1		mulg1.b	$$⊢B={\mathrm{Base}}_G$$
2		mulg1.m	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
3		mulgnegnn.i	$$⊢I={inv}_g\left(G\right)$$
4		nncn	$$⊢N\in \mathbb{N}\to N\in ℂ$$
5	4	negnegd	$$⊢N\in \mathbb{N}\to -\mathrm{-<mi\; mathcolor="\#808">N</mi>}=N$$
6	5	adantr	$$⊢\left(N\in \mathbb{N}\wedge X\in B\right)\to -\mathrm{-<mi\; mathcolor="\#808">N</mi>}=N$$
7	6	fveq2d	$$⊢\left(N\in \mathbb{N}\wedge X\in B\right)\to seq1\left({+}_G,\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(-\mathrm{-<mi\; mathcolor="\#808">N</mi>}\right)=seq1\left({+}_G,\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(N\right)$$
8	7	fveq2d	$$⊢\left(N\in \mathbb{N}\wedge X\in B\right)\to I\left(seq1\left({+}_G,\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(-\mathrm{-<mi\; mathcolor="\#808">N</mi>}\right)\right)=I\left(seq1\left({+}_G,\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(N\right)\right)$$
9		nnnegz	$$⊢N\in \mathbb{N}\to -N\in \mathbb{Z}$$
10		eqid	$$⊢{+}_G={+}_G$$
11		eqid	$$⊢0_G=0_G$$
12		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)$$
13	1 10 11 3 2 12	mulgval	$$⊢\left(-N\in \mathbb{Z}\wedge X\in B\right)\to \mathrm{-<mi\; mathcolor="\#808">N</mi>}\underset{\dot{}}{·}X=if\left(-N=0,0_G,if\left(0<-N,seq1\left({+}_G,\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(-N\right),I\left(seq1\left({+}_G,\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(-\mathrm{-<mi\; mathcolor="\#808">N</mi>}\right)\right)\right)\right)$$
14	9 13	sylan	$$⊢\left(N\in \mathbb{N}\wedge X\in B\right)\to \mathrm{-<mi\; mathcolor="\#808">N</mi>}\underset{\dot{}}{·}X=if\left(-N=0,0_G,if\left(0<-N,seq1\left({+}_G,\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(-N\right),I\left(seq1\left({+}_G,\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(-\mathrm{-<mi\; mathcolor="\#808">N</mi>}\right)\right)\right)\right)$$
15		nnne0	$$⊢N\in \mathbb{N}\to N\ne 0$$
16		negeq0	$$⊢N\in ℂ\to \left(N=0\leftrightarrow -N=0\right)$$
17	16	necon3abid	$$⊢N\in ℂ\to \left(N\ne 0\leftrightarrow \neg -N=0\right)$$
18	4 17	syl	$$⊢N\in \mathbb{N}\to \left(N\ne 0\leftrightarrow \neg -N=0\right)$$
19	15 18	mpbid	$$⊢N\in \mathbb{N}\to \neg -N=0$$
20	19	iffalsed	$$⊢N\in \mathbb{N}\to if\left(-N=0,0_G,if\left(0<-N,seq1\left({+}_G,\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(-N\right),I\left(seq1\left({+}_G,\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(-\mathrm{-<mi\; mathcolor="\#808">N</mi>}\right)\right)\right)\right)=if\left(0<-N,seq1\left({+}_G,\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(-N\right),I\left(seq1\left({+}_G,\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(-\mathrm{-<mi\; mathcolor="\#808">N</mi>}\right)\right)\right)$$
21		nnre	$$⊢N\in \mathbb{N}\to N\in ℝ$$
22	21	renegcld	$$⊢N\in \mathbb{N}\to -N\in ℝ$$
23		nngt0	$$⊢N\in \mathbb{N}\to 0<N$$
24	21	lt0neg2d	$$⊢N\in \mathbb{N}\to \left(0<N\leftrightarrow -N<0\right)$$
25	23 24	mpbid	$$⊢N\in \mathbb{N}\to -N<0$$
26		0re	$$⊢0\in ℝ$$
27		ltnsym	$$⊢\left(-N\in ℝ\wedge 0\in ℝ\right)\to \left(-N<0\to \neg 0<-N\right)$$
28	26 27	mpan2	$$⊢-N\in ℝ\to \left(-N<0\to \neg 0<-N\right)$$
29	22 25 28	sylc	$$⊢N\in \mathbb{N}\to \neg 0<-N$$
30	29	iffalsed	$$⊢N\in \mathbb{N}\to if\left(0<-N,seq1\left({+}_G,\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(-N\right),I\left(seq1\left({+}_G,\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(-\mathrm{-<mi\; mathcolor="\#808">N</mi>}\right)\right)\right)=I\left(seq1\left({+}_G,\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(-\mathrm{-<mi\; mathcolor="\#808">N</mi>}\right)\right)$$
31	20 30	eqtrd	$$⊢N\in \mathbb{N}\to if\left(-N=0,0_G,if\left(0<-N,seq1\left({+}_G,\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(-N\right),I\left(seq1\left({+}_G,\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(-\mathrm{-<mi\; mathcolor="\#808">N</mi>}\right)\right)\right)\right)=I\left(seq1\left({+}_G,\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(-\mathrm{-<mi\; mathcolor="\#808">N</mi>}\right)\right)$$
32	31	adantr	$$⊢\left(N\in \mathbb{N}\wedge X\in B\right)\to if\left(-N=0,0_G,if\left(0<-N,seq1\left({+}_G,\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(-N\right),I\left(seq1\left({+}_G,\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(-\mathrm{-<mi\; mathcolor="\#808">N</mi>}\right)\right)\right)\right)=I\left(seq1\left({+}_G,\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(-\mathrm{-<mi\; mathcolor="\#808">N</mi>}\right)\right)$$
33	14 32	eqtrd	$$⊢\left(N\in \mathbb{N}\wedge X\in B\right)\to \mathrm{-<mi\; mathcolor="\#808">N</mi>}\underset{\dot{}}{·}X=I\left(seq1\left({+}_G,\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(-\mathrm{-<mi\; mathcolor="\#808">N</mi>}\right)\right)$$
34	1 10 2 12	mulgnn	$$⊢\left(N\in \mathbb{N}\wedge X\in B\right)\to N\underset{\dot{}}{·}X=seq1\left({+}_G,\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(N\right)$$
35	34	fveq2d	$$⊢\left(N\in \mathbb{N}\wedge X\in B\right)\to I\left(N\underset{\dot{}}{·}X\right)=I\left(seq1\left({+}_G,\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(N\right)\right)$$
36	8 33 35	3eqtr4d	$$⊢\left(N\in \mathbb{N}\wedge X\in B\right)\to \mathrm{-<mi\; mathcolor="\#808">N</mi>}\underset{\dot{}}{·}X=I\left(N\underset{\dot{}}{·}X\right)$$