Theorem mulgfn

Description: Functionality of the group multiple operation. (Contributed by Mario Carneiro, 21-Mar-2015) (Revised by Mario Carneiro, 2-Oct-2015)

	Ref	Expression
Hypotheses	mulgfn.b	$$⊢B={\mathrm{Base}}_G$$
	mulgfn.t	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
Assertion	mulgfn	$$⊢\underset{\dot{}}{·}Fn\left(\mathbb{Z}\times B\right)$$

Proof

Step	Hyp	Ref	Expression
1		mulgfn.b	$$⊢B={\mathrm{Base}}_G$$
2		mulgfn.t	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
3		eqid	$$⊢{+}_G={+}_G$$
4		eqid	$$⊢0_G=0_G$$
5		eqid	$$⊢{inv}_g\left(G\right)={inv}_g\left(G\right)$$
6	1 3 4 5 2	mulgfval	$$⊢\underset{\dot{}}{·}=\left(n\in \mathbb{Z},x\in B⟼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),{inv}_g\left(G\right)\left(seq1\left({+}_G,\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(-n\right)\right)\right)\right)\right)$$
7		fvex	$$⊢0_G\in \mathrm{V}$$
8		fvex	$$⊢seq1\left({+}_G,\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n\right)\in \mathrm{V}$$
9		fvex	$$⊢{inv}_g\left(G\right)\left(seq1\left({+}_G,\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(-n\right)\right)\in \mathrm{V}$$
10	8 9	ifex	$$⊢if\left(0<n,seq1\left({+}_G,\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(n\right),{inv}_g\left(G\right)\left(seq1\left({+}_G,\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(-n\right)\right)\right)\in \mathrm{V}$$
11	7 10	ifex	$$⊢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),{inv}_g\left(G\right)\left(seq1\left({+}_G,\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(-n\right)\right)\right)\right)\in \mathrm{V}$$
12	6 11	fnmpoi	$$⊢\underset{\dot{}}{·}Fn\left(\mathbb{Z}\times B\right)$$