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 
|- ( CCfld |`s NN0 ) e. SRing

Proof

Step Hyp Ref Expression
1 cnring 
 |-  CCfld e. Ring
2 ringcmn 
 |-  ( CCfld e. Ring -> CCfld e. CMnd )
3 1 2 ax-mp 
 |-  CCfld e. CMnd
4 nn0subm 
 |-  NN0 e. ( SubMnd ` CCfld )
5 eqid 
 |-  ( CCfld |`s NN0 ) = ( CCfld |`s NN0 )
6 5 submcmn 
 |-  ( ( CCfld e. CMnd /\ NN0 e. ( SubMnd ` CCfld ) ) -> ( CCfld |`s NN0 ) e. CMnd )
7 3 4 6 mp2an 
 |-  ( CCfld |`s NN0 ) e. CMnd
8 nn0ex 
 |-  NN0 e. _V
9 eqid 
 |-  ( mulGrp ` CCfld ) = ( mulGrp ` CCfld )
10 5 9 mgpress 
 |-  ( ( CCfld e. CMnd /\ NN0 e. _V ) -> ( ( mulGrp ` CCfld ) |`s NN0 ) = ( mulGrp ` ( CCfld |`s NN0 ) ) )
11 3 8 10 mp2an 
 |-  ( ( mulGrp ` CCfld ) |`s NN0 ) = ( mulGrp ` ( CCfld |`s NN0 ) )
12 nn0sscn 
 |-  NN0 C_ CC
13 1nn0 
 |-  1 e. NN0
14 nn0mulcl 
 |-  ( ( x e. NN0 /\ y e. NN0 ) -> ( x x. y ) e. NN0 )
15 14 rgen2 
 |-  A. x e. NN0 A. y e. NN0 ( x x. y ) e. NN0
16 9 ringmgp 
 |-  ( CCfld e. Ring -> ( mulGrp ` CCfld ) e. Mnd )
17 1 16 ax-mp 
 |-  ( mulGrp ` CCfld ) e. Mnd
18 cnfldbas 
 |-  CC = ( Base ` CCfld )
19 9 18 mgpbas 
 |-  CC = ( Base ` ( mulGrp ` CCfld ) )
20 cnfld1 
 |-  1 = ( 1r ` CCfld )
21 9 20 ringidval 
 |-  1 = ( 0g ` ( mulGrp ` CCfld ) )
22 cnfldmul 
 |-  x. = ( .r ` CCfld )
23 9 22 mgpplusg 
 |-  x. = ( +g ` ( mulGrp ` CCfld ) )
