Theorem mulg1

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

	Ref	Expression
Hypotheses	mulg1.b	$$⊢B={\mathrm{Base}}_G$$
	mulg1.m	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
Assertion	mulg1	$$⊢X\in B\to 1\underset{\dot{}}{·}X=X$$

Proof

Step	Hyp	Ref	Expression
1		mulg1.b	$$⊢B={\mathrm{Base}}_G$$
2		mulg1.m	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
3		1nn	$$⊢1\in \mathbb{N}$$
4		eqid	$$⊢{+}_G={+}_G$$
5		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)$$
6	1 4 2 5	mulgnn	$$⊢\left(1\in \mathbb{N}\wedge X\in B\right)\to 1\underset{\dot{}}{·}X=seq1\left({+}_G,\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(1\right)$$
7	3 6	mpan	$$⊢X\in B\to 1\underset{\dot{}}{·}X=seq1\left({+}_G,\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(1\right)$$
8		1z	$$⊢1\in \mathbb{Z}$$
9		fvconst2g	$$⊢\left(X\in B\wedge 1\in \mathbb{N}\right)\to \left(\mathbb{N}\times \left\{X\right\}\right)\left(1\right)=X$$
10	3 9	mpan2	$$⊢X\in B\to \left(\mathbb{N}\times \left\{X\right\}\right)\left(1\right)=X$$
11	8 10	seq1i	$$⊢X\in B\to seq1\left({+}_G,\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(1\right)=X$$
12	7 11	eqtrd	$$⊢X\in B\to 1\underset{\dot{}}{·}X=X$$