Metamath Proof Explorer

Theorem 2zrngmsgrp

Description: R is a (multiplicative) semigroup. (Contributed by AV, 4-Feb-2020)

Ref Expression
Hypotheses 2zrng.e 
|- E = { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) }
2zrngbas.r 
|- R = ( CCfld |`s E )
2zrngmmgm.1 
|- M = ( mulGrp ` R )
Assertion 2zrngmsgrp 
|- M e. Smgrp

Proof

Step Hyp Ref Expression
1 2zrng.e 
 |-  E = { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) }
2 2zrngbas.r 
 |-  R = ( CCfld |`s E )
3 2zrngmmgm.1 
 |-  M = ( mulGrp ` R )
4 1 2 3 2zrngmmgm 
 |-  M e. Mgm
5 elrabi 
 |-  ( a e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } -> a e. ZZ )
6 elrabi 
 |-  ( y e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } -> y e. ZZ )
7 elrabi 
 |-  ( b e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } -> b e. ZZ )
8 5 6 7 3anim123i 
 |-  ( ( a e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } /\ y e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } /\ b e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } ) -> ( a e. ZZ /\ y e. ZZ /\ b e. ZZ ) )
9 zcn 
 |-  ( a e. ZZ -> a e. CC )
10 zcn 
 |-  ( y e. ZZ -> y e. CC )
11 zcn 
 |-  ( b e. ZZ -> b e. CC )
12 9 10 11 3anim123i 
 |-  ( ( a e. ZZ /\ y e. ZZ /\ b e. ZZ ) -> ( a e. CC /\ y e. CC /\ b e. CC ) )
13 mulass 
 |-  ( ( a e. CC /\ y e. CC /\ b e. CC ) -> ( ( a x. y ) x. b ) = ( a x. ( y x. b ) ) )
14 8 12 13 3syl 
 |-  ( ( a e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } /\ y e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } /\ b e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } ) -> ( ( a x. y ) x. b ) = ( a x. ( y x. b ) ) )
15 14 rgen3 
 |-  A. a e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } A. y e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } A. b e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } ( ( a x. y ) x. b ) = ( a x. ( y x. b ) )
16 1 2 2zrngbas 
 |-  E = ( Base ` R )
17 3 16 mgpbas 
 |-  E = ( Base ` M )
18 1 17 eqtr3i 
 |-  { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } = ( Base ` M )
19 1 2 2zrngmul 
 |-  x. = ( .r ` R )
20 3 19 mgpplusg 
 |-  x. = ( +g ` M )
21 18 20 issgrp 
 |-  ( M e. Smgrp <-> ( M e. Mgm /\ A. a e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } A. y e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } A. b e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } ( ( a x. y ) x. b ) = ( a x. ( y x. b ) ) ) )
22 4 15 21 mpbir2an 
 |-  M e. Smgrp