Theorem mulgnnp1

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

	Ref	Expression
Hypotheses	mulg1.b	$$⊢B={\mathrm{Base}}_G$$
	mulg1.m	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
	mulgnnp1.p	$$⊢\underset{\dot{}}{+}={+}_G$$
Assertion	mulgnnp1	$$⊢\left(N\in \mathbb{N}\wedge X\in B\right)\to \left(N+1\right)\underset{\dot{}}{·}X=\left(N\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}X$$

Proof

Step	Hyp	Ref	Expression
1		mulg1.b	$$⊢B={\mathrm{Base}}_G$$
2		mulg1.m	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
3		mulgnnp1.p	$$⊢\underset{\dot{}}{+}={+}_G$$
4		simpl	$$⊢\left(N\in \mathbb{N}\wedge X\in B\right)\to N\in \mathbb{N}$$
5		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
6	4 5	eleqtrdi	$$⊢\left(N\in \mathbb{N}\wedge X\in B\right)\to N\in {\mathbb{Z}}_{\ge 1}$$
7		seqp1	$$⊢N\in {\mathbb{Z}}_{\ge 1}\to seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(N+1\right)=seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(N\right)\underset{\dot{}}{+}\left(\mathbb{N}\times \left\{X\right\}\right)\left(N+1\right)$$
8	6 7	syl	$$⊢\left(N\in \mathbb{N}\wedge X\in B\right)\to seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(N+1\right)=seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(N\right)\underset{\dot{}}{+}\left(\mathbb{N}\times \left\{X\right\}\right)\left(N+1\right)$$
9		id	$$⊢X\in B\to X\in B$$
10		peano2nn	$$⊢N\in \mathbb{N}\to N+1\in \mathbb{N}$$
11		fvconst2g	$$⊢\left(X\in B\wedge N+1\in \mathbb{N}\right)\to \left(\mathbb{N}\times \left\{X\right\}\right)\left(N+1\right)=X$$
12	9 10 11	syl2anr	$$⊢\left(N\in \mathbb{N}\wedge X\in B\right)\to \left(\mathbb{N}\times \left\{X\right\}\right)\left(N+1\right)=X$$
13	12	oveq2d	$$⊢\left(N\in \mathbb{N}\wedge X\in B\right)\to seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(N\right)\underset{\dot{}}{+}\left(\mathbb{N}\times \left\{X\right\}\right)\left(N+1\right)=seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(N\right)\underset{\dot{}}{+}X$$
14	8 13	eqtrd	$$⊢\left(N\in \mathbb{N}\wedge X\in B\right)\to seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(N+1\right)=seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(N\right)\underset{\dot{}}{+}X$$
15		eqid	$$⊢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)$$
16	1 3 2 15	mulgnn	$$⊢\left(N+1\in \mathbb{N}\wedge X\in B\right)\to \left(N+1\right)\underset{\dot{}}{·}X=seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(N+1\right)$$
17	10 16	sylan	$$⊢\left(N\in \mathbb{N}\wedge X\in B\right)\to \left(N+1\right)\underset{\dot{}}{·}X=seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(N+1\right)$$
18	1 3 2 15	mulgnn	$$⊢\left(N\in \mathbb{N}\wedge X\in B\right)\to N\underset{\dot{}}{·}X=seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(N\right)$$
19	18	oveq1d	$$⊢\left(N\in \mathbb{N}\wedge X\in B\right)\to \left(N\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}X=seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(N\right)\underset{\dot{}}{+}X$$
20	14 17 19	3eqtr4d	$$⊢\left(N\in \mathbb{N}\wedge X\in B\right)\to \left(N+1\right)\underset{\dot{}}{·}X=\left(N\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}X$$