Metamath Proof Explorer

Theorem pzriprnglem8

Description: Lemma 8 for pzriprng : I resp. J is a two-sided ideal of the non-unital ring R . (Contributed by AV, 21-Mar-2025)

Ref Expression
Hypotheses pzriprng.r 
|- R = ( ZZring Xs. ZZring )
pzriprng.i 
|- I = ( ZZ X. { 0 } )
pzriprng.j 
|- J = ( R |`s I )
Assertion pzriprnglem8 
|- I e. ( 2Ideal ` R )

Proof

Step Hyp Ref Expression
1 pzriprng.r 
 |-  R = ( ZZring Xs. ZZring )
2 pzriprng.i 
 |-  I = ( ZZ X. { 0 } )
3 pzriprng.j 
 |-  J = ( R |`s I )
4 1 pzriprnglem2 
 |-  ( Base ` R ) = ( ZZ X. ZZ )
5 4 eleq2i 
 |-  ( x e. ( Base ` R ) <-> x e. ( ZZ X. ZZ ) )
6 elxp2 
 |-  ( x e. ( ZZ X. ZZ ) <-> E. a e. ZZ E. b e. ZZ x = <. a , b >. )
7 5 6 bitri 
 |-  ( x e. ( Base ` R ) <-> E. a e. ZZ E. b e. ZZ x = <. a , b >. )
8 1 2 pzriprnglem3 
 |-  ( y e. I <-> E. c e. ZZ y = <. c , 0 >. )
9 simpll 
 |-  ( ( ( a e. ZZ /\ b e. ZZ ) /\ c e. ZZ ) -> a e. ZZ )
10 simpr 
 |-  ( ( ( a e. ZZ /\ b e. ZZ ) /\ c e. ZZ ) -> c e. ZZ )
11 9 10 zmulcld 
 |-  ( ( ( a e. ZZ /\ b e. ZZ ) /\ c e. ZZ ) -> ( a x. c ) e. ZZ )
12 zcn 
 |-  ( b e. ZZ -> b e. CC )
13 12 adantl 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> b e. CC )
14 13 adantr 
 |-  ( ( ( a e. ZZ /\ b e. ZZ ) /\ c e. ZZ ) -> b e. CC )
15 14 mul01d 
 |-  ( ( ( a e. ZZ /\ b e. ZZ ) /\ c e. ZZ ) -> ( b x. 0 ) = 0 )
16 ovex 
 |-  ( b x. 0 ) e. _V
17 16 elsn 
 |-  ( ( b x. 0 ) e. { 0 } <-> ( b x. 0 ) = 0 )
18 15 17 sylibr 
 |-  ( ( ( a e. ZZ /\ b e. ZZ ) /\ c e. ZZ ) -> ( b x. 0 ) e. { 0 } )
19 11 18 opelxpd 
 |-  ( ( ( a e. ZZ /\ b e. ZZ ) /\ c e. ZZ ) -> <. ( a x. c ) , ( b x. 0 ) >. e. ( ZZ X. { 0 } ) )
20 10 9 zmulcld 
 |-  ( ( ( a e. ZZ /\ b e. ZZ ) /\ c e. ZZ ) -> ( c x. a ) e. ZZ )
21 14 mul02d 
 |-  ( ( ( a e. ZZ /\ b e. ZZ ) /\ c e. ZZ ) -> ( 0 x. b ) = 0 )
22 ovex 
 |-  ( 0 x. b ) e. _V
23 22 elsn 
 |-  ( ( 0 x. b ) e. { 0 } <-> ( 0 x. b ) = 0 )
24 21 23 sylibr 
 |-  ( ( ( a e. ZZ /\ b e. ZZ ) /\ c e. ZZ ) -> ( 0 x. b ) e. { 0 } )
25 20 24 opelxpd 
 |-  ( ( ( a e. ZZ /\ b e. ZZ ) /\ c e. ZZ ) -> <. ( c x. a ) , ( 0 x. b ) >. e. ( ZZ X. { 0 } ) )
26 zringbas 
 |-  ZZ = ( Base ` ZZring )
27 zringring 
 |-  ZZring e. Ring
28 27 a1i 
 |-  ( ( ( a e. ZZ /\ b e. ZZ ) /\ c e. ZZ ) -> ZZring e. Ring )
29 simplr 
 |-  ( ( ( a e. ZZ /\ b e. ZZ ) /\ c e. ZZ ) -> b e. ZZ )
30 0zd 
 |-  ( ( ( a e. ZZ /\ b e. ZZ ) /\ c e. ZZ ) -> 0 e. ZZ )
31 29 30 zmulcld 
 |-  ( ( ( a e. ZZ /\ b e. ZZ ) /\ c e. ZZ ) -> ( b x. 0 ) e. ZZ )
32 zringmulr 
 |-  x. = ( .r ` ZZring )
33 eqid 
 |-  ( .r ` R ) = ( .r ` R )