24 19 21 23 issubm 
 |-  ( ( mulGrp ` CCfld ) e. Mnd -> ( NN0 e. ( SubMnd ` ( mulGrp ` CCfld ) ) <-> ( NN0 C_ CC /\ 1 e. NN0 /\ A. x e. NN0 A. y e. NN0 ( x x. y ) e. NN0 ) ) )
25 17 24 ax-mp 
 |-  ( NN0 e. ( SubMnd ` ( mulGrp ` CCfld ) ) <-> ( NN0 C_ CC /\ 1 e. NN0 /\ A. x e. NN0 A. y e. NN0 ( x x. y ) e. NN0 ) )
26 12 13 15 25 mpbir3an 
 |-  NN0 e. ( SubMnd ` ( mulGrp ` CCfld ) )
27 eqid 
 |-  ( ( mulGrp ` CCfld ) |`s NN0 ) = ( ( mulGrp ` CCfld ) |`s NN0 )
28 27 submmnd 
 |-  ( NN0 e. ( SubMnd ` ( mulGrp ` CCfld ) ) -> ( ( mulGrp ` CCfld ) |`s NN0 ) e. Mnd )
29 26 28 ax-mp 
 |-  ( ( mulGrp ` CCfld ) |`s NN0 ) e. Mnd
30 11 29 eqeltrri 
 |-  ( mulGrp ` ( CCfld |`s NN0 ) ) e. Mnd
31 simpl 
 |-  ( ( x e. NN0 /\ ( y e. NN0 /\ z e. NN0 ) ) -> x e. NN0 )
32 31 nn0cnd 
 |-  ( ( x e. NN0 /\ ( y e. NN0 /\ z e. NN0 ) ) -> x e. CC )
33 simprl 
 |-  ( ( x e. NN0 /\ ( y e. NN0 /\ z e. NN0 ) ) -> y e. NN0 )
34 33 nn0cnd 
 |-  ( ( x e. NN0 /\ ( y e. NN0 /\ z e. NN0 ) ) -> y e. CC )
35 simprr 
 |-  ( ( x e. NN0 /\ ( y e. NN0 /\ z e. NN0 ) ) -> z e. NN0 )
36 35 nn0cnd 
 |-  ( ( x e. NN0 /\ ( y e. NN0 /\ z e. NN0 ) ) -> z e. CC )
37 32 34 36 adddid 
 |-  ( ( x e. NN0 /\ ( y e. NN0 /\ z e. NN0 ) ) -> ( x x. ( y + z ) ) = ( ( x x. y ) + ( x x. z ) ) )
38 32 34 36 adddird 
 |-  ( ( x e. NN0 /\ ( y e. NN0 /\ z e. NN0 ) ) -> ( ( x + y ) x. z ) = ( ( x x. z ) + ( y x. z ) ) )
39 37 38 jca 
 |-  ( ( x e. NN0 /\ ( y e. NN0 /\ z e. NN0 ) ) -> ( ( x x. ( y + z ) ) = ( ( x x. y ) + ( x x. z ) ) /\ ( ( x + y ) x. z ) = ( ( x x. z ) + ( y x. z ) ) ) )
40 39 ralrimivva 
 |-  ( x e. NN0 -> A. y e. NN0 A. z e. NN0 ( ( x x. ( y + z ) ) = ( ( x x. y ) + ( x x. z ) ) /\ ( ( x + y ) x. z ) = ( ( x x. z ) + ( y x. z ) ) ) )
41 nn0cn 
 |-  ( x e. NN0 -> x e. CC )
42 41 mul02d 
 |-  ( x e. NN0 -> ( 0 x. x ) = 0 )
43 41 mul01d 
 |-  ( x e. NN0 -> ( x x. 0 ) = 0 )
44 40 42 43 jca32 
 |-  ( x e. NN0 -> ( A. y e. NN0 A. z e. NN0 ( ( x x. ( y + z ) ) = ( ( x x. y ) + ( x x. z ) ) /\ ( ( x + y ) x. z ) = ( ( x x. z ) + ( y x. z ) ) ) /\ ( ( 0 x. x ) = 0 /\ ( x x. 0 ) = 0 ) ) )
45 44 rgen 
 |-  A. x e. NN0 ( A. y e. NN0 A. z e. NN0 ( ( x x. ( y + z ) ) = ( ( x x. y ) + ( x x. z ) ) /\ ( ( x + y ) x. z ) = ( ( x x. z ) + ( y x. z ) ) ) /\ ( ( 0 x. x ) = 0 /\ ( x x. 0 ) = 0 ) )
46 5 18 ressbas2 
 |-  ( NN0 C_ CC -> NN0 = ( Base ` ( CCfld |`s NN0 ) ) )
47 12 46 ax-mp 
 |-  NN0 = ( Base ` ( CCfld |`s NN0 ) )
48 eqid 
 |-  ( mulGrp ` ( CCfld |`s NN0 ) ) = ( mulGrp ` ( CCfld |`s NN0 ) )
49 cnfldadd 
 |-  + = ( +g ` CCfld )
50 5 49 ressplusg 
 |-  ( NN0 e. _V -> + = ( +g ` ( CCfld |`s NN0 ) ) )
51 8 50 ax-mp 
 |-  + = ( +g ` ( CCfld |`s NN0 ) )
52 5 22 ressmulr 
 |-  ( NN0 e. _V -> x. = ( .r ` ( CCfld |`s NN0 ) ) )
53 8 52 ax-mp 
 |-  x. = ( .r ` ( CCfld |`s NN0 ) )
54 ringmnd 
 |-  ( CCfld e. Ring -> CCfld e. Mnd )
55 1 54 ax-mp 
 |-  CCfld e. Mnd
56 0nn0 
 |-  0 e. NN0
57 cnfld0 
 |-  0 = ( 0g ` CCfld )
58 5 18 57 ress0g 
 |-  ( ( CCfld e. Mnd /\ 0 e. NN0 /\ NN0 C_ CC ) -> 0 = ( 0g ` ( CCfld |`s NN0 ) ) )
59 55 56 12 58 mp3an 
 |-  0 = ( 0g ` ( CCfld |`s NN0 ) )
60 47 48 51 53 59 issrg 
 |-  ( ( CCfld |`s NN0 ) e. SRing <-> ( ( CCfld |`s NN0 ) e. CMnd /\ ( mulGrp ` ( CCfld |`s NN0 ) ) e. Mnd /\ A. x e. NN0 ( A. y e. NN0 A. z e. NN0 ( ( x x. ( y + z ) ) = ( ( x x. y ) + ( x x. z ) ) /\ ( ( x + y ) x. z ) = ( ( x x. z ) + ( y x. z ) ) ) /\ ( ( 0 x. x ) = 0 /\ ( x x. 0 ) = 0 ) ) ) )
61 7 30 45 60 mpbir3an 
 |-  ( CCfld |`s NN0 ) e. SRing