Metamath Proof Explorer

Theorem 2zrngmmgm

Description: R is a (multiplicative) magma. (Contributed by AV, 11-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 2zrngmmgm 
|- M e. Mgm

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 eqeq1 
 |-  ( z = a -> ( z = ( 2 x. x ) <-> a = ( 2 x. x ) ) )
5 4 rexbidv 
 |-  ( z = a -> ( E. x e. ZZ z = ( 2 x. x ) <-> E. x e. ZZ a = ( 2 x. x ) ) )
6 5 1 elrab2 
 |-  ( a e. E <-> ( a e. ZZ /\ E. x e. ZZ a = ( 2 x. x ) ) )
7 eqeq1 
 |-  ( z = b -> ( z = ( 2 x. x ) <-> b = ( 2 x. x ) ) )
8 7 rexbidv 
 |-  ( z = b -> ( E. x e. ZZ z = ( 2 x. x ) <-> E. x e. ZZ b = ( 2 x. x ) ) )
9 8 1 elrab2 
 |-  ( b e. E <-> ( b e. ZZ /\ E. x e. ZZ b = ( 2 x. x ) ) )
10 zmulcl 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> ( a x. b ) e. ZZ )
11 10 ad2ant2r 
 |-  ( ( ( a e. ZZ /\ E. x e. ZZ a = ( 2 x. x ) ) /\ ( b e. ZZ /\ E. x e. ZZ b = ( 2 x. x ) ) ) -> ( a x. b ) e. ZZ )
12 nfv 
 |-  F/ x a e. ZZ
13 nfv 
 |-  F/ x b e. ZZ
14 nfre1 
 |-  F/ x E. x e. ZZ b = ( 2 x. x )
15 13 14 nfan 
 |-  F/ x ( b e. ZZ /\ E. x e. ZZ b = ( 2 x. x ) )
16 nfv 
 |-  F/ x E. y e. ZZ ( a x. b ) = ( 2 x. y )
17 15 16 nfim 
 |-  F/ x ( ( b e. ZZ /\ E. x e. ZZ b = ( 2 x. x ) ) -> E. y e. ZZ ( a x. b ) = ( 2 x. y ) )
18 12 17 nfim 
 |-  F/ x ( a e. ZZ -> ( ( b e. ZZ /\ E. x e. ZZ b = ( 2 x. x ) ) -> E. y e. ZZ ( a x. b ) = ( 2 x. y ) ) )
19 simpll 
 |-  ( ( ( x e. ZZ /\ a = ( 2 x. x ) ) /\ a e. ZZ ) -> x e. ZZ )
20 simpl 
 |-  ( ( b e. ZZ /\ E. x e. ZZ b = ( 2 x. x ) ) -> b e. ZZ )
21 zmulcl 
 |-  ( ( x e. ZZ /\ b e. ZZ ) -> ( x x. b ) e. ZZ )
22 19 20 21 syl2an 
 |-  ( ( ( ( x e. ZZ /\ a = ( 2 x. x ) ) /\ a e. ZZ ) /\ ( b e. ZZ /\ E. x e. ZZ b = ( 2 x. x ) ) ) -> ( x x. b ) e. ZZ )
23 oveq2 
 |-  ( y = ( x x. b ) -> ( 2 x. y ) = ( 2 x. ( x x. b ) ) )
24 23 eqeq2d 
 |-  ( y = ( x x. b ) -> ( ( a x. b ) = ( 2 x. y ) <-> ( a x. b ) = ( 2 x. ( x x. b ) ) ) )
25 24 adantl 
 |-  ( ( ( ( ( x e. ZZ /\ a = ( 2 x. x ) ) /\ a e. ZZ ) /\ ( b e. ZZ /\ E. x e. ZZ b = ( 2 x. x ) ) ) /\ y = ( x x. b ) ) -> ( ( a x. b ) = ( 2 x. y ) <-> ( a x. b ) = ( 2 x. ( x x. b ) ) ) )
26 oveq1 
 |-  ( a = ( 2 x. x ) -> ( a x. b ) = ( ( 2 x. x ) x. b ) )
27 26 ad3antlr 
 |-  ( ( ( ( x e. ZZ /\ a = ( 2 x. x ) ) /\ a e. ZZ ) /\ ( b e. ZZ /\ E. x e. ZZ b = ( 2 x. x ) ) ) -> ( a x. b ) = ( ( 2 x. x ) x. b ) )
28 2cnd 
 |-  ( ( ( ( x e. ZZ /\ a = ( 2 x. x ) ) /\ a e. ZZ ) /\ ( b e. ZZ /\ E. x e. ZZ b = ( 2 x. x ) ) ) -> 2 e. CC )
29 zcn 
 |-  ( x e. ZZ -> x e. CC )
30 29 ad3antrrr 
 |-  ( ( ( ( x e. ZZ /\ a = ( 2 x. x ) ) /\ a e. ZZ ) /\ ( b e. ZZ /\ E. x e. ZZ b = ( 2 x. x ) ) ) -> x e. CC )
31 zcn 
 |-  ( b e. ZZ -> b e. CC )
32 31 adantr 
 |-  ( ( b e. ZZ /\ E. x e. ZZ b = ( 2 x. x ) ) -> b e. CC )
33 32 adantl 
 |-  ( ( ( ( x e. ZZ /\ a = ( 2 x. x ) ) /\ a e. ZZ ) /\ ( b e. ZZ /\ E. x e. ZZ b = ( 2 x. x ) ) ) -> b e. CC )
34 28 30 33 mulassd 
 |-  ( ( ( ( x e. ZZ /\ a = ( 2 x. x ) ) /\ a e. ZZ ) /\ ( b e. ZZ /\ E. x e. ZZ b = ( 2 x. x ) ) ) -> ( ( 2 x. x ) x. b ) = ( 2 x. ( x x. b ) ) )
35 27 34 eqtrd 
 |-  ( ( ( ( x e. ZZ /\ a = ( 2 x. x ) ) /\ a e. ZZ ) /\ ( b e. ZZ /\ E. x e. ZZ b = ( 2 x. x ) ) ) -> ( a x. b ) = ( 2 x. ( x x. b ) ) )
36 22 25 35 rspcedvd 
 |-  ( ( ( ( x e. ZZ /\ a = ( 2 x. x ) ) /\ a e. ZZ ) /\ ( b e. ZZ /\ E. x e. ZZ b = ( 2 x. x ) ) ) -> E. y e. ZZ ( a x. b ) = ( 2 x. y ) )
37 36 exp41 
 |-  ( x e. ZZ -> ( a = ( 2 x. x ) -> ( a e. ZZ -> ( ( b e. ZZ /\ E. x e. ZZ b = ( 2 x. x ) ) -> E. y e. ZZ ( a x. b ) = ( 2 x. y ) ) ) ) )
38 18 37 rexlimi 
 |-  ( E. x e. ZZ a = ( 2 x. x ) -> ( a e. ZZ -> ( ( b e. ZZ /\ E. x e. ZZ b = ( 2 x. x ) ) -> E. y e. ZZ ( a x. b ) = ( 2 x. y ) ) ) )
39 38 impcom 
 |-  ( ( a e. ZZ /\ E. x e. ZZ a = ( 2 x. x ) ) -> ( ( b e. ZZ /\ E. x e. ZZ b = ( 2 x. x ) ) -> E. y e. ZZ ( a x. b ) = ( 2 x. y ) ) )
40 39 imp 
 |-  ( ( ( a e. ZZ /\ E. x e. ZZ a = ( 2 x. x ) ) /\ ( b e. ZZ /\ E. x e. ZZ b = ( 2 x. x ) ) ) -> E. y e. ZZ ( a x. b ) = ( 2 x. y ) )
41 eqeq1 
 |-  ( z = ( a x. b ) -> ( z = ( 2 x. x ) <-> ( a x. b ) = ( 2 x. x ) ) )
42 41 rexbidv 
 |-  ( z = ( a x. b ) -> ( E. x e. ZZ z = ( 2 x. x ) <-> E. x e. ZZ ( a x. b ) = ( 2 x. x ) ) )
43 42 1 elrab2 
 |-  ( ( a x. b ) e. E <-> ( ( a x. b ) e. ZZ /\ E. x e. ZZ ( a x. b ) = ( 2 x. x ) ) )
44 oveq2 
 |-  ( x = y -> ( 2 x. x ) = ( 2 x. y ) )
45 44 eqeq2d 
 |-  ( x = y -> ( ( a x. b ) = ( 2 x. x ) <-> ( a x. b ) = ( 2 x. y ) ) )
46 45 cbvrexvw 
 |-  ( E. x e. ZZ ( a x. b ) = ( 2 x. x ) <-> E. y e. ZZ ( a x. b ) = ( 2 x. y ) )
47 46 anbi2i 
 |-  ( ( ( a x. b ) e. ZZ /\ E. x e. ZZ ( a x. b ) = ( 2 x. x ) ) <-> ( ( a x. b ) e. ZZ /\ E. y e. ZZ ( a x. b ) = ( 2 x. y ) ) )
48 43 47 bitri 
 |-  ( ( a x. b ) e. E <-> ( ( a x. b ) e. ZZ /\ E. y e. ZZ ( a x. b ) = ( 2 x. y ) ) )
49 11 40 48 sylanbrc 
 |-  ( ( ( a e. ZZ /\ E. x e. ZZ a = ( 2 x. x ) ) /\ ( b e. ZZ /\ E. x e. ZZ b = ( 2 x. x ) ) ) -> ( a x. b ) e. E )
50 6 9 49 syl2anb 
 |-  ( ( a e. E /\ b e. E ) -> ( a x. b ) e. E )
51 50 rgen2 
 |-  A. a e. E A. b e. E ( a x. b ) e. E
52 1 0even 
 |-  0 e. E
53 1 2 2zrngbas 
 |-  E = ( Base ` R )
54 3 53 mgpbas 
 |-  E = ( Base ` M )
55 1 2 2zrngmul 
 |-  x. = ( .r ` R )
56 3 55 mgpplusg 
 |-  x. = ( +g ` M )
57 54 56 ismgmn0 
 |-  ( 0 e. E -> ( M e. Mgm <-> A. a e. E A. b e. E ( a x. b ) e. E ) )
58 52 57 ax-mp 
 |-  ( M e. Mgm <-> A. a e. E A. b e. E ( a x. b ) e. E )
59 51 58 mpbir 
 |-  M e. Mgm