Theorem nn0omnd

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

	Ref	Expression
Assertion	nn0omnd	⊢ ( ℂfld ↾s ℕ0 ) ∈ oMnd

Proof

Step	Hyp	Ref	Expression
1		df-refld	⊢ ℝfld = ( ℂfld ↾s ℝ )
2	1	oveq1i	⊢ ( ℝfld ↾s ℕ0 ) = ( ( ℂfld ↾s ℝ ) ↾s ℕ0 )
3		reex	⊢ ℝ ∈ V
4		nn0ssre	⊢ ℕ0 ⊆ ℝ
5		ressabs	⊢ ( ( ℝ ∈ V ∧ ℕ0 ⊆ ℝ ) → ( ( ℂfld ↾s ℝ ) ↾s ℕ0 ) = ( ℂfld ↾s ℕ0 ) )
6	3 4 5	mp2an	⊢ ( ( ℂfld ↾s ℝ ) ↾s ℕ0 ) = ( ℂfld ↾s ℕ0 )
7	2 6	eqtri	⊢ ( ℝfld ↾s ℕ0 ) = ( ℂfld ↾s ℕ0 )
8		reofld	⊢ ℝfld ∈ oField
9		isofld	⊢ ( ℝfld ∈ oField ↔ ( ℝfld ∈ Field ∧ ℝfld ∈ oRing ) )
10	9	simprbi	⊢ ( ℝfld ∈ oField → ℝfld ∈ oRing )
11		orngogrp	⊢ ( ℝfld ∈ oRing → ℝfld ∈ oGrp )
12		isogrp	⊢ ( ℝfld ∈ oGrp ↔ ( ℝfld ∈ Grp ∧ ℝfld ∈ oMnd ) )
13	12	simprbi	⊢ ( ℝfld ∈ oGrp → ℝfld ∈ oMnd )
14	10 11 13	3syl	⊢ ( ℝfld ∈ oField → ℝfld ∈ oMnd )
15	8 14	ax-mp	⊢ ℝfld ∈ oMnd
16		nn0subm	⊢ ℕ0 ∈ ( SubMnd ‘ ℂfld )
17		eqid	⊢ ( ℂfld ↾s ℕ0 ) = ( ℂfld ↾s ℕ0 )
18	17	submmnd	⊢ ( ℕ0 ∈ ( SubMnd ‘ ℂfld ) → ( ℂfld ↾s ℕ0 ) ∈ Mnd )
19	16 18	ax-mp	⊢ ( ℂfld ↾s ℕ0 ) ∈ Mnd
20	7 19	eqeltri	⊢ ( ℝfld ↾s ℕ0 ) ∈ Mnd
21		submomnd	⊢ ( ( ℝfld ∈ oMnd ∧ ( ℝfld ↾s ℕ0 ) ∈ Mnd ) → ( ℝfld ↾s ℕ0 ) ∈ oMnd )
22	15 20 21	mp2an	⊢ ( ℝfld ↾s ℕ0 ) ∈ oMnd
23	7 22	eqeltrri	⊢ ( ℂfld ↾s ℕ0 ) ∈ oMnd