Theorem ressmulgnn0d

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

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

Proof

Step	Hyp	Ref	Expression
1		ressmulgnn0d.1	$$⊢\phi \to G{\upharpoonright }_{𝑠}A=H$$
2		ressmulgnn0d.2	$$⊢\phi \to 0_G=0_H$$
3		ressmulgnn0d.3	$$⊢\phi \to A\subseteq {\mathrm{Base}}_G$$
4		ressmulgnn0d.4	$$⊢\phi \to N\in {\mathbb{N}}_0$$
5		ressmulgnn0d.5	$$⊢\phi \to X\in A$$
6	1	fveq2d	$$⊢\phi \to {\cdot }_{\left(G{\upharpoonright }_{𝑠}A\right)}={\cdot }_H$$
7	6	oveqd	$$⊢\phi \to N{\cdot }_{\left(G{\upharpoonright }_{𝑠}A\right)}X=N{\cdot }_{H}X$$
8	7	adantr	$$⊢\left(\phi \wedge N\in \mathbb{N}\right)\to N{\cdot }_{\left(G{\upharpoonright }_{𝑠}A\right)}X=N{\cdot }_{H}X$$
9		eqid	$$⊢G{\upharpoonright }_{𝑠}A=G{\upharpoonright }_{𝑠}A$$
10	3	adantr	$$⊢\left(\phi \wedge N\in \mathbb{N}\right)\to A\subseteq {\mathrm{Base}}_G$$
11	5	adantr	$$⊢\left(\phi \wedge N\in \mathbb{N}\right)\to X\in A$$
12		simpr	$$⊢\left(\phi \wedge N\in \mathbb{N}\right)\to N\in \mathbb{N}$$
13	9 10 11 12	ressmulgnnd	$$⊢\left(\phi \wedge N\in \mathbb{N}\right)\to N{\cdot }_{\left(G{\upharpoonright }_{𝑠}A\right)}X=N{\cdot }_{G}X$$
14	8 13	eqtr3d	$$⊢\left(\phi \wedge N\in \mathbb{N}\right)\to N{\cdot }_{H}X=N{\cdot }_{G}X$$
15	5	adantr	$$⊢\left(\phi \wedge N=0\right)\to X\in A$$
16		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
17	9 16	ressbas2	$$⊢A\subseteq {\mathrm{Base}}_G\to A={\mathrm{Base}}_{\left(G{\upharpoonright }_{𝑠}A\right)}$$
18	3 17	syl	$$⊢\phi \to A={\mathrm{Base}}_{\left(G{\upharpoonright }_{𝑠}A\right)}$$
19	18	adantr	$$⊢\left(\phi \wedge N=0\right)\to A={\mathrm{Base}}_{\left(G{\upharpoonright }_{𝑠}A\right)}$$
20	15 19	eleqtrd	$$⊢\left(\phi \wedge N=0\right)\to X\in {\mathrm{Base}}_{\left(G{\upharpoonright }_{𝑠}A\right)}$$
21		eqid	$$⊢{\mathrm{Base}}_{\left(G{\upharpoonright }_{𝑠}A\right)}={\mathrm{Base}}_{\left(G{\upharpoonright }_{𝑠}A\right)}$$
22		eqid	$$⊢0_{\left(G{\upharpoonright }_{𝑠}A\right)}=0_{\left(G{\upharpoonright }_{𝑠}A\right)}$$
23		eqid	$$⊢{\cdot }_{\left(G{\upharpoonright }_{𝑠}A\right)}={\cdot }_{\left(G{\upharpoonright }_{𝑠}A\right)}$$
24	21 22 23	mulg0	$$⊢X\in {\mathrm{Base}}_{\left(G{\upharpoonright }_{𝑠}A\right)}\to 0{\cdot }_{\left(G{\upharpoonright }_{𝑠}A\right)}X=0_{\left(G{\upharpoonright }_{𝑠}A\right)}$$
25	20 24	syl	$$⊢\left(\phi \wedge N=0\right)\to 0{\cdot }_{\left(G{\upharpoonright }_{𝑠}A\right)}X=0_{\left(G{\upharpoonright }_{𝑠}A\right)}$$
26	6	oveqd	$$⊢\phi \to 0{\cdot }_{\left(G{\upharpoonright }_{𝑠}A\right)}X=0{\cdot }_{H}X$$
27	26	adantr	$$⊢\left(\phi \wedge N=0\right)\to 0{\cdot }_{\left(G{\upharpoonright }_{𝑠}A\right)}X=0{\cdot }_{H}X$$
28	1	adantr	$$⊢\left(\phi \wedge N=0\right)\to G{\upharpoonright }_{𝑠}A=H$$
29	28	fveq2d	$$⊢\left(\phi \wedge N=0\right)\to 0_{\left(G{\upharpoonright }_{𝑠}A\right)}=0_H$$
30	2	adantr	$$⊢\left(\phi \wedge N=0\right)\to 0_G=0_H$$
31	29 30	eqtr4d	$$⊢\left(\phi \wedge N=0\right)\to 0_{\left(G{\upharpoonright }_{𝑠}A\right)}=0_G$$
32	25 27 31	3eqtr3d	$$⊢\left(\phi \wedge N=0\right)\to 0{\cdot }_{H}X=0_G$$
33		simpr	$$⊢\left(\phi \wedge N=0\right)\to N=0$$
34	33	oveq1d	$$⊢\left(\phi \wedge N=0\right)\to N{\cdot }_{H}X=0{\cdot }_{H}X$$
35	3	adantr	$$⊢\left(\phi \wedge N=0\right)\to A\subseteq {\mathrm{Base}}_G$$
36	35 15	sseldd	$$⊢\left(\phi \wedge N=0\right)\to X\in {\mathrm{Base}}_G$$
37		eqid	$$⊢0_G=0_G$$
38		eqid	$$⊢{\cdot }_G={\cdot }_G$$
39	16 37 38	mulg0	$$⊢X\in {\mathrm{Base}}_G\to 0{\cdot }_{G}X=0_G$$
40	36 39	syl	$$⊢\left(\phi \wedge N=0\right)\to 0{\cdot }_{G}X=0_G$$
41	32 34 40	3eqtr4d	$$⊢\left(\phi \wedge N=0\right)\to N{\cdot }_{H}X=0{\cdot }_{G}X$$
42	33	oveq1d	$$⊢\left(\phi \wedge N=0\right)\to N{\cdot }_{G}X=0{\cdot }_{G}X$$
43	41 42	eqtr4d	$$⊢\left(\phi \wedge N=0\right)\to N{\cdot }_{H}X=N{\cdot }_{G}X$$
44		elnn0	$$⊢N\in {\mathbb{N}}_0\leftrightarrow \left(N\in \mathbb{N}\vee N=0\right)$$
45	4 44	sylib	$$⊢\phi \to \left(N\in \mathbb{N}\vee N=0\right)$$
46	14 43 45	mpjaodan	$$⊢\phi \to N{\cdot }_{H}X=N{\cdot }_{G}X$$