This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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