Metamath Proof Explorer

Theorem 2zrngnmlid

Description: R has no multiplicative (left) 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 2zrngnmlid 
|- A. b e. E E. a e. E ( b x. a ) =/= 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 1 2even 
 |-  2 e. E
5 4 a1i 
 |-  ( b e. E -> 2 e. E )
6 oveq2 
 |-  ( a = 2 -> ( b x. a ) = ( b x. 2 ) )
7 id 
 |-  ( a = 2 -> a = 2 )
8 6 7 neeq12d 
 |-  ( a = 2 -> ( ( b x. a ) =/= a <-> ( b x. 2 ) =/= 2 ) )
9 8 adantl 
 |-  ( ( b e. E /\ a = 2 ) -> ( ( b x. a ) =/= a <-> ( b x. 2 ) =/= 2 ) )
10 elrabi 
 |-  ( b e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } -> b e. ZZ )
11 10 zcnd 
 |-  ( b e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } -> b e. CC )
12 11 1 eleq2s 
 |-  ( b e. E -> b e. CC )
13 1 1neven 
 |-  1 e/ E
14 elnelne2 
 |-  ( ( b e. E /\ 1 e/ E ) -> b =/= 1 )
15 13 14 mpan2 
 |-  ( b e. E -> b =/= 1 )
16 15 adantr 
 |-  ( ( b e. E /\ b e. CC ) -> b =/= 1 )
17 simpr 
 |-  ( ( b e. E /\ b e. CC ) -> b e. CC )
18 2cnd 
 |-  ( ( b e. E /\ b e. CC ) -> 2 e. CC )
19 2ne0 
 |-  2 =/= 0
20 19 a1i 
 |-  ( ( b e. E /\ b e. CC ) -> 2 =/= 0 )
21 17 18 20 divcan4d 
 |-  ( ( b e. E /\ b e. CC ) -> ( ( b x. 2 ) / 2 ) = b )
22 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
23 divid 
 |-  ( ( 2 e. CC /\ 2 =/= 0 ) -> ( 2 / 2 ) = 1 )
24 22 23 mp1i 
 |-  ( ( b e. E /\ b e. CC ) -> ( 2 / 2 ) = 1 )
25 16 21 24 3netr4d 
 |-  ( ( b e. E /\ b e. CC ) -> ( ( b x. 2 ) / 2 ) =/= ( 2 / 2 ) )
26 17 18 mulcld 
 |-  ( ( b e. E /\ b e. CC ) -> ( b x. 2 ) e. CC )
27 22 a1i 
 |-  ( ( b e. E /\ b e. CC ) -> ( 2 e. CC /\ 2 =/= 0 ) )
28 div11 
 |-  ( ( ( b x. 2 ) e. CC /\ 2 e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( ( b x. 2 ) / 2 ) = ( 2 / 2 ) <-> ( b x. 2 ) = 2 ) )
29 26 18 27 28 syl3anc 
 |-  ( ( b e. E /\ b e. CC ) -> ( ( ( b x. 2 ) / 2 ) = ( 2 / 2 ) <-> ( b x. 2 ) = 2 ) )
30 29 biimprd 
 |-  ( ( b e. E /\ b e. CC ) -> ( ( b x. 2 ) = 2 -> ( ( b x. 2 ) / 2 ) = ( 2 / 2 ) ) )
31 30 necon3d 
 |-  ( ( b e. E /\ b e. CC ) -> ( ( ( b x. 2 ) / 2 ) =/= ( 2 / 2 ) -> ( b x. 2 ) =/= 2 ) )
32 25 31 mpd 
 |-  ( ( b e. E /\ b e. CC ) -> ( b x. 2 ) =/= 2 )
33 12 32 mpdan 
 |-  ( b e. E -> ( b x. 2 ) =/= 2 )
34 5 9 33 rspcedvd 
 |-  ( b e. E -> E. a e. E ( b x. a ) =/= a )
35 34 rgen 
 |-  A. b e. E E. a e. E ( b x. a ) =/= a