Theorem xrge0mulgnn0

Description: The group multiple function in the extended nonnegative real numbers. (Contributed by Thierry Arnoux, 14-Jun-2017)

	Ref	Expression
Assertion	xrge0mulgnn0	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \left[0,\mathrm{+\infty }\right]\right)\to A{\cdot }_{\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)}B=A{\cdot }_{𝑒}B$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢{ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]={ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]$$
2		iccssxr	$$⊢\left[0,\mathrm{+\infty }\right]\subseteq {ℝ}^{*}$$
3		xrsbas	$$⊢{ℝ}^{*}={\mathrm{Base}}_{{ℝ}_{𝑠}^{*}}$$
4	2 3	sseqtri	$$⊢\left[0,\mathrm{+\infty }\right]\subseteq {\mathrm{Base}}_{{ℝ}_{𝑠}^{*}}$$
5		eqid	$$⊢{\cdot }_{{ℝ}_{𝑠}^{*}}={\cdot }_{{ℝ}_{𝑠}^{*}}$$
6		eqid	$$⊢{inv}_g\left({ℝ}_{𝑠}^{*}\right)={inv}_g\left({ℝ}_{𝑠}^{*}\right)$$
7		xrs0	$$⊢0=0_{{ℝ}_{𝑠}^{*}}$$
8		xrge00	$$⊢0=0_{\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)}$$
9	7 8	eqtr3i	$$⊢0_{{ℝ}_{𝑠}^{*}}=0_{\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)}$$
10	1 4 5 6 9	ressmulgnn0	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \left[0,\mathrm{+\infty }\right]\right)\to A{\cdot }_{\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)}B=A{\cdot }_{{ℝ}_{𝑠}^{*}}B$$
11		nn0z	$$⊢A\in {\mathbb{N}}_0\to A\in \mathbb{Z}$$
12		eliccxr	$$⊢B\in \left[0,\mathrm{+\infty }\right]\to B\in {ℝ}^{*}$$
13		xrsmulgzz	$$⊢\left(A\in \mathbb{Z}\wedge B\in {ℝ}^{*}\right)\to A{\cdot }_{{ℝ}_{𝑠}^{*}}B=A{\cdot }_{𝑒}B$$
14	11 12 13	syl2an	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \left[0,\mathrm{+\infty }\right]\right)\to A{\cdot }_{{ℝ}_{𝑠}^{*}}B=A{\cdot }_{𝑒}B$$
15	10 14	eqtrd	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \left[0,\mathrm{+\infty }\right]\right)\to A{\cdot }_{\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)}B=A{\cdot }_{𝑒}B$$