Metamath Proof Explorer

Theorem 2zrngnring

Description: R is not a unital ring. (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 )
2zrngmmgm.1 
|- M = ( mulGrp ` R )
Assertion 2zrngnring 
|- R e/ Ring

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 2zrngnmlid 
 |-  A. b e. E E. a e. E ( b x. a ) =/= a
5 1 2 2zrngbas 
 |-  E = ( Base ` R )
6 3 5 mgpbas 
 |-  E = ( Base ` M )
7 1 2 2zrngmul 
 |-  x. = ( .r ` R )
8 3 7 mgpplusg 
 |-  x. = ( +g ` M )
9 6 8 isnmnd 
 |-  ( A. b e. E E. a e. E ( b x. a ) =/= a -> M e/ Mnd )
10 df-nel 
 |-  ( M e/ Mnd <-> -. M e. Mnd )
11 9 10 sylib 
 |-  ( A. b e. E E. a e. E ( b x. a ) =/= a -> -. M e. Mnd )
12 4 11 ax-mp 
 |-  -. M e. Mnd
13 12 3mix2i 
 |-  ( -. R e. Grp \/ -. M e. Mnd \/ -. A. x e. ( Base ` R ) A. y e. ( Base ` R ) A. z e. ( Base ` R ) ( ( x x. ( y ( +g ` R ) z ) ) = ( ( x x. y ) ( +g ` R ) ( x x. z ) ) /\ ( ( x ( +g ` R ) y ) x. z ) = ( ( x x. z ) ( +g ` R ) ( y x. z ) ) ) )
14 3ianor 
 |-  ( -. ( R e. Grp /\ M e. Mnd /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) A. z e. ( Base ` R ) ( ( x x. ( y ( +g ` R ) z ) ) = ( ( x x. y ) ( +g ` R ) ( x x. z ) ) /\ ( ( x ( +g ` R ) y ) x. z ) = ( ( x x. z ) ( +g ` R ) ( y x. z ) ) ) ) <-> ( -. R e. Grp \/ -. M e. Mnd \/ -. A. x e. ( Base ` R ) A. y e. ( Base ` R ) A. z e. ( Base ` R ) ( ( x x. ( y ( +g ` R ) z ) ) = ( ( x x. y ) ( +g ` R ) ( x x. z ) ) /\ ( ( x ( +g ` R ) y ) x. z ) = ( ( x x. z ) ( +g ` R ) ( y x. z ) ) ) ) )
15 13 14 mpbir 
 |-  -. ( R e. Grp /\ M e. Mnd /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) A. z e. ( Base ` R ) ( ( x x. ( y ( +g ` R ) z ) ) = ( ( x x. y ) ( +g ` R ) ( x x. z ) ) /\ ( ( x ( +g ` R ) y ) x. z ) = ( ( x x. z ) ( +g ` R ) ( y x. z ) ) ) )
16 eqid 
 |-  ( Base ` R ) = ( Base ` R )
17 eqid 
 |-  ( +g ` R ) = ( +g ` R )
18 16 3 17 7 isring 
 |-  ( R e. Ring <-> ( R e. Grp /\ M e. Mnd /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) A. z e. ( Base ` R ) ( ( x x. ( y ( +g ` R ) z ) ) = ( ( x x. y ) ( +g ` R ) ( x x. z ) ) /\ ( ( x ( +g ` R ) y ) x. z ) = ( ( x x. z ) ( +g ` R ) ( y x. z ) ) ) ) )
19 15 18 mtbir 
 |-  -. R e. Ring
20 19 nelir 
 |-  R e/ Ring