Metamath Proof Explorer

Theorem 2zrngALT

Description: The ring of integers restricted to the even integers is a (non-unital) ring, the "ring of even integers". Alternate version of 2zrng , based on a restriction of the field of the complex numbers. The proof is based on the facts that the ring of even integers is an additive abelian group (see 2zrngaabl ) and a multiplicative semigroup (see 2zrngmsgrp ). (Contributed by AV, 11-Feb-2020) (New usage is discouraged.) (Proof modification is discouraged.)

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 2zrngALT 
|- R e. Rng

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 2zrngaabl 
 |-  R e. Abel
5 1 2 3 2zrngmsgrp 
 |-  M e. Smgrp
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 elrabi 
 |-  ( b e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } -> b e. ZZ )
10 9 zcnd 
 |-  ( b e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } -> b e. CC )
11 10 1 eleq2s 
 |-  ( b e. E -> b e. CC )
12 elrabi 
 |-  ( y e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } -> y e. ZZ )
13 12 zcnd 
 |-  ( y e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } -> y e. CC )
14 13 1 eleq2s 
 |-  ( y e. E -> y e. CC )
15 adddi 
 |-  ( ( a e. CC /\ b e. CC /\ y e. CC ) -> ( a x. ( b + y ) ) = ( ( a x. b ) + ( a x. y ) ) )
16 adddir 
 |-  ( ( a e. CC /\ b e. CC /\ y e. CC ) -> ( ( a + b ) x. y ) = ( ( a x. y ) + ( b x. y ) ) )
17 15 16 jca 
 |-  ( ( a e. CC /\ b e. CC /\ y e. CC ) -> ( ( a x. ( b + y ) ) = ( ( a x. b ) + ( a x. y ) ) /\ ( ( a + b ) x. y ) = ( ( a x. y ) + ( b x. y ) ) ) )
18 8 11 14 17 syl3an 
 |-  ( ( a e. E /\ b e. E /\ y e. E ) -> ( ( a x. ( b + y ) ) = ( ( a x. b ) + ( a x. y ) ) /\ ( ( a + b ) x. y ) = ( ( a x. y ) + ( b x. y ) ) ) )
19 18 rgen3 
 |-  A. a e. E A. b e. E A. y e. E ( ( a x. ( b + y ) ) = ( ( a x. b ) + ( a x. y ) ) /\ ( ( a + b ) x. y ) = ( ( a x. y ) + ( b x. y ) ) )
20 1 2 2zrngbas 
 |-  E = ( Base ` R )
21 1 2 2zrngadd 
 |-  + = ( +g ` R )
22 1 2 2zrngmul 
 |-  x. = ( .r ` R )
23 20 3 21 22 isrng 
 |-  ( R e. Rng <-> ( R e. Abel /\ M e. Smgrp /\ A. a e. E A. b e. E A. y e. E ( ( a x. ( b + y ) ) = ( ( a x. b ) + ( a x. y ) ) /\ ( ( a + b ) x. y ) = ( ( a x. y ) + ( b x. y ) ) ) ) )
24 4 5 19 23 mpbir3an 
 |-  R e. Rng