Metamath Proof Explorer

Theorem 2zrngnmrid

Description: R has no multiplicative (right) identity. (Contributed by AV, 12-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 2zrngnmrid 
|- A. a e. ( E \ { 0 } ) A. b e. E ( a x. b ) =/= a

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 eldifsn 
 |-  ( a e. ( E \ { 0 } ) <-> ( a e. E /\ a =/= 0 ) )
5 eqeq1 
 |-  ( z = a -> ( z = ( 2 x. x ) <-> a = ( 2 x. x ) ) )
6 5 rexbidv 
 |-  ( z = a -> ( E. x e. ZZ z = ( 2 x. x ) <-> E. x e. ZZ a = ( 2 x. x ) ) )
7 6 1 elrab2 
 |-  ( a e. E <-> ( a e. ZZ /\ E. x e. ZZ a = ( 2 x. x ) ) )
8 zcn 
 |-  ( a e. ZZ -> a e. CC )
9 8 adantr 
 |-  ( ( a e. ZZ /\ E. x e. ZZ a = ( 2 x. x ) ) -> a e. CC )
10 7 9 sylbi 
 |-  ( a e. E -> a e. CC )
11 10 anim1i 
 |-  ( ( a e. E /\ a =/= 0 ) -> ( a e. CC /\ a =/= 0 ) )
12 4 11 sylbi 
 |-  ( a e. ( E \ { 0 } ) -> ( a e. CC /\ a =/= 0 ) )
13 eqeq1 
 |-  ( z = b -> ( z = ( 2 x. x ) <-> b = ( 2 x. x ) ) )
14 13 rexbidv 
 |-  ( z = b -> ( E. x e. ZZ z = ( 2 x. x ) <-> E. x e. ZZ b = ( 2 x. x ) ) )
15 14 1 elrab2 
 |-  ( b e. E <-> ( b e. ZZ /\ E. x e. ZZ b = ( 2 x. x ) ) )
16 zcn 
 |-  ( b e. ZZ -> b e. CC )
17 16 adantr 
 |-  ( ( b e. ZZ /\ E. x e. ZZ b = ( 2 x. x ) ) -> b e. CC )
18 15 17 sylbi 
 |-  ( b e. E -> b e. CC )
19 18 ancli 
 |-  ( b e. E -> ( b e. E /\ b e. CC ) )
20 1 1neven 
 |-  1 e/ E
21 elnelne2 
 |-  ( ( b e. E /\ 1 e/ E ) -> b =/= 1 )
22 20 21 mpan2 
 |-  ( b e. E -> b =/= 1 )
23 22 ad2antrl 
 |-  ( ( ( a e. CC /\ a =/= 0 ) /\ ( b e. E /\ b e. CC ) ) -> b =/= 1 )
24 simpr 
 |-  ( ( b e. E /\ b e. CC ) -> b e. CC )
25 24 anim2i 
 |-  ( ( ( a e. CC /\ a =/= 0 ) /\ ( b e. E /\ b e. CC ) ) -> ( ( a e. CC /\ a =/= 0 ) /\ b e. CC ) )
26 3anass 
 |-  ( ( b e. CC /\ a e. CC /\ a =/= 0 ) <-> ( b e. CC /\ ( a e. CC /\ a =/= 0 ) ) )
27 ancom 
 |-  ( ( b e. CC /\ ( a e. CC /\ a =/= 0 ) ) <-> ( ( a e. CC /\ a =/= 0 ) /\ b e. CC ) )
28 26 27 bitri 
 |-  ( ( b e. CC /\ a e. CC /\ a =/= 0 ) <-> ( ( a e. CC /\ a =/= 0 ) /\ b e. CC ) )
29 25 28 sylibr 
 |-  ( ( ( a e. CC /\ a =/= 0 ) /\ ( b e. E /\ b e. CC ) ) -> ( b e. CC /\ a e. CC /\ a =/= 0 ) )
30 divcan3 
 |-  ( ( b e. CC /\ a e. CC /\ a =/= 0 ) -> ( ( a x. b ) / a ) = b )
31 29 30 syl 
 |-  ( ( ( a e. CC /\ a =/= 0 ) /\ ( b e. E /\ b e. CC ) ) -> ( ( a x. b ) / a ) = b )
32 divid 
 |-  ( ( a e. CC /\ a =/= 0 ) -> ( a / a ) = 1 )
33 32 adantr 
 |-  ( ( ( a e. CC /\ a =/= 0 ) /\ ( b e. E /\ b e. CC ) ) -> ( a / a ) = 1 )
34 23 31 33 3netr4d 
 |-  ( ( ( a e. CC /\ a =/= 0 ) /\ ( b e. E /\ b e. CC ) ) -> ( ( a x. b ) / a ) =/= ( a / a ) )
35 simpl 
 |-  ( ( a e. CC /\ a =/= 0 ) -> a e. CC )
36 mulcl 
 |-  ( ( a e. CC /\ b e. CC ) -> ( a x. b ) e. CC )
37 35 24 36 syl2an 
 |-  ( ( ( a e. CC /\ a =/= 0 ) /\ ( b e. E /\ b e. CC ) ) -> ( a x. b ) e. CC )
38 35 adantr 
 |-  ( ( ( a e. CC /\ a =/= 0 ) /\ ( b e. E /\ b e. CC ) ) -> a e. CC )
39 simpl 
 |-  ( ( ( a e. CC /\ a =/= 0 ) /\ ( b e. E /\ b e. CC ) ) -> ( a e. CC /\ a =/= 0 ) )
40 div11 
 |-  ( ( ( a x. b ) e. CC /\ a e. CC /\ ( a e. CC /\ a =/= 0 ) ) -> ( ( ( a x. b ) / a ) = ( a / a ) <-> ( a x. b ) = a ) )
41 37 38 39 40 syl3anc 
 |-  ( ( ( a e. CC /\ a =/= 0 ) /\ ( b e. E /\ b e. CC ) ) -> ( ( ( a x. b ) / a ) = ( a / a ) <-> ( a x. b ) = a ) )
42 41 biimprd 
 |-  ( ( ( a e. CC /\ a =/= 0 ) /\ ( b e. E /\ b e. CC ) ) -> ( ( a x. b ) = a -> ( ( a x. b ) / a ) = ( a / a ) ) )
43 42 necon3d 
 |-  ( ( ( a e. CC /\ a =/= 0 ) /\ ( b e. E /\ b e. CC ) ) -> ( ( ( a x. b ) / a ) =/= ( a / a ) -> ( a x. b ) =/= a ) )
44 34 43 mpd 
 |-  ( ( ( a e. CC /\ a =/= 0 ) /\ ( b e. E /\ b e. CC ) ) -> ( a x. b ) =/= a )
45 12 19 44 syl2an 
 |-  ( ( a e. ( E \ { 0 } ) /\ b e. E ) -> ( a x. b ) =/= a )
46 45 rgen2 
 |-  A. a e. ( E \ { 0 } ) A. b e. E ( a x. b ) =/= a