Metamath Proof Explorer

Theorem pzriprnglem5

Description: Lemma 5 for pzriprng : I is a subring of the non-unital ring R . (Contributed by AV, 18-Mar-2025)

Ref Expression
Hypotheses pzriprng.r 
|- R = ( ZZring Xs. ZZring )
pzriprng.i 
|- I = ( ZZ X. { 0 } )
Assertion pzriprnglem5 
|- I e. ( SubRng ` R )

Proof

Step Hyp Ref Expression
1 pzriprng.r 
 |-  R = ( ZZring Xs. ZZring )
2 pzriprng.i 
 |-  I = ( ZZ X. { 0 } )
3 1 2 pzriprnglem4 
 |-  I e. ( SubGrp ` R )
4 1 2 pzriprnglem3 
 |-  ( x e. I <-> E. a e. ZZ x = <. a , 0 >. )
5 1 2 pzriprnglem3 
 |-  ( y e. I <-> E. b e. ZZ y = <. b , 0 >. )
6 zringbas 
 |-  ZZ = ( Base ` ZZring )
7 zringring 
 |-  ZZring e. Ring
8 7 a1i 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> ZZring e. Ring )
9 simpl 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> a e. ZZ )
10 0zd 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> 0 e. ZZ )
11 simpr 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> b e. ZZ )
12 zringmulr 
 |-  x. = ( .r ` ZZring )
13 12 eqcomi 
 |-  ( .r ` ZZring ) = x.
14 13 oveqi 
 |-  ( a ( .r ` ZZring ) b ) = ( a x. b )
15 zmulcl 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> ( a x. b ) e. ZZ )
16 14 15 eqeltrid 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> ( a ( .r ` ZZring ) b ) e. ZZ )
17 13 oveqi 
 |-  ( 0 ( .r ` ZZring ) 0 ) = ( 0 x. 0 )
18 0cn 
 |-  0 e. CC
19 18 mul02i 
 |-  ( 0 x. 0 ) = 0
20 17 19 eqtri 
 |-  ( 0 ( .r ` ZZring ) 0 ) = 0
21 0z 
 |-  0 e. ZZ
22 20 21 eqeltri 
 |-  ( 0 ( .r ` ZZring ) 0 ) e. ZZ
23 22 a1i 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> ( 0 ( .r ` ZZring ) 0 ) e. ZZ )
24 eqid 
 |-  ( .r ` ZZring ) = ( .r ` ZZring )
25 eqid 
 |-  ( .r ` R ) = ( .r ` R )
26 1 6 6 8 8 9 10 11 10 16 23 24 24 25 xpsmul 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> ( <. a , 0 >. ( .r ` R ) <. b , 0 >. ) = <. ( a ( .r ` ZZring ) b ) , ( 0 ( .r ` ZZring ) 0 ) >. )
27 c0ex 
 |-  0 e. _V
28 27 snid 
 |-  0 e. { 0 }
29 28 a1i 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> 0 e. { 0 } )
30 20 29 eqeltrid 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> ( 0 ( .r ` ZZring ) 0 ) e. { 0 } )
31 16 30 opelxpd 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> <. ( a ( .r ` ZZring ) b ) , ( 0 ( .r ` ZZring ) 0 ) >. e. ( ZZ X. { 0 } ) )
32 26 31 eqeltrd 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> ( <. a , 0 >. ( .r ` R ) <. b , 0 >. ) e. ( ZZ X. { 0 } ) )
33 32 adantr 
 |-  ( ( ( a e. ZZ /\ b e. ZZ ) /\ ( y = <. b , 0 >. /\ x = <. a , 0 >. ) ) -> ( <. a , 0 >. ( .r ` R ) <. b , 0 >. ) e. ( ZZ X. { 0 } ) )
34 oveq12 
 |-  ( ( x = <. a , 0 >. /\ y = <. b , 0 >. ) -> ( x ( .r ` R ) y ) = ( <. a , 0 >. ( .r ` R ) <. b , 0 >. ) )
35 34 ancoms 
 |-  ( ( y = <. b , 0 >. /\ x = <. a , 0 >. ) -> ( x ( .r ` R ) y ) = ( <. a , 0 >. ( .r ` R ) <. b , 0 >. ) )
36 35 adantl 
 |-  ( ( ( a e. ZZ /\ b e. ZZ ) /\ ( y = <. b , 0 >. /\ x = <. a , 0 >. ) ) -> ( x ( .r ` R ) y ) = ( <. a , 0 >. ( .r ` R ) <. b , 0 >. ) )
37 2 a1i 
 |-  ( ( ( a e. ZZ /\ b e. ZZ ) /\ ( y = <. b , 0 >. /\ x = <. a , 0 >. ) ) -> I = ( ZZ X. { 0 } ) )
38 33 36 37 3eltr4d 
 |-  ( ( ( a e. ZZ /\ b e. ZZ ) /\ ( y = <. b , 0 >. /\ x = <. a , 0 >. ) ) -> ( x ( .r ` R ) y ) e. I )
39 38 exp32 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> ( y = <. b , 0 >. -> ( x = <. a , 0 >. -> ( x ( .r ` R ) y ) e. I ) ) )
40 39 rexlimdva 
 |-  ( a e. ZZ -> ( E. b e. ZZ y = <. b , 0 >. -> ( x = <. a , 0 >. -> ( x ( .r ` R ) y ) e. I ) ) )
41 40 com23 
 |-  ( a e. ZZ -> ( x = <. a , 0 >. -> ( E. b e. ZZ y = <. b , 0 >. -> ( x ( .r ` R ) y ) e. I ) ) )
42 41 rexlimiv 
 |-  ( E. a e. ZZ x = <. a , 0 >. -> ( E. b e. ZZ y = <. b , 0 >. -> ( x ( .r ` R ) y ) e. I ) )
43 42 imp 
 |-  ( ( E. a e. ZZ x = <. a , 0 >. /\ E. b e. ZZ y = <. b , 0 >. ) -> ( x ( .r ` R ) y ) e. I )
44 4 5 43 syl2anb 
 |-  ( ( x e. I /\ y e. I ) -> ( x ( .r ` R ) y ) e. I )
45 44 rgen2 
 |-  A. x e. I A. y e. I ( x ( .r ` R ) y ) e. I
46 1 pzriprnglem1 
 |-  R e. Rng
47 eqid 
 |-  ( Base ` R ) = ( Base ` R )
48 47 25 issubrng2 
 |-  ( R e. Rng -> ( I e. ( SubRng ` R ) <-> ( I e. ( SubGrp ` R ) /\ A. x e. I A. y e. I ( x ( .r ` R ) y ) e. I ) ) )
49 46 48 ax-mp 
 |-  ( I e. ( SubRng ` R ) <-> ( I e. ( SubGrp ` R ) /\ A. x e. I A. y e. I ( x ( .r ` R ) y ) e. I ) )
50 3 45 49 mpbir2an 
 |-  I e. ( SubRng ` R )