Theorem nn0srg

Description: The nonnegative integers form a semiring (commutative by subcmn ). (Contributed by Thierry Arnoux, 1-May-2018)

	Ref	Expression
Assertion	nn0srg	⊢ ( ℂfld ↾s ℕ0 ) ∈ SRing

Proof

Step	Hyp	Ref	Expression
1		cnring	⊢ ℂfld ∈ Ring
2		ringcmn	⊢ ( ℂfld ∈ Ring → ℂfld ∈ CMnd )
3	1 2	ax-mp	⊢ ℂfld ∈ CMnd
4		nn0subm	⊢ ℕ0 ∈ ( SubMnd ‘ ℂfld )
5		eqid	⊢ ( ℂfld ↾s ℕ0 ) = ( ℂfld ↾s ℕ0 )
6	5	submcmn	⊢ ( ( ℂfld ∈ CMnd ∧ ℕ0 ∈ ( SubMnd ‘ ℂfld ) ) → ( ℂfld ↾s ℕ0 ) ∈ CMnd )
7	3 4 6	mp2an	⊢ ( ℂfld ↾s ℕ0 ) ∈ CMnd
8		nn0ex	⊢ ℕ0 ∈ V
9		eqid	⊢ ( mulGrp ‘ ℂfld ) = ( mulGrp ‘ ℂfld )
10	5 9	mgpress	⊢ ( ( ℂfld ∈ CMnd ∧ ℕ0 ∈ V ) → ( ( mulGrp ‘ ℂfld ) ↾s ℕ0 ) = ( mulGrp ‘ ( ℂfld ↾s ℕ0 ) ) )
11	3 8 10	mp2an	⊢ ( ( mulGrp ‘ ℂfld ) ↾s ℕ0 ) = ( mulGrp ‘ ( ℂfld ↾s ℕ0 ) )
12		nn0sscn	⊢ ℕ0 ⊆ ℂ
13		1nn0	⊢ 1 ∈ ℕ0
14		nn0mulcl	⊢ ( ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) → ( 𝑥 · 𝑦 ) ∈ ℕ0 )
15	14	rgen2	⊢ ∀ 𝑥 ∈ ℕ0 ∀ 𝑦 ∈ ℕ0 ( 𝑥 · 𝑦 ) ∈ ℕ0
16	9	ringmgp	⊢ ( ℂfld ∈ Ring → ( mulGrp ‘ ℂfld ) ∈ Mnd )
17	1 16	ax-mp	⊢ ( mulGrp ‘ ℂfld ) ∈ Mnd
18		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
19	9 18	mgpbas	⊢ ℂ = ( Base ‘ ( mulGrp ‘ ℂfld ) )
20		cnfld1	⊢ 1 = ( 1r ‘ ℂfld )
21	9 20	ringidval	⊢ 1 = ( 0g ‘ ( mulGrp ‘ ℂfld ) )
22		cnfldmul	⊢ · = ( .r ‘ ℂfld )
23	9 22	mgpplusg	⊢ · = ( +g ‘ ( mulGrp ‘ ℂfld ) )
24	19 21 23	issubm	⊢ ( ( mulGrp ‘ ℂfld ) ∈ Mnd → ( ℕ0 ∈ ( SubMnd ‘ ( mulGrp ‘ ℂfld ) ) ↔ ( ℕ0 ⊆ ℂ ∧ 1 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ∀ 𝑦 ∈ ℕ0 ( 𝑥 · 𝑦 ) ∈ ℕ0 ) ) )
25	17 24	ax-mp	⊢ ( ℕ0 ∈ ( SubMnd ‘ ( mulGrp ‘ ℂfld ) ) ↔ ( ℕ0 ⊆ ℂ ∧ 1 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ∀ 𝑦 ∈ ℕ0 ( 𝑥 · 𝑦 ) ∈ ℕ0 ) )
26	12 13 15 25	mpbir3an	⊢ ℕ0 ∈ ( SubMnd ‘ ( mulGrp ‘ ℂfld ) )
27		eqid	⊢ ( ( mulGrp ‘ ℂfld ) ↾s ℕ0 ) = ( ( mulGrp ‘ ℂfld ) ↾s ℕ0 )
28	27	submmnd	⊢ ( ℕ0 ∈ ( SubMnd ‘ ( mulGrp ‘ ℂfld ) ) → ( ( mulGrp ‘ ℂfld ) ↾s ℕ0 ) ∈ Mnd )
29	26 28	ax-mp	⊢ ( ( mulGrp ‘ ℂfld ) ↾s ℕ0 ) ∈ Mnd
30	11 29	eqeltrri	⊢ ( mulGrp ‘ ( ℂfld ↾s ℕ0 ) ) ∈ Mnd
31		simpl	⊢ ( ( 𝑥 ∈ ℕ0 ∧ ( 𝑦 ∈ ℕ0 ∧ 𝑧 ∈ ℕ0 ) ) → 𝑥 ∈ ℕ0 )
32	31	nn0cnd	⊢ ( ( 𝑥 ∈ ℕ0 ∧ ( 𝑦 ∈ ℕ0 ∧ 𝑧 ∈ ℕ0 ) ) → 𝑥 ∈ ℂ )
33		simprl	⊢ ( ( 𝑥 ∈ ℕ0 ∧ ( 𝑦 ∈ ℕ0 ∧ 𝑧 ∈ ℕ0 ) ) → 𝑦 ∈ ℕ0 )
34	33	nn0cnd	⊢ ( ( 𝑥 ∈ ℕ0 ∧ ( 𝑦 ∈ ℕ0 ∧ 𝑧 ∈ ℕ0 ) ) → 𝑦 ∈ ℂ )
35		simprr	⊢ ( ( 𝑥 ∈ ℕ0 ∧ ( 𝑦 ∈ ℕ0 ∧ 𝑧 ∈ ℕ0 ) ) → 𝑧 ∈ ℕ0 )
36	35	nn0cnd	⊢ ( ( 𝑥 ∈ ℕ0 ∧ ( 𝑦 ∈ ℕ0 ∧ 𝑧 ∈ ℕ0 ) ) → 𝑧 ∈ ℂ )
37	32 34 36	adddid	⊢ ( ( 𝑥 ∈ ℕ0 ∧ ( 𝑦 ∈ ℕ0 ∧ 𝑧 ∈ ℕ0 ) ) → ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) )
38	32 34 36	adddird	⊢ ( ( 𝑥 ∈ ℕ0 ∧ ( 𝑦 ∈ ℕ0 ∧ 𝑧 ∈ ℕ0 ) ) → ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) )
39	37 38	jca	⊢ ( ( 𝑥 ∈ ℕ0 ∧ ( 𝑦 ∈ ℕ0 ∧ 𝑧 ∈ ℕ0 ) ) → ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) )
40	39	ralrimivva	⊢ ( 𝑥 ∈ ℕ0 → ∀ 𝑦 ∈ ℕ0 ∀ 𝑧 ∈ ℕ0 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) )
41		nn0cn	⊢ ( 𝑥 ∈ ℕ0 → 𝑥 ∈ ℂ )
42	41	mul02d	⊢ ( 𝑥 ∈ ℕ0 → ( 0 · 𝑥 ) = 0 )
43	41	mul01d	⊢ ( 𝑥 ∈ ℕ0 → ( 𝑥 · 0 ) = 0 )
44	40 42 43	jca32	⊢ ( 𝑥 ∈ ℕ0 → ( ∀ 𝑦 ∈ ℕ0 ∀ 𝑧 ∈ ℕ0 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( 0 · 𝑥 ) = 0 ∧ ( 𝑥 · 0 ) = 0 ) ) )
45	44	rgen	⊢ ∀ 𝑥 ∈ ℕ0 ( ∀ 𝑦 ∈ ℕ0 ∀ 𝑧 ∈ ℕ0 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( 0 · 𝑥 ) = 0 ∧ ( 𝑥 · 0 ) = 0 ) )
46	5 18	ressbas2	⊢ ( ℕ0 ⊆ ℂ → ℕ0 = ( Base ‘ ( ℂfld ↾s ℕ0 ) ) )
47	12 46	ax-mp	⊢ ℕ0 = ( Base ‘ ( ℂfld ↾s ℕ0 ) )
48		eqid	⊢ ( mulGrp ‘ ( ℂfld ↾s ℕ0 ) ) = ( mulGrp ‘ ( ℂfld ↾s ℕ0 ) )
49		cnfldadd	⊢ + = ( +g ‘ ℂfld )
50	5 49	ressplusg	⊢ ( ℕ0 ∈ V → + = ( +g ‘ ( ℂfld ↾s ℕ0 ) ) )
51	8 50	ax-mp	⊢ + = ( +g ‘ ( ℂfld ↾s ℕ0 ) )
52	5 22	ressmulr	⊢ ( ℕ0 ∈ V → · = ( .r ‘ ( ℂfld ↾s ℕ0 ) ) )
53	8 52	ax-mp	⊢ · = ( .r ‘ ( ℂfld ↾s ℕ0 ) )
54		ringmnd	⊢ ( ℂfld ∈ Ring → ℂfld ∈ Mnd )
55	1 54	ax-mp	⊢ ℂfld ∈ Mnd
56		0nn0	⊢ 0 ∈ ℕ0
57		cnfld0	⊢ 0 = ( 0g ‘ ℂfld )
58	5 18 57	ress0g	⊢ ( ( ℂfld ∈ Mnd ∧ 0 ∈ ℕ0 ∧ ℕ0 ⊆ ℂ ) → 0 = ( 0g ‘ ( ℂfld ↾s ℕ0 ) ) )
59	55 56 12 58	mp3an	⊢ 0 = ( 0g ‘ ( ℂfld ↾s ℕ0 ) )
60	47 48 51 53 59	issrg	⊢ ( ( ℂfld ↾s ℕ0 ) ∈ SRing ↔ ( ( ℂfld ↾s ℕ0 ) ∈ CMnd ∧ ( mulGrp ‘ ( ℂfld ↾s ℕ0 ) ) ∈ Mnd ∧ ∀ 𝑥 ∈ ℕ0 ( ∀ 𝑦 ∈ ℕ0 ∀ 𝑧 ∈ ℕ0 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( 0 · 𝑥 ) = 0 ∧ ( 𝑥 · 0 ) = 0 ) ) ) )
61	7 30 45 60	mpbir3an	⊢ ( ℂfld ↾s ℕ0 ) ∈ SRing