Theorem nn0omnd

Description: The nonnegative integers form an ordered monoid. (Contributed by Thierry Arnoux, 23-Mar-2018)

	Ref	Expression
Assertion	nn0omnd	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\in \mathrm{oMnd}$$

Proof

Step	Hyp	Ref	Expression
1		df-refld	$$⊢{ℝ}_{\mathrm{fld}}={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ$$
2	1	oveq1i	$$⊢{ℝ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0=\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ\right){\upharpoonright }_{𝑠}{\mathbb{N}}_0$$
3		reex	$$⊢ℝ\in \mathrm{V}$$
4		nn0ssre	$$⊢{\mathbb{N}}_0\subseteq ℝ$$
5		ressabs	$$⊢\left(ℝ\in \mathrm{V}\wedge {\mathbb{N}}_0\subseteq ℝ\right)\to \left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ\right){\upharpoonright }_{𝑠}{\mathbb{N}}_0={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0$$
6	3 4 5	mp2an	$$⊢\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ\right){\upharpoonright }_{𝑠}{\mathbb{N}}_0={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0$$
7	2 6	eqtri	$$⊢{ℝ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0$$
8		reofld	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{oField}$$
9		isofld	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{oField}\leftrightarrow \left({ℝ}_{\mathrm{fld}}\in \mathrm{Field}\wedge {ℝ}_{\mathrm{fld}}\in \mathrm{oRing}\right)$$
10	9	simprbi	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{oField}\to {ℝ}_{\mathrm{fld}}\in \mathrm{oRing}$$
11		orngogrp	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{oRing}\to {ℝ}_{\mathrm{fld}}\in \mathrm{oGrp}$$
12		isogrp	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{oGrp}\leftrightarrow \left({ℝ}_{\mathrm{fld}}\in \mathrm{Grp}\wedge {ℝ}_{\mathrm{fld}}\in \mathrm{oMnd}\right)$$
13	12	simprbi	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{oGrp}\to {ℝ}_{\mathrm{fld}}\in \mathrm{oMnd}$$
14	10 11 13	3syl	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{oField}\to {ℝ}_{\mathrm{fld}}\in \mathrm{oMnd}$$
15	8 14	ax-mp	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{oMnd}$$
16		nn0subm	$$⊢{\mathbb{N}}_0\in \mathrm{SubMnd}\left({ℂ}_{\mathrm{fld}}\right)$$
17		eqid	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0$$
18	17	submmnd	$$⊢{\mathbb{N}}_0\in \mathrm{SubMnd}\left({ℂ}_{\mathrm{fld}}\right)\to {ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\in \mathrm{Mnd}$$
19	16 18	ax-mp	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\in \mathrm{Mnd}$$
20	7 19	eqeltri	$$⊢{ℝ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\in \mathrm{Mnd}$$
21		submomnd	$$⊢\left({ℝ}_{\mathrm{fld}}\in \mathrm{oMnd}\wedge {ℝ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\in \mathrm{Mnd}\right)\to {ℝ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\in \mathrm{oMnd}$$
22	15 20 21	mp2an	$$⊢{ℝ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\in \mathrm{oMnd}$$
23	7 22	eqeltrri	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\in \mathrm{oMnd}$$