Theorem nn0mnd

Description: The set of nonnegative integers under (complex) addition is a monoid. Example in Lang p. 6. Remark: M could have also been written as ` ( CCfld |``s NN0 ) ` . (Contributed by AV, 27-Dec-2023)

	Ref	Expression
Hypothesis	nn0mnd.g	⊢ 𝑀 = { ⟨ ( Base ‘ ndx ) , ℕ0 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ }
Assertion	nn0mnd	⊢ 𝑀 ∈ Mnd

Proof

Step	Hyp	Ref	Expression
1		nn0mnd.g	⊢ 𝑀 = { ⟨ ( Base ‘ ndx ) , ℕ0 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ }
2		nn0addcl	⊢ ( ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) → ( 𝑥 + 𝑦 ) ∈ ℕ0 )
3		nn0cn	⊢ ( 𝑥 ∈ ℕ0 → 𝑥 ∈ ℂ )
4		nn0cn	⊢ ( 𝑦 ∈ ℕ0 → 𝑦 ∈ ℂ )
5		nn0cn	⊢ ( 𝑧 ∈ ℕ0 → 𝑧 ∈ ℂ )
6	3 4 5	3anim123i	⊢ ( ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ∧ 𝑧 ∈ ℕ0 ) → ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) )
7	6	3expa	⊢ ( ( ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑧 ∈ ℕ0 ) → ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) )
8		addass	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
9	7 8	syl	⊢ ( ( ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑧 ∈ ℕ0 ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
10	9	ralrimiva	⊢ ( ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) → ∀ 𝑧 ∈ ℕ0 ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
11	2 10	jca	⊢ ( ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) → ( ( 𝑥 + 𝑦 ) ∈ ℕ0 ∧ ∀ 𝑧 ∈ ℕ0 ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) ) )
12	11	rgen2	⊢ ∀ 𝑥 ∈ ℕ0 ∀ 𝑦 ∈ ℕ0 ( ( 𝑥 + 𝑦 ) ∈ ℕ0 ∧ ∀ 𝑧 ∈ ℕ0 ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
13		c0ex	⊢ 0 ∈ V
14		eleq1	⊢ ( 𝑒 = 0 → ( 𝑒 ∈ ℕ0 ↔ 0 ∈ ℕ0 ) )
15		oveq1	⊢ ( 𝑒 = 0 → ( 𝑒 + 𝑥 ) = ( 0 + 𝑥 ) )
16	15	eqeq1d	⊢ ( 𝑒 = 0 → ( ( 𝑒 + 𝑥 ) = 𝑥 ↔ ( 0 + 𝑥 ) = 𝑥 ) )
17		oveq2	⊢ ( 𝑒 = 0 → ( 𝑥 + 𝑒 ) = ( 𝑥 + 0 ) )
18	17	eqeq1d	⊢ ( 𝑒 = 0 → ( ( 𝑥 + 𝑒 ) = 𝑥 ↔ ( 𝑥 + 0 ) = 𝑥 ) )
19	16 18	anbi12d	⊢ ( 𝑒 = 0 → ( ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ↔ ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) ) )
20	19	ralbidv	⊢ ( 𝑒 = 0 → ( ∀ 𝑥 ∈ ℕ0 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ↔ ∀ 𝑥 ∈ ℕ0 ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) ) )
21	14 20	anbi12d	⊢ ( 𝑒 = 0 → ( ( 𝑒 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) ↔ ( 0 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) ) ) )
22		0nn0	⊢ 0 ∈ ℕ0
23	3	addid2d	⊢ ( 𝑥 ∈ ℕ0 → ( 0 + 𝑥 ) = 𝑥 )
24	3	addid1d	⊢ ( 𝑥 ∈ ℕ0 → ( 𝑥 + 0 ) = 𝑥 )
25	23 24	jca	⊢ ( 𝑥 ∈ ℕ0 → ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) )
26	25	rgen	⊢ ∀ 𝑥 ∈ ℕ0 ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 )
27	22 26	pm3.2i	⊢ ( 0 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) )
28	13 21 27	ceqsexv2d	⊢ ∃ 𝑒 ( 𝑒 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) )
29		df-rex	⊢ ( ∃ 𝑒 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ↔ ∃ 𝑒 ( 𝑒 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) )
30	28 29	mpbir	⊢ ∃ 𝑒 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 )
31	12 30	pm3.2i	⊢ ( ∀ 𝑥 ∈ ℕ0 ∀ 𝑦 ∈ ℕ0 ( ( 𝑥 + 𝑦 ) ∈ ℕ0 ∧ ∀ 𝑧 ∈ ℕ0 ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) ) ∧ ∃ 𝑒 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) )
32		nn0ex	⊢ ℕ0 ∈ V
33	1	grpbase	⊢ ( ℕ0 ∈ V → ℕ0 = ( Base ‘ 𝑀 ) )
34	32 33	ax-mp	⊢ ℕ0 = ( Base ‘ 𝑀 )
35		addex	⊢ + ∈ V
36	1	grpplusg	⊢ ( + ∈ V → + = ( +g ‘ 𝑀 ) )
37	35 36	ax-mp	⊢ + = ( +g ‘ 𝑀 )
38	34 37	ismnd	⊢ ( 𝑀 ∈ Mnd ↔ ( ∀ 𝑥 ∈ ℕ0 ∀ 𝑦 ∈ ℕ0 ( ( 𝑥 + 𝑦 ) ∈ ℕ0 ∧ ∀ 𝑧 ∈ ℕ0 ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) ) ∧ ∃ 𝑒 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) )
39	31 38	mpbir	⊢ 𝑀 ∈ Mnd