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 syl6ibr
 |-  ( ( 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