Metamath Proof Explorer

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 
|- M = { <. ( Base ` ndx ) , NN0 >. , <. ( +g ` ndx ) , + >. }
Assertion nn0mnd 
|- M e. Mnd

Proof

Step Hyp Ref Expression
1 nn0mnd.g 
 |-  M = { <. ( Base ` ndx ) , NN0 >. , <. ( +g ` ndx ) , + >. }
2 nn0addcl 
 |-  ( ( x e. NN0 /\ y e. NN0 ) -> ( x + y ) e. NN0 )
3 nn0cn 
 |-  ( x e. NN0 -> x e. CC )
4 nn0cn 
 |-  ( y e. NN0 -> y e. CC )
5 nn0cn 
 |-  ( z e. NN0 -> z e. CC )
6 3 4 5 3anim123i 
 |-  ( ( x e. NN0 /\ y e. NN0 /\ z e. NN0 ) -> ( x e. CC /\ y e. CC /\ z e. CC ) )
7 6 3expa 
 |-  ( ( ( x e. NN0 /\ y e. NN0 ) /\ z e. NN0 ) -> ( x e. CC /\ y e. CC /\ z e. CC ) )
8 addass 
 |-  ( ( x e. CC /\ y e. CC /\ z e. CC ) -> ( ( x + y ) + z ) = ( x + ( y + z ) ) )
9 7 8 syl 
 |-  ( ( ( x e. NN0 /\ y e. NN0 ) /\ z e. NN0 ) -> ( ( x + y ) + z ) = ( x + ( y + z ) ) )
10 9 ralrimiva 
 |-  ( ( x e. NN0 /\ y e. NN0 ) -> A. z e. NN0 ( ( x + y ) + z ) = ( x + ( y + z ) ) )
11 2 10 jca 
 |-  ( ( x e. NN0 /\ y e. NN0 ) -> ( ( x + y ) e. NN0 /\ A. z e. NN0 ( ( x + y ) + z ) = ( x + ( y + z ) ) ) )
12 11 rgen2 
 |-  A. x e. NN0 A. y e. NN0 ( ( x + y ) e. NN0 /\ A. z e. NN0 ( ( x + y ) + z ) = ( x + ( y + z ) ) )
13 c0ex 
 |-  0 e. _V
14 eleq1 
 |-  ( e = 0 -> ( e e. NN0 <-> 0 e. NN0 ) )
15 oveq1 
 |-  ( e = 0 -> ( e + x ) = ( 0 + x ) )
16 15 eqeq1d 
 |-  ( e = 0 -> ( ( e + x ) = x <-> ( 0 + x ) = x ) )
17 oveq2 
 |-  ( e = 0 -> ( x + e ) = ( x + 0 ) )
18 17 eqeq1d 
 |-  ( e = 0 -> ( ( x + e ) = x <-> ( x + 0 ) = x ) )
19 16 18 anbi12d 
 |-  ( e = 0 -> ( ( ( e + x ) = x /\ ( x + e ) = x ) <-> ( ( 0 + x ) = x /\ ( x + 0 ) = x ) ) )
20 19 ralbidv 
 |-  ( e = 0 -> ( A. x e. NN0 ( ( e + x ) = x /\ ( x + e ) = x ) <-> A. x e. NN0 ( ( 0 + x ) = x /\ ( x + 0 ) = x ) ) )
21 14 20 anbi12d 
 |-  ( e = 0 -> ( ( e e. NN0 /\ A. x e. NN0 ( ( e + x ) = x /\ ( x + e ) = x ) ) <-> ( 0 e. NN0 /\ A. x e. NN0 ( ( 0 + x ) = x /\ ( x + 0 ) = x ) ) ) )
22 0nn0 
 |-  0 e. NN0
23 3 addid2d 
 |-  ( x e. NN0 -> ( 0 + x ) = x )
24 3 addid1d 
 |-  ( x e. NN0 -> ( x + 0 ) = x )
25 23 24 jca 
 |-  ( x e. NN0 -> ( ( 0 + x ) = x /\ ( x + 0 ) = x ) )
26 25 rgen 
 |-  A. x e. NN0 ( ( 0 + x ) = x /\ ( x + 0 ) = x )
27 22 26 pm3.2i 
 |-  ( 0 e. NN0 /\ A. x e. NN0 ( ( 0 + x ) = x /\ ( x + 0 ) = x ) )
28 13 21 27 ceqsexv2d 
 |-  E. e ( e e. NN0 /\ A. x e. NN0 ( ( e + x ) = x /\ ( x + e ) = x ) )
29 df-rex 
 |-  ( E. e e. NN0 A. x e. NN0 ( ( e + x ) = x /\ ( x + e ) = x ) <-> E. e ( e e. NN0 /\ A. x e. NN0 ( ( e + x ) = x /\ ( x + e ) = x ) ) )
30 28 29 mpbir 
 |-  E. e e. NN0 A. x e. NN0 ( ( e + x ) = x /\ ( x + e ) = x )
31 12 30 pm3.2i 
 |-  ( A. x e. NN0 A. y e. NN0 ( ( x + y ) e. NN0 /\ A. z e. NN0 ( ( x + y ) + z ) = ( x + ( y + z ) ) ) /\ E. e e. NN0 A. x e. NN0 ( ( e + x ) = x /\ ( x + e ) = x ) )
32 nn0ex 
 |-  NN0 e. _V
33 1 grpbase 
 |-  ( NN0 e. _V -> NN0 = ( Base ` M ) )
34 32 33 ax-mp 
 |-  NN0 = ( Base ` M )
35 addex 
 |-  + e. _V
36 1 grpplusg 
 |-  ( + e. _V -> + = ( +g ` M ) )
37 35 36 ax-mp 
 |-  + = ( +g ` M )
38 34 37 ismnd 
 |-  ( M e. Mnd <-> ( A. x e. NN0 A. y e. NN0 ( ( x + y ) e. NN0 /\ A. z e. NN0 ( ( x + y ) + z ) = ( x + ( y + z ) ) ) /\ E. e e. NN0 A. x e. NN0 ( ( e + x ) = x /\ ( x + e ) = x ) ) )
39 31 38 mpbir 
 |-  M e. Mnd