Theorem ressmulgnn0

Description: Values for the group multiple function in a restricted structure. (Contributed by Thierry Arnoux, 14-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)$$
	ressmulgnn0.4	$$⊢0_G=0_H$$
Assertion	ressmulgnn0	$$⊢\left(N\in {\mathbb{N}}_0\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		ressmulgnn0.4	$$⊢0_G=0_H$$
6		simpr	$$⊢\left(\left(N\in {\mathbb{N}}_0\wedge X\in A\right)\wedge N\in \mathbb{N}\right)\to N\in \mathbb{N}$$
7		simplr	$$⊢\left(\left(N\in {\mathbb{N}}_0\wedge X\in A\right)\wedge N\in \mathbb{N}\right)\to X\in A$$
8	1 2 3 4	ressmulgnn	$$⊢\left(N\in \mathbb{N}\wedge X\in A\right)\to N{\cdot }_{H}X=N\underset{\dot{}}{\ast }X$$
9	6 7 8	syl2anc	$$⊢\left(\left(N\in {\mathbb{N}}_0\wedge X\in A\right)\wedge N\in \mathbb{N}\right)\to N{\cdot }_{H}X=N\underset{\dot{}}{\ast }X$$
10		simplr	$$⊢\left(\left(N\in {\mathbb{N}}_0\wedge X\in A\right)\wedge N=0\right)\to X\in A$$
11		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
12	1 11	ressbas2	$$⊢A\subseteq {\mathrm{Base}}_G\to A={\mathrm{Base}}_H$$
13	2 12	ax-mp	$$⊢A={\mathrm{Base}}_H$$
14		eqid	$$⊢{\cdot }_H={\cdot }_H$$
15	13 5 14	mulg0	$$⊢X\in A\to 0{\cdot }_{H}X=0_G$$
16	10 15	syl	$$⊢\left(\left(N\in {\mathbb{N}}_0\wedge X\in A\right)\wedge N=0\right)\to 0{\cdot }_{H}X=0_G$$
17		simpr	$$⊢\left(\left(N\in {\mathbb{N}}_0\wedge X\in A\right)\wedge N=0\right)\to N=0$$
18	17	oveq1d	$$⊢\left(\left(N\in {\mathbb{N}}_0\wedge X\in A\right)\wedge N=0\right)\to N{\cdot }_{H}X=0{\cdot }_{H}X$$
19	2 10	sselid	$$⊢\left(\left(N\in {\mathbb{N}}_0\wedge X\in A\right)\wedge N=0\right)\to X\in {\mathrm{Base}}_G$$
20		eqid	$$⊢0_G=0_G$$
21	11 20 3	mulg0	$$⊢X\in {\mathrm{Base}}_G\to 0\underset{\dot{}}{\ast }X=0_G$$
22	19 21	syl	$$⊢\left(\left(N\in {\mathbb{N}}_0\wedge X\in A\right)\wedge N=0\right)\to 0\underset{\dot{}}{\ast }X=0_G$$
23	16 18 22	3eqtr4d	$$⊢\left(\left(N\in {\mathbb{N}}_0\wedge X\in A\right)\wedge N=0\right)\to N{\cdot }_{H}X=0\underset{\dot{}}{\ast }X$$
24	17	oveq1d	$$⊢\left(\left(N\in {\mathbb{N}}_0\wedge X\in A\right)\wedge N=0\right)\to N\underset{\dot{}}{\ast }X=0\underset{\dot{}}{\ast }X$$
25	23 24	eqtr4d	$$⊢\left(\left(N\in {\mathbb{N}}_0\wedge X\in A\right)\wedge N=0\right)\to N{\cdot }_{H}X=N\underset{\dot{}}{\ast }X$$
26		elnn0	$$⊢N\in {\mathbb{N}}_0\leftrightarrow \left(N\in \mathbb{N}\vee N=0\right)$$
27	26	biimpi	$$⊢N\in {\mathbb{N}}_0\to \left(N\in \mathbb{N}\vee N=0\right)$$
28	27	adantr	$$⊢\left(N\in {\mathbb{N}}_0\wedge X\in A\right)\to \left(N\in \mathbb{N}\vee N=0\right)$$
29	9 25 28	mpjaodan	$$⊢\left(N\in {\mathbb{N}}_0\wedge X\in A\right)\to N{\cdot }_{H}X=N\underset{\dot{}}{\ast }X$$