Theorem ressmulgnnd

Description: Values for the group multiple function in a restricted structure, a deduction version. (Contributed by metakunt, 14-May-2025)

	Ref	Expression
Hypotheses	ressmulgnnd.1	$$⊢H=G{\upharpoonright }_{𝑠}A$$
	ressmulgnnd.2	$$⊢\phi \to A\subseteq {\mathrm{Base}}_G$$
	ressmulgnnd.3	$$⊢\phi \to X\in A$$
	ressmulgnnd.4	$$⊢\phi \to N\in \mathbb{N}$$
Assertion	ressmulgnnd	$$⊢\phi \to N{\cdot }_{H}X=N{\cdot }_{G}X$$

Proof

Step	Hyp	Ref	Expression
1		ressmulgnnd.1	$$⊢H=G{\upharpoonright }_{𝑠}A$$
2		ressmulgnnd.2	$$⊢\phi \to A\subseteq {\mathrm{Base}}_G$$
3		ressmulgnnd.3	$$⊢\phi \to X\in A$$
4		ressmulgnnd.4	$$⊢\phi \to N\in \mathbb{N}$$
5	4	nngt0d	$$⊢\phi \to 0<N$$
6	4	adantr	$$⊢\left(\phi \wedge 0<N\right)\to N\in \mathbb{N}$$
7	3	adantr	$$⊢\left(\phi \wedge 0<N\right)\to X\in A$$
8		eqid	$$⊢G{\upharpoonright }_{𝑠}A=G{\upharpoonright }_{𝑠}A$$
9		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
10	8 9	ressbas2	$$⊢A\subseteq {\mathrm{Base}}_G\to A={\mathrm{Base}}_{\left(G{\upharpoonright }_{𝑠}A\right)}$$
11	2 10	syl	$$⊢\phi \to A={\mathrm{Base}}_{\left(G{\upharpoonright }_{𝑠}A\right)}$$
12	11	adantr	$$⊢\left(\phi \wedge 0<N\right)\to A={\mathrm{Base}}_{\left(G{\upharpoonright }_{𝑠}A\right)}$$
13		eqcom	$$⊢H=G{\upharpoonright }_{𝑠}A\leftrightarrow G{\upharpoonright }_{𝑠}A=H$$
14	1 13	mpbi	$$⊢G{\upharpoonright }_{𝑠}A=H$$
15	14	fveq2i	$$⊢{\mathrm{Base}}_{\left(G{\upharpoonright }_{𝑠}A\right)}={\mathrm{Base}}_H$$
16	15	a1i	$$⊢\left(\phi \wedge 0<N\right)\to {\mathrm{Base}}_{\left(G{\upharpoonright }_{𝑠}A\right)}={\mathrm{Base}}_H$$
17	12 16	eqtrd	$$⊢\left(\phi \wedge 0<N\right)\to A={\mathrm{Base}}_H$$
18	7 17	eleqtrd	$$⊢\left(\phi \wedge 0<N\right)\to X\in {\mathrm{Base}}_H$$
19		eqid	$$⊢{\mathrm{Base}}_H={\mathrm{Base}}_H$$
20		eqid	$$⊢{+}_H={+}_H$$
21		eqid	$$⊢{\cdot }_H={\cdot }_H$$
22		eqid	$$⊢seq1\left({+}_H,\left(\mathbb{N}\times \left\{X\right\}\right)\right)=seq1\left({+}_H,\left(\mathbb{N}\times \left\{X\right\}\right)\right)$$
23	19 20 21 22	mulgnn	$$⊢\left(N\in \mathbb{N}\wedge X\in {\mathrm{Base}}_H\right)\to N{\cdot }_{H}X=seq1\left({+}_H,\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(N\right)$$
24	6 18 23	syl2anc	$$⊢\left(\phi \wedge 0<N\right)\to N{\cdot }_{H}X=seq1\left({+}_H,\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(N\right)$$
25		fvexd	$$⊢\phi \to {\mathrm{Base}}_G\in \mathrm{V}$$
26	25 2	ssexd	$$⊢\phi \to A\in \mathrm{V}$$
27		eqid	$$⊢{+}_G={+}_G$$
28	1 27	ressplusg	$$⊢A\in \mathrm{V}\to {+}_G={+}_H$$
29	26 28	syl	$$⊢\phi \to {+}_G={+}_H$$
30	29	eqcomd	$$⊢\phi \to {+}_H={+}_G$$
31	30	adantr	$$⊢\left(\phi \wedge 0<N\right)\to {+}_H={+}_G$$
32	31	seqeq2d	$$⊢\left(\phi \wedge 0<N\right)\to seq1\left({+}_H,\left(\mathbb{N}\times \left\{X\right\}\right)\right)=seq1\left({+}_G,\left(\mathbb{N}\times \left\{X\right\}\right)\right)$$
33	32	fveq1d	$$⊢\left(\phi \wedge 0<N\right)\to seq1\left({+}_H,\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(N\right)=seq1\left({+}_G,\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(N\right)$$
34	2 3	sseldd	$$⊢\phi \to X\in {\mathrm{Base}}_G$$
35	34	adantr	$$⊢\left(\phi \wedge 0<N\right)\to X\in {\mathrm{Base}}_G$$
36		eqid	$$⊢{\cdot }_G={\cdot }_G$$
37		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)$$
38	9 27 36 37	mulgnn	$$⊢\left(N\in \mathbb{N}\wedge X\in {\mathrm{Base}}_G\right)\to N{\cdot }_{G}X=seq1\left({+}_G,\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(N\right)$$
39	6 35 38	syl2anc	$$⊢\left(\phi \wedge 0<N\right)\to N{\cdot }_{G}X=seq1\left({+}_G,\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(N\right)$$
40	39	eqcomd	$$⊢\left(\phi \wedge 0<N\right)\to seq1\left({+}_G,\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(N\right)=N{\cdot }_{G}X$$
41	24 33 40	3eqtrd	$$⊢\left(\phi \wedge 0<N\right)\to N{\cdot }_{H}X=N{\cdot }_{G}X$$
42	41	ex	$$⊢\phi \to \left(0<N\to N{\cdot }_{H}X=N{\cdot }_{G}X\right)$$
43	5 42	mpd	$$⊢\phi \to N{\cdot }_{H}X=N{\cdot }_{G}X$$