Theorem mulgval

Description: Value of the group multiple (exponentiation) operation. (Contributed by Mario Carneiro, 11-Dec-2014)

	Ref	Expression
Hypotheses	mulgval.b	$$⊢B={\mathrm{Base}}_G$$
	mulgval.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	mulgval.o	$$⊢\underset{\dot{}}{0}=0_G$$
	mulgval.i	$$⊢I={inv}_g\left(G\right)$$
	mulgval.t	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
	mulgval.s	$$⊢S=seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{X\right\}\right)\right)$$
Assertion	mulgval	$$⊢\left(N\in \mathbb{Z}\wedge X\in B\right)\to N\underset{\dot{}}{·}X=if\left(N=0,\underset{\dot{}}{0},if\left(0<N,S\left(N\right),I\left(S\left(-N\right)\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		mulgval.b	$$⊢B={\mathrm{Base}}_G$$
2		mulgval.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		mulgval.o	$$⊢\underset{\dot{}}{0}=0_G$$
4		mulgval.i	$$⊢I={inv}_g\left(G\right)$$
5		mulgval.t	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
6		mulgval.s	$$⊢S=seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{X\right\}\right)\right)$$
7		simpl	$$⊢\left(n=N\wedge x=X\right)\to n=N$$
8	7	eqeq1d	$$⊢\left(n=N\wedge x=X\right)\to \left(n=0\leftrightarrow N=0\right)$$
9	7	breq2d	$$⊢\left(n=N\wedge x=X\right)\to \left(0<n\leftrightarrow 0<N\right)$$
10		simpr	$$⊢\left(n=N\wedge x=X\right)\to x=X$$
11	10	sneqd	$$⊢\left(n=N\wedge x=X\right)\to \left\{x\right\}=\left\{X\right\}$$
12	11	xpeq2d	$$⊢\left(n=N\wedge x=X\right)\to \mathbb{N}\times \left\{x\right\}=\mathbb{N}\times \left\{X\right\}$$
13	12	seqeq3d	$$⊢\left(n=N\wedge x=X\right)\to seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)=seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{X\right\}\right)\right)$$
14	13 6	eqtr4di	$$⊢\left(n=N\wedge x=X\right)\to seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)=S$$
15	14 7	fveq12d	$$⊢\left(n=N\wedge x=X\right)\to seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n\right)=S\left(N\right)$$
16	7	negeqd	$$⊢\left(n=N\wedge x=X\right)\to -n=-N$$
17	14 16	fveq12d	$$⊢\left(n=N\wedge x=X\right)\to seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(-n\right)=S\left(-N\right)$$
18	17	fveq2d	$$⊢\left(n=N\wedge x=X\right)\to I\left(seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(-n\right)\right)=I\left(S\left(-N\right)\right)$$
19	9 15 18	ifbieq12d	$$⊢\left(n=N\wedge x=X\right)\to if\left(0<n,seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n\right),I\left(seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(-n\right)\right)\right)=if\left(0<N,S\left(N\right),I\left(S\left(-N\right)\right)\right)$$
20	8 19	ifbieq2d	$$⊢\left(n=N\wedge x=X\right)\to if\left(n=0,\underset{\dot{}}{0},if\left(0<n,seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n\right),I\left(seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(-n\right)\right)\right)\right)=if\left(N=0,\underset{\dot{}}{0},if\left(0<N,S\left(N\right),I\left(S\left(-N\right)\right)\right)\right)$$
21	1 2 3 4 5	mulgfval	$$⊢\underset{\dot{}}{·}=\left(n\in \mathbb{Z},x\in B⟼if\left(n=0,\underset{\dot{}}{0},if\left(0<n,seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n\right),I\left(seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(-n\right)\right)\right)\right)\right)$$
22	3	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
23		fvex	$$⊢S\left(N\right)\in \mathrm{V}$$
24		fvex	$$⊢I\left(S\left(-N\right)\right)\in \mathrm{V}$$
25	23 24	ifex	$$⊢if\left(0<N,S\left(N\right),I\left(S\left(-N\right)\right)\right)\in \mathrm{V}$$
26	22 25	ifex	$$⊢if\left(N=0,\underset{\dot{}}{0},if\left(0<N,S\left(N\right),I\left(S\left(-N\right)\right)\right)\right)\in \mathrm{V}$$
27	20 21 26	ovmpoa	$$⊢\left(N\in \mathbb{Z}\wedge X\in B\right)\to N\underset{\dot{}}{·}X=if\left(N=0,\underset{\dot{}}{0},if\left(0<N,S\left(N\right),I\left(S\left(-N\right)\right)\right)\right)$$