Metamath Proof Explorer

Theorem 2zrngagrp

Description: R is an (additive) group. (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 2zrngagrp 
|- R e. Grp

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 1 2 2zrngamnd 
 |-  R e. Mnd
4 eqeq1 
 |-  ( z = y -> ( z = ( 2 x. x ) <-> y = ( 2 x. x ) ) )
5 4 rexbidv 
 |-  ( z = y -> ( E. x e. ZZ z = ( 2 x. x ) <-> E. x e. ZZ y = ( 2 x. x ) ) )
6 5 1 elrab2 
 |-  ( y e. E <-> ( y e. ZZ /\ E. x e. ZZ y = ( 2 x. x ) ) )
7 znegcl 
 |-  ( y e. ZZ -> -u y e. ZZ )
8 7 adantr 
 |-  ( ( y e. ZZ /\ E. x e. ZZ y = ( 2 x. x ) ) -> -u y e. ZZ )
9 nfv 
 |-  F/ x y e. ZZ
10 nfre1 
 |-  F/ x E. x e. ZZ -u y = ( 2 x. x )
11 znegcl 
 |-  ( x e. ZZ -> -u x e. ZZ )
12 11 adantl 
 |-  ( ( y e. ZZ /\ x e. ZZ ) -> -u x e. ZZ )
13 12 adantr 
 |-  ( ( ( y e. ZZ /\ x e. ZZ ) /\ y = ( 2 x. x ) ) -> -u x e. ZZ )
14 oveq2 
 |-  ( z = -u x -> ( 2 x. z ) = ( 2 x. -u x ) )
15 14 eqeq2d 
 |-  ( z = -u x -> ( -u y = ( 2 x. z ) <-> -u y = ( 2 x. -u x ) ) )
16 15 adantl 
 |-  ( ( ( ( y e. ZZ /\ x e. ZZ ) /\ y = ( 2 x. x ) ) /\ z = -u x ) -> ( -u y = ( 2 x. z ) <-> -u y = ( 2 x. -u x ) ) )
17 negeq 
 |-  ( y = ( 2 x. x ) -> -u y = -u ( 2 x. x ) )
18 2cnd 
 |-  ( x e. ZZ -> 2 e. CC )
19 zcn 
 |-  ( x e. ZZ -> x e. CC )
20 18 19 mulneg2d 
 |-  ( x e. ZZ -> ( 2 x. -u x ) = -u ( 2 x. x ) )
21 20 eqcomd 
 |-  ( x e. ZZ -> -u ( 2 x. x ) = ( 2 x. -u x ) )
22 21 adantl 
 |-  ( ( y e. ZZ /\ x e. ZZ ) -> -u ( 2 x. x ) = ( 2 x. -u x ) )
23 17 22 sylan9eqr 
 |-  ( ( ( y e. ZZ /\ x e. ZZ ) /\ y = ( 2 x. x ) ) -> -u y = ( 2 x. -u x ) )
24 13 16 23 rspcedvd 
 |-  ( ( ( y e. ZZ /\ x e. ZZ ) /\ y = ( 2 x. x ) ) -> E. z e. ZZ -u y = ( 2 x. z ) )
25 oveq2 
 |-  ( x = z -> ( 2 x. x ) = ( 2 x. z ) )
26 25 eqeq2d 
 |-  ( x = z -> ( -u y = ( 2 x. x ) <-> -u y = ( 2 x. z ) ) )
27 26 cbvrexvw 
 |-  ( E. x e. ZZ -u y = ( 2 x. x ) <-> E. z e. ZZ -u y = ( 2 x. z ) )
28 24 27 sylibr 
 |-  ( ( ( y e. ZZ /\ x e. ZZ ) /\ y = ( 2 x. x ) ) -> E. x e. ZZ -u y = ( 2 x. x ) )
29 28 exp31 
 |-  ( y e. ZZ -> ( x e. ZZ -> ( y = ( 2 x. x ) -> E. x e. ZZ -u y = ( 2 x. x ) ) ) )
30 9 10 29 rexlimd 
 |-  ( y e. ZZ -> ( E. x e. ZZ y = ( 2 x. x ) -> E. x e. ZZ -u y = ( 2 x. x ) ) )
31 30 imp 
 |-  ( ( y e. ZZ /\ E. x e. ZZ y = ( 2 x. x ) ) -> E. x e. ZZ -u y = ( 2 x. x ) )
32 eqeq1 
 |-  ( z = -u y -> ( z = ( 2 x. x ) <-> -u y = ( 2 x. x ) ) )
33 32 rexbidv 
 |-  ( z = -u y -> ( E. x e. ZZ z = ( 2 x. x ) <-> E. x e. ZZ -u y = ( 2 x. x ) ) )
34 33 1 elrab2 
 |-  ( -u y e. E <-> ( -u y e. ZZ /\ E. x e. ZZ -u y = ( 2 x. x ) ) )
35 8 31 34 sylanbrc 
 |-  ( ( y e. ZZ /\ E. x e. ZZ y = ( 2 x. x ) ) -> -u y e. E )
36 6 35 sylbi 
 |-  ( y e. E -> -u y e. E )
37 oveq1 
 |-  ( z = -u y -> ( z + y ) = ( -u y + y ) )
38 37 eqeq1d 
 |-  ( z = -u y -> ( ( z + y ) = 0 <-> ( -u y + y ) = 0 ) )
39 38 adantl 
 |-  ( ( y e. E /\ z = -u y ) -> ( ( z + y ) = 0 <-> ( -u y + y ) = 0 ) )
40 elrabi 
 |-  ( y e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } -> y e. ZZ )
41 40 1 eleq2s 
 |-  ( y e. E -> y e. ZZ )
42 41 zcnd 
 |-  ( y e. E -> y e. CC )
43 42 negcld 
 |-  ( y e. E -> -u y e. CC )
44 43 42 addcomd 
 |-  ( y e. E -> ( -u y + y ) = ( y + -u y ) )
45 42 negidd 
 |-  ( y e. E -> ( y + -u y ) = 0 )
46 44 45 eqtrd 
 |-  ( y e. E -> ( -u y + y ) = 0 )
47 36 39 46 rspcedvd 
 |-  ( y e. E -> E. z e. E ( z + y ) = 0 )
48 47 rgen 
 |-  A. y e. E E. z e. E ( z + y ) = 0
49 1 2 2zrngbas 
 |-  E = ( Base ` R )
50 1 2 2zrngadd 
 |-  + = ( +g ` R )
51 1 2 2zrng0 
 |-  0 = ( 0g ` R )
52 49 50 51 isgrp 
 |-  ( R e. Grp <-> ( R e. Mnd /\ A. y e. E E. z e. E ( z + y ) = 0 ) )
53 3 48 52 mpbir2an 
 |-  R e. Grp