Metamath Proof Explorer

Theorem 2zrngnmlid2

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 2zrngnmlid2 
|- A. a e. ( E \ { 0 } ) A. b 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 2 3 2zrngnmrid 
 |-  A. a e. ( E \ { 0 } ) A. b e. E ( a x. b ) =/= a
5 eldifi 
 |-  ( a e. ( E \ { 0 } ) -> a e. E )
6 elrabi 
 |-  ( a e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } -> a e. ZZ )
7 6 zcnd 
 |-  ( a e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } -> a e. CC )
8 7 1 eleq2s 
 |-  ( a e. E -> a e. CC )
9 5 8 syl 
 |-  ( a e. ( E \ { 0 } ) -> a e. CC )
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 mulcom 
 |-  ( ( a e. CC /\ b e. CC ) -> ( a x. b ) = ( b x. a ) )
14 9 12 13 syl2an 
 |-  ( ( a e. ( E \ { 0 } ) /\ b e. E ) -> ( a x. b ) = ( b x. a ) )
15 14 eqcomd 
 |-  ( ( a e. ( E \ { 0 } ) /\ b e. E ) -> ( b x. a ) = ( a x. b ) )
16 15 eqeq1d 
 |-  ( ( a e. ( E \ { 0 } ) /\ b e. E ) -> ( ( b x. a ) = a <-> ( a x. b ) = a ) )
17 16 biimpd 
 |-  ( ( a e. ( E \ { 0 } ) /\ b e. E ) -> ( ( b x. a ) = a -> ( a x. b ) = a ) )
18 17 necon3d 
 |-  ( ( a e. ( E \ { 0 } ) /\ b e. E ) -> ( ( a x. b ) =/= a -> ( b x. a ) =/= a ) )
19 18 ralimdva 
 |-  ( a e. ( E \ { 0 } ) -> ( A. b e. E ( a x. b ) =/= a -> A. b e. E ( b x. a ) =/= a ) )
20 19 ralimia 
 |-  ( A. a e. ( E \ { 0 } ) A. b e. E ( a x. b ) =/= a -> A. a e. ( E \ { 0 } ) A. b e. E ( b x. a ) =/= a )
21 4 20 ax-mp 
 |-  A. a e. ( E \ { 0 } ) A. b e. E ( b x. a ) =/= a