34 1 26 26 28 28 9 29 10 30 11 31 32 32 33 xpsmul 
 |-  ( ( ( a e. ZZ /\ b e. ZZ ) /\ c e. ZZ ) -> ( <. a , b >. ( .r ` R ) <. c , 0 >. ) = <. ( a x. c ) , ( b x. 0 ) >. )
35 34 eleq1d 
 |-  ( ( ( a e. ZZ /\ b e. ZZ ) /\ c e. ZZ ) -> ( ( <. a , b >. ( .r ` R ) <. c , 0 >. ) e. ( ZZ X. { 0 } ) <-> <. ( a x. c ) , ( b x. 0 ) >. e. ( ZZ X. { 0 } ) ) )
36 simpl 
 |-  ( ( c e. ZZ /\ ( a e. ZZ /\ b e. ZZ ) ) -> c e. ZZ )
37 simprl 
 |-  ( ( c e. ZZ /\ ( a e. ZZ /\ b e. ZZ ) ) -> a e. ZZ )
38 36 37 zmulcld 
 |-  ( ( c e. ZZ /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( c x. a ) e. ZZ )
39 38 ancoms 
 |-  ( ( ( a e. ZZ /\ b e. ZZ ) /\ c e. ZZ ) -> ( c x. a ) e. ZZ )
40 0zd 
 |-  ( ( c e. ZZ /\ ( a e. ZZ /\ b e. ZZ ) ) -> 0 e. ZZ )
41 simprr 
 |-  ( ( c e. ZZ /\ ( a e. ZZ /\ b e. ZZ ) ) -> b e. ZZ )
42 40 41 zmulcld 
 |-  ( ( c e. ZZ /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( 0 x. b ) e. ZZ )
43 42 ancoms 
 |-  ( ( ( a e. ZZ /\ b e. ZZ ) /\ c e. ZZ ) -> ( 0 x. b ) e. ZZ )
44 1 26 26 28 28 10 30 9 29 39 43 32 32 33 xpsmul 
 |-  ( ( ( a e. ZZ /\ b e. ZZ ) /\ c e. ZZ ) -> ( <. c , 0 >. ( .r ` R ) <. a , b >. ) = <. ( c x. a ) , ( 0 x. b ) >. )
45 44 eleq1d 
 |-  ( ( ( a e. ZZ /\ b e. ZZ ) /\ c e. ZZ ) -> ( ( <. c , 0 >. ( .r ` R ) <. a , b >. ) e. ( ZZ X. { 0 } ) <-> <. ( c x. a ) , ( 0 x. b ) >. e. ( ZZ X. { 0 } ) ) )
46 35 45 anbi12d 
 |-  ( ( ( a e. ZZ /\ b e. ZZ ) /\ c e. ZZ ) -> ( ( ( <. a , b >. ( .r ` R ) <. c , 0 >. ) e. ( ZZ X. { 0 } ) /\ ( <. c , 0 >. ( .r ` R ) <. a , b >. ) e. ( ZZ X. { 0 } ) ) <-> ( <. ( a x. c ) , ( b x. 0 ) >. e. ( ZZ X. { 0 } ) /\ <. ( c x. a ) , ( 0 x. b ) >. e. ( ZZ X. { 0 } ) ) ) )
47 19 25 46 mpbir2and 
 |-  ( ( ( a e. ZZ /\ b e. ZZ ) /\ c e. ZZ ) -> ( ( <. a , b >. ( .r ` R ) <. c , 0 >. ) e. ( ZZ X. { 0 } ) /\ ( <. c , 0 >. ( .r ` R ) <. a , b >. ) e. ( ZZ X. { 0 } ) ) )
48 47 adantr 
 |-  ( ( ( ( a e. ZZ /\ b e. ZZ ) /\ c e. ZZ ) /\ ( y = <. c , 0 >. /\ x = <. a , b >. ) ) -> ( ( <. a , b >. ( .r ` R ) <. c , 0 >. ) e. ( ZZ X. { 0 } ) /\ ( <. c , 0 >. ( .r ` R ) <. a , b >. ) e. ( ZZ X. { 0 } ) ) )
49 oveq12 
 |-  ( ( x = <. a , b >. /\ y = <. c , 0 >. ) -> ( x ( .r ` R ) y ) = ( <. a , b >. ( .r ` R ) <. c , 0 >. ) )
50 49 ancoms 
 |-  ( ( y = <. c , 0 >. /\ x = <. a , b >. ) -> ( x ( .r ` R ) y ) = ( <. a , b >. ( .r ` R ) <. c , 0 >. ) )
51 50 adantl 
 |-  ( ( ( ( a e. ZZ /\ b e. ZZ ) /\ c e. ZZ ) /\ ( y = <. c , 0 >. /\ x = <. a , b >. ) ) -> ( x ( .r ` R ) y ) = ( <. a , b >. ( .r ` R ) <. c , 0 >. ) )
52 2 a1i 
 |-  ( ( ( ( a e. ZZ /\ b e. ZZ ) /\ c e. ZZ ) /\ ( y = <. c , 0 >. /\ x = <. a , b >. ) ) -> I = ( ZZ X. { 0 } ) )
53 51 52 eleq12d 
 |-  ( ( ( ( a e. ZZ /\ b e. ZZ ) /\ c e. ZZ ) /\ ( y = <. c , 0 >. /\ x = <. a , b >. ) ) -> ( ( x ( .r ` R ) y ) e. I <-> ( <. a , b >. ( .r ` R ) <. c , 0 >. ) e. ( ZZ X. { 0 } ) ) )
54 oveq12 
 |-  ( ( y = <. c , 0 >. /\ x = <. a , b >. ) -> ( y ( .r ` R ) x ) = ( <. c , 0 >. ( .r ` R ) <. a , b >. ) )
55 54 adantl 
 |-  ( ( ( ( a e. ZZ /\ b e. ZZ ) /\ c e. ZZ ) /\ ( y = <. c , 0 >. /\ x = <. a , b >. ) ) -> ( y ( .r ` R ) x ) = ( <. c , 0 >. ( .r ` R ) <. a , b >. ) )
56 55 52 eleq12d 
 |-  ( ( ( ( a e. ZZ /\ b e. ZZ ) /\ c e. ZZ ) /\ ( y = <. c , 0 >. /\ x = <. a , b >. ) ) -> ( ( y ( .r ` R ) x ) e. I <-> ( <. c , 0 >. ( .r ` R ) <. a , b >. ) e. ( ZZ X. { 0 } ) ) )
57 53 56 anbi12d 
 |-  ( ( ( ( a e. ZZ /\ b e. ZZ ) /\ c e. ZZ ) /\ ( y = <. c , 0 >. /\ x = <. a , b >. ) ) -> ( ( ( x ( .r ` R ) y ) e. I /\ ( y ( .r ` R ) x ) e. I ) <-> ( ( <. a , b >. ( .r ` R ) <. c , 0 >. ) e. ( ZZ X. { 0 } ) /\ ( <. c , 0 >. ( .r ` R ) <. a , b >. ) e. ( ZZ X. { 0 } ) ) ) )
58 48 57 mpbird 
 |-  ( ( ( ( a e. ZZ /\ b e. ZZ ) /\ c e. ZZ ) /\ ( y = <. c , 0 >. /\ x = <. a , b >. ) ) -> ( ( x ( .r ` R ) y ) e. I /\ ( y ( .r ` R ) x ) e. I ) )
59 58 exp32 
 |-  ( ( ( a e. ZZ /\ b e. ZZ ) /\ c e. ZZ ) -> ( y = <. c , 0 >. -> ( x = <. a , b >. -> ( ( x ( .r ` R ) y ) e. I /\ ( y ( .r ` R ) x ) e. I ) ) ) )
60 59 rexlimdva 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> ( E. c e. ZZ y = <. c , 0 >. -> ( x = <. a , b >. -> ( ( x ( .r ` R ) y ) e. I /\ ( y ( .r ` R ) x ) e. I ) ) ) )
61 60 com23 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> ( x = <. a , b >. -> ( E. c e. ZZ y = <. c , 0 >. -> ( ( x ( .r ` R ) y ) e. I /\ ( y ( .r ` R ) x ) e. I ) ) ) )
62 61 rexlimivv 
 |-  ( E. a e. ZZ E. b e. ZZ x = <. a , b >. -> ( E. c e. ZZ y = <. c , 0 >. -> ( ( x ( .r ` R ) y ) e. I /\ ( y ( .r ` R ) x ) e. I ) ) )
63 62 imp 
 |-  ( ( E. a e. ZZ E. b e. ZZ x = <. a , b >. /\ E. c e. ZZ y = <. c , 0 >. ) -> ( ( x ( .r ` R ) y ) e. I /\ ( y ( .r ` R ) x ) e. I ) )
64 7 8 63 syl2anb 
 |-  ( ( x e. ( Base ` R ) /\ y e. I ) -> ( ( x ( .r ` R ) y ) e. I /\ ( y ( .r ` R ) x ) e. I ) )
65 64 rgen2 
 |-  A. x e. ( Base ` R ) A. y e. I ( ( x ( .r ` R ) y ) e. I /\ ( y ( .r ` R ) x ) e. I )
66 1 pzriprnglem1 
 |-  R e. Rng
67 1 2 pzriprnglem4 
 |-  I e. ( SubGrp ` R )
68 eqid 
 |-  ( 2Ideal ` R ) = ( 2Ideal ` R )
69 eqid 
 |-  ( Base ` R ) = ( Base ` R )
70 68 69 33 df2idl2rng 
 |-  ( ( R e. Rng /\ I e. ( SubGrp ` R ) ) -> ( I e. ( 2Ideal ` R ) <-> A. x e. ( Base ` R ) A. y e. I ( ( x ( .r ` R ) y ) e. I /\ ( y ( .r ` R ) x ) e. I ) ) )
71 66 67 70 mp2an 
 |-  ( I e. ( 2Ideal ` R ) <-> A. x e. ( Base ` R ) A. y e. I ( ( x ( .r ` R ) y ) e. I /\ ( y ( .r ` R ) x ) e. I ) )
72 65 71 mpbir 
 |-  I e. ( 2Ideal ` R )