Metamath Proof Explorer

Theorem 2zrngamgm

Description: R is an (additive) magma. (Contributed by AV, 6-Jan-2020)

Ref Expression
Hypotheses 2zrng.e 
|- E = { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) }
2zrngbas.r 
|- R = ( CCfld |`s E )
Assertion 2zrngamgm 
|- R 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 eqeq1 
 |-  ( z = a -> ( z = ( 2 x. x ) <-> a = ( 2 x. x ) ) )
4 3 rexbidv 
 |-  ( z = a -> ( E. x e. ZZ z = ( 2 x. x ) <-> E. x e. ZZ a = ( 2 x. x ) ) )
5 4 1 elrab2 
 |-  ( a e. E <-> ( a e. ZZ /\ E. x e. ZZ a = ( 2 x. x ) ) )
6 eqeq1 
 |-  ( z = b -> ( z = ( 2 x. x ) <-> b = ( 2 x. x ) ) )
7 6 rexbidv 
 |-  ( z = b -> ( E. x e. ZZ z = ( 2 x. x ) <-> E. x e. ZZ b = ( 2 x. x ) ) )
8 7 1 elrab2 
 |-  ( b e. E <-> ( b e. ZZ /\ E. x e. ZZ b = ( 2 x. x ) ) )
9 oveq2 
 |-  ( x = y -> ( 2 x. x ) = ( 2 x. y ) )
10 9 eqeq2d 
 |-  ( x = y -> ( a = ( 2 x. x ) <-> a = ( 2 x. y ) ) )
11 10 cbvrexvw 
 |-  ( E. x e. ZZ a = ( 2 x. x ) <-> E. y e. ZZ a = ( 2 x. y ) )
12 zaddcl 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> ( a + b ) e. ZZ )
13 12 ancoms 
 |-  ( ( b e. ZZ /\ a e. ZZ ) -> ( a + b ) e. ZZ )
14 13 adantr 
 |-  ( ( ( b e. ZZ /\ a e. ZZ ) /\ ( E. x e. ZZ b = ( 2 x. x ) /\ E. y e. ZZ a = ( 2 x. y ) ) ) -> ( a + b ) e. ZZ )
15 simpl 
 |-  ( ( y e. ZZ /\ a = ( 2 x. y ) ) -> y e. ZZ )
16 simpl 
 |-  ( ( x e. ZZ /\ b = ( 2 x. x ) ) -> x e. ZZ )
17 zaddcl 
 |-  ( ( y e. ZZ /\ x e. ZZ ) -> ( y + x ) e. ZZ )
18 15 16 17 syl2anr 
 |-  ( ( ( x e. ZZ /\ b = ( 2 x. x ) ) /\ ( y e. ZZ /\ a = ( 2 x. y ) ) ) -> ( y + x ) e. ZZ )
19 18 adantr 
 |-  ( ( ( ( x e. ZZ /\ b = ( 2 x. x ) ) /\ ( y e. ZZ /\ a = ( 2 x. y ) ) ) /\ ( b e. ZZ /\ a e. ZZ ) ) -> ( y + x ) e. ZZ )
20 oveq2 
 |-  ( z = ( y + x ) -> ( 2 x. z ) = ( 2 x. ( y + x ) ) )
21 20 eqeq2d 
 |-  ( z = ( y + x ) -> ( ( 2 x. ( y + x ) ) = ( 2 x. z ) <-> ( 2 x. ( y + x ) ) = ( 2 x. ( y + x ) ) ) )
22 21 adantl 
 |-  ( ( ( ( ( x e. ZZ /\ b = ( 2 x. x ) ) /\ ( y e. ZZ /\ a = ( 2 x. y ) ) ) /\ ( b e. ZZ /\ a e. ZZ ) ) /\ z = ( y + x ) ) -> ( ( 2 x. ( y + x ) ) = ( 2 x. z ) <-> ( 2 x. ( y + x ) ) = ( 2 x. ( y + x ) ) ) )
23 eqidd 
 |-  ( ( ( ( x e. ZZ /\ b = ( 2 x. x ) ) /\ ( y e. ZZ /\ a = ( 2 x. y ) ) ) /\ ( b e. ZZ /\ a e. ZZ ) ) -> ( 2 x. ( y + x ) ) = ( 2 x. ( y + x ) ) )
24 19 22 23 rspcedvd 
 |-  ( ( ( ( x e. ZZ /\ b = ( 2 x. x ) ) /\ ( y e. ZZ /\ a = ( 2 x. y ) ) ) /\ ( b e. ZZ /\ a e. ZZ ) ) -> E. z e. ZZ ( 2 x. ( y + x ) ) = ( 2 x. z ) )
25 simpr 
 |-  ( ( y e. ZZ /\ a = ( 2 x. y ) ) -> a = ( 2 x. y ) )
26 simpr 
 |-  ( ( x e. ZZ /\ b = ( 2 x. x ) ) -> b = ( 2 x. x ) )
27 25 26 oveqan12rd 
 |-  ( ( ( x e. ZZ /\ b = ( 2 x. x ) ) /\ ( y e. ZZ /\ a = ( 2 x. y ) ) ) -> ( a + b ) = ( ( 2 x. y ) + ( 2 x. x ) ) )
28 27 adantr 
 |-  ( ( ( ( x e. ZZ /\ b = ( 2 x. x ) ) /\ ( y e. ZZ /\ a = ( 2 x. y ) ) ) /\ ( b e. ZZ /\ a e. ZZ ) ) -> ( a + b ) = ( ( 2 x. y ) + ( 2 x. x ) ) )
29 2cnd 
 |-  ( ( ( x e. ZZ /\ b = ( 2 x. x ) ) /\ ( y e. ZZ /\ a = ( 2 x. y ) ) ) -> 2 e. CC )
30 zcn 
 |-  ( y e. ZZ -> y e. CC )
31 30 adantr 
 |-  ( ( y e. ZZ /\ a = ( 2 x. y ) ) -> y e. CC )
32 31 adantl 
 |-  ( ( ( x e. ZZ /\ b = ( 2 x. x ) ) /\ ( y e. ZZ /\ a = ( 2 x. y ) ) ) -> y e. CC )
33 zcn 
 |-  ( x e. ZZ -> x e. CC )
34 33 adantr 
 |-  ( ( x e. ZZ /\ b = ( 2 x. x ) ) -> x e. CC )
35 34 adantr 
 |-  ( ( ( x e. ZZ /\ b = ( 2 x. x ) ) /\ ( y e. ZZ /\ a = ( 2 x. y ) ) ) -> x e. CC )
36 29 32 35 adddid 
 |-  ( ( ( x e. ZZ /\ b = ( 2 x. x ) ) /\ ( y e. ZZ /\ a = ( 2 x. y ) ) ) -> ( 2 x. ( y + x ) ) = ( ( 2 x. y ) + ( 2 x. x ) ) )
37 36 adantr 
 |-  ( ( ( ( x e. ZZ /\ b = ( 2 x. x ) ) /\ ( y e. ZZ /\ a = ( 2 x. y ) ) ) /\ ( b e. ZZ /\ a e. ZZ ) ) -> ( 2 x. ( y + x ) ) = ( ( 2 x. y ) + ( 2 x. x ) ) )
38 28 37 eqtr4d 
 |-  ( ( ( ( x e. ZZ /\ b = ( 2 x. x ) ) /\ ( y e. ZZ /\ a = ( 2 x. y ) ) ) /\ ( b e. ZZ /\ a e. ZZ ) ) -> ( a + b ) = ( 2 x. ( y + x ) ) )
39 38 eqeq1d 
 |-  ( ( ( ( x e. ZZ /\ b = ( 2 x. x ) ) /\ ( y e. ZZ /\ a = ( 2 x. y ) ) ) /\ ( b e. ZZ /\ a e. ZZ ) ) -> ( ( a + b ) = ( 2 x. z ) <-> ( 2 x. ( y + x ) ) = ( 2 x. z ) ) )
40 39 rexbidv 
 |-  ( ( ( ( x e. ZZ /\ b = ( 2 x. x ) ) /\ ( y e. ZZ /\ a = ( 2 x. y ) ) ) /\ ( b e. ZZ /\ a e. ZZ ) ) -> ( E. z e. ZZ ( a + b ) = ( 2 x. z ) <-> E. z e. ZZ ( 2 x. ( y + x ) ) = ( 2 x. z ) ) )
41 24 40 mpbird 
 |-  ( ( ( ( x e. ZZ /\ b = ( 2 x. x ) ) /\ ( y e. ZZ /\ a = ( 2 x. y ) ) ) /\ ( b e. ZZ /\ a e. ZZ ) ) -> E. z e. ZZ ( a + b ) = ( 2 x. z ) )
42 41 ex 
 |-  ( ( ( x e. ZZ /\ b = ( 2 x. x ) ) /\ ( y e. ZZ /\ a = ( 2 x. y ) ) ) -> ( ( b e. ZZ /\ a e. ZZ ) -> E. z e. ZZ ( a + b ) = ( 2 x. z ) ) )
43 42 rexlimdvaa 
 |-  ( ( x e. ZZ /\ b = ( 2 x. x ) ) -> ( E. y e. ZZ a = ( 2 x. y ) -> ( ( b e. ZZ /\ a e. ZZ ) -> E. z e. ZZ ( a + b ) = ( 2 x. z ) ) ) )
44 43 rexlimiva 
 |-  ( E. x e. ZZ b = ( 2 x. x ) -> ( E. y e. ZZ a = ( 2 x. y ) -> ( ( b e. ZZ /\ a e. ZZ ) -> E. z e. ZZ ( a + b ) = ( 2 x. z ) ) ) )
45 44 imp 
 |-  ( ( E. x e. ZZ b = ( 2 x. x ) /\ E. y e. ZZ a = ( 2 x. y ) ) -> ( ( b e. ZZ /\ a e. ZZ ) -> E. z e. ZZ ( a + b ) = ( 2 x. z ) ) )
46 oveq2 
 |-  ( x = z -> ( 2 x. x ) = ( 2 x. z ) )
47 46 eqeq2d 
 |-  ( x = z -> ( ( a + b ) = ( 2 x. x ) <-> ( a + b ) = ( 2 x. z ) ) )
48 47 cbvrexvw 
 |-  ( E. x e. ZZ ( a + b ) = ( 2 x. x ) <-> E. z e. ZZ ( a + b ) = ( 2 x. z ) )
49 45 48 imbitrrdi 
 |-  ( ( E. x e. ZZ b = ( 2 x. x ) /\ E. y e. ZZ a = ( 2 x. y ) ) -> ( ( b e. ZZ /\ a e. ZZ ) -> E. x e. ZZ ( a + b ) = ( 2 x. x ) ) )
50 49 impcom 
 |-  ( ( ( b e. ZZ /\ a e. ZZ ) /\ ( E. x e. ZZ b = ( 2 x. x ) /\ E. y e. ZZ a = ( 2 x. y ) ) ) -> E. x e. ZZ ( a + b ) = ( 2 x. x ) )
51 eqeq1 
 |-  ( z = ( a + b ) -> ( z = ( 2 x. x ) <-> ( a + b ) = ( 2 x. x ) ) )
52 51 rexbidv 
 |-  ( z = ( a + b ) -> ( E. x e. ZZ z = ( 2 x. x ) <-> E. x e. ZZ ( a + b ) = ( 2 x. x ) ) )
53 52 1 elrab2 
 |-  ( ( a + b ) e. E <-> ( ( a + b ) e. ZZ /\ E. x e. ZZ ( a + b ) = ( 2 x. x ) ) )
54 14 50 53 sylanbrc 
 |-  ( ( ( b e. ZZ /\ a e. ZZ ) /\ ( E. x e. ZZ b = ( 2 x. x ) /\ E. y e. ZZ a = ( 2 x. y ) ) ) -> ( a + b ) e. E )
55 54 exp32 
 |-  ( ( b e. ZZ /\ a e. ZZ ) -> ( E. x e. ZZ b = ( 2 x. x ) -> ( E. y e. ZZ a = ( 2 x. y ) -> ( a + b ) e. E ) ) )
56 55 impancom 
 |-  ( ( b e. ZZ /\ E. x e. ZZ b = ( 2 x. x ) ) -> ( a e. ZZ -> ( E. y e. ZZ a = ( 2 x. y ) -> ( a + b ) e. E ) ) )
57 56 com13 
 |-  ( E. y e. ZZ a = ( 2 x. y ) -> ( a e. ZZ -> ( ( b e. ZZ /\ E. x e. ZZ b = ( 2 x. x ) ) -> ( a + b ) e. E ) ) )
58 11 57 sylbi 
 |-  ( E. x e. ZZ a = ( 2 x. x ) -> ( a e. ZZ -> ( ( b e. ZZ /\ E. x e. ZZ b = ( 2 x. x ) ) -> ( a + b ) e. E ) ) )
59 58 impcom 
 |-  ( ( a e. ZZ /\ E. x e. ZZ a = ( 2 x. x ) ) -> ( ( b e. ZZ /\ E. x e. ZZ b = ( 2 x. x ) ) -> ( a + b ) e. E ) )
60 59 imp 
 |-  ( ( ( a e. ZZ /\ E. x e. ZZ a = ( 2 x. x ) ) /\ ( b e. ZZ /\ E. x e. ZZ b = ( 2 x. x ) ) ) -> ( a + b ) e. E )
61 5 8 60 syl2anb 
 |-  ( ( a e. E /\ b e. E ) -> ( a + b ) e. E )
62 61 rgen2 
 |-  A. a e. E A. b e. E ( a + b ) e. E
63 0z 
 |-  0 e. ZZ
64 2cn 
 |-  2 e. CC
65 0zd 
 |-  ( 2 e. CC -> 0 e. ZZ )
66 oveq2 
 |-  ( x = 0 -> ( 2 x. x ) = ( 2 x. 0 ) )
67 66 eqeq2d 
 |-  ( x = 0 -> ( 0 = ( 2 x. x ) <-> 0 = ( 2 x. 0 ) ) )
68 67 adantl 
 |-  ( ( 2 e. CC /\ x = 0 ) -> ( 0 = ( 2 x. x ) <-> 0 = ( 2 x. 0 ) ) )
69 mul01 
 |-  ( 2 e. CC -> ( 2 x. 0 ) = 0 )
70 69 eqcomd 
 |-  ( 2 e. CC -> 0 = ( 2 x. 0 ) )
71 65 68 70 rspcedvd 
 |-  ( 2 e. CC -> E. x e. ZZ 0 = ( 2 x. x ) )
72 64 71 ax-mp 
 |-  E. x e. ZZ 0 = ( 2 x. x )
73 eqeq1 
 |-  ( z = 0 -> ( z = ( 2 x. x ) <-> 0 = ( 2 x. x ) ) )
74 73 rexbidv 
 |-  ( z = 0 -> ( E. x e. ZZ z = ( 2 x. x ) <-> E. x e. ZZ 0 = ( 2 x. x ) ) )
75 74 elrab 
 |-  ( 0 e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } <-> ( 0 e. ZZ /\ E. x e. ZZ 0 = ( 2 x. x ) ) )
76 63 72 75 mpbir2an 
 |-  0 e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) }
77 76 1 eleqtrri 
 |-  0 e. E
78 1 2 2zrngbas 
 |-  E = ( Base ` R )
79 1 2 2zrngadd 
 |-  + = ( +g ` R )
80 78 79 ismgmn0 
 |-  ( 0 e. E -> ( R e. Mgm <-> A. a e. E A. b e. E ( a + b ) e. E ) )
81 77 80 ax-mp 
 |-  ( R e. Mgm <-> A. a e. E A. b e. E ( a + b ) e. E )
82 62 81 mpbir 
 |-  R e. Mgm