Theorem ressmulgnn

Description: Values for the group multiple function in a restricted structure. (Contributed by Thierry Arnoux, 12-Jun-2017)

	Ref	Expression
Hypotheses	ressmulgnn.1	$$⊢H=G{\upharpoonright }_{𝑠}A$$
	ressmulgnn.2	$$⊢A\subseteq {\mathrm{Base}}_G$$
	ressmulgnn.3	$$⊢\underset{\dot{}}{\ast }={\cdot }_G$$
	ressmulgnn.4	$$⊢I={inv}_g\left(G\right)$$
Assertion	ressmulgnn	$$⊢\left(N\in \mathbb{N}\wedge X\in A\right)\to N{\cdot }_{H}X=N\underset{\dot{}}{\ast }X$$

Proof

Step	Hyp	Ref	Expression
1		ressmulgnn.1	$$⊢H=G{\upharpoonright }_{𝑠}A$$
2		ressmulgnn.2	$$⊢A\subseteq {\mathrm{Base}}_G$$
3		ressmulgnn.3	$$⊢\underset{\dot{}}{\ast }={\cdot }_G$$
4		ressmulgnn.4	$$⊢I={inv}_g\left(G\right)$$
5		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
6	1 5	ressbas2	$$⊢A\subseteq {\mathrm{Base}}_G\to A={\mathrm{Base}}_H$$
7	2 6	ax-mp	$$⊢A={\mathrm{Base}}_H$$
8		eqid	$$⊢{+}_H={+}_H$$
9		eqid	$$⊢{\cdot }_H={\cdot }_H$$
10		fvex	$$⊢{\mathrm{Base}}_G\in \mathrm{V}$$
11	10 2	ssexi	$$⊢A\in \mathrm{V}$$
12		eqid	$$⊢{+}_G={+}_G$$
13	1 12	ressplusg	$$⊢A\in \mathrm{V}\to {+}_G={+}_H$$
14	11 13	ax-mp	$$⊢{+}_G={+}_H$$
15		seqeq2	$$⊢{+}_G={+}_H\to seq1\left({+}_G,\left(\mathbb{N}\times \left\{X\right\}\right)\right)=seq1\left({+}_H,\left(\mathbb{N}\times \left\{X\right\}\right)\right)$$
16	14 15	ax-mp	$$⊢seq1\left({+}_G,\left(\mathbb{N}\times \left\{X\right\}\right)\right)=seq1\left({+}_H,\left(\mathbb{N}\times \left\{X\right\}\right)\right)$$
17	7 8 9 16	mulgnn	$$⊢\left(N\in \mathbb{N}\wedge X\in A\right)\to N{\cdot }_{H}X=seq1\left({+}_G,\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(N\right)$$
18		simpr	$$⊢\left(N\in \mathbb{N}\wedge X\in A\right)\to X\in A$$
19	2 18	sselid	$$⊢\left(N\in \mathbb{N}\wedge X\in A\right)\to X\in {\mathrm{Base}}_G$$
20		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)$$
21	5 12 3 20	mulgnn	$$⊢\left(N\in \mathbb{N}\wedge X\in {\mathrm{Base}}_G\right)\to N\underset{\dot{}}{\ast }X=seq1\left({+}_G,\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(N\right)$$
22	19 21	syldan	$$⊢\left(N\in \mathbb{N}\wedge X\in A\right)\to N\underset{\dot{}}{\ast }X=seq1\left({+}_G,\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(N\right)$$
23	17 22	eqtr4d	$$⊢\left(N\in \mathbb{N}\wedge X\in A\right)\to N{\cdot }_{H}X=N\underset{\dot{}}{\ast }X$$