Metamath Proof Explorer

Theorem pzriprnglem9

Description: Lemma 9 for pzriprng : The ring unity of the ring J . (Contributed by AV, 22-Mar-2025)

Ref Expression
Hypotheses pzriprng.r 
|- R = ( ZZring Xs. ZZring )
pzriprng.i 
|- I = ( ZZ X. { 0 } )
pzriprng.j 
|- J = ( R |`s I )
pzriprng.1 
|- .1. = ( 1r ` J )
Assertion pzriprnglem9 
|- .1. = <. 1 , 0 >.

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 pzriprng.1 
 |-  .1. = ( 1r ` J )
5 1z 
 |-  1 e. ZZ
6 c0ex 
 |-  0 e. _V
7 6 snid 
 |-  0 e. { 0 }
8 2 eleq2i 
 |-  ( <. 1 , 0 >. e. I <-> <. 1 , 0 >. e. ( ZZ X. { 0 } ) )
9 opelxp 
 |-  ( <. 1 , 0 >. e. ( ZZ X. { 0 } ) <-> ( 1 e. ZZ /\ 0 e. { 0 } ) )
10 8 9 bitri 
 |-  ( <. 1 , 0 >. e. I <-> ( 1 e. ZZ /\ 0 e. { 0 } ) )
11 5 7 10 mpbir2an 
 |-  <. 1 , 0 >. e. I
12 1 2 3 pzriprnglem6 
 |-  ( x e. I -> ( ( <. 1 , 0 >. ( .r ` J ) x ) = x /\ ( x ( .r ` J ) <. 1 , 0 >. ) = x ) )
13 12 rgen 
 |-  A. x e. I ( ( <. 1 , 0 >. ( .r ` J ) x ) = x /\ ( x ( .r ` J ) <. 1 , 0 >. ) = x )
14 11 13 pm3.2i 
 |-  ( <. 1 , 0 >. e. I /\ A. x e. I ( ( <. 1 , 0 >. ( .r ` J ) x ) = x /\ ( x ( .r ` J ) <. 1 , 0 >. ) = x ) )
15 1 2 3 pzriprnglem7 
 |-  J e. Ring
16 1 2 pzriprnglem5 
 |-  I e. ( SubRng ` R )
17 3 subrngbas 
 |-  ( I e. ( SubRng ` R ) -> I = ( Base ` J ) )
18 16 17 ax-mp 
 |-  I = ( Base ` J )
19 eqid 
 |-  ( .r ` J ) = ( .r ` J )
20 18 19 4 isringid 
 |-  ( J e. Ring -> ( ( <. 1 , 0 >. e. I /\ A. x e. I ( ( <. 1 , 0 >. ( .r ` J ) x ) = x /\ ( x ( .r ` J ) <. 1 , 0 >. ) = x ) ) <-> .1. = <. 1 , 0 >. ) )
21 15 20 ax-mp 
 |-  ( ( <. 1 , 0 >. e. I /\ A. x e. I ( ( <. 1 , 0 >. ( .r ` J ) x ) = x /\ ( x ( .r ` J ) <. 1 , 0 >. ) = x ) ) <-> .1. = <. 1 , 0 >. )
22 14 21 mpbi 
 |-  .1. = <. 1 , 0 >.