Metamath Proof Explorer

Theorem pzriprnglem7

Description: Lemma 7 for pzriprng : J is a unital ring. (Contributed by AV, 19-Mar-2025)

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

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 2 pzriprnglem5 
 |-  I e. ( SubRng ` R )
5 3 subrngrng 
 |-  ( I e. ( SubRng ` R ) -> J e. Rng )
6 4 5 ax-mp 
 |-  J e. Rng
7 1z 
 |-  1 e. ZZ
8 c0ex 
 |-  0 e. _V
9 8 snid 
 |-  0 e. { 0 }
10 7 9 opelxpii 
 |-  <. 1 , 0 >. e. ( ZZ X. { 0 } )
11 3 subrngbas 
 |-  ( I e. ( SubRng ` R ) -> I = ( Base ` J ) )
12 4 11 ax-mp 
 |-  I = ( Base ` J )
13 12 2 eqtr3i 
 |-  ( Base ` J ) = ( ZZ X. { 0 } )
14 10 13 eleqtrri 
 |-  <. 1 , 0 >. e. ( Base ` J )
15 oveq1 
 |-  ( i = <. 1 , 0 >. -> ( i ( .r ` J ) x ) = ( <. 1 , 0 >. ( .r ` J ) x ) )
16 15 eqeq1d 
 |-  ( i = <. 1 , 0 >. -> ( ( i ( .r ` J ) x ) = x <-> ( <. 1 , 0 >. ( .r ` J ) x ) = x ) )
17 16 ovanraleqv 
 |-  ( i = <. 1 , 0 >. -> ( A. x e. ( Base ` J ) ( ( i ( .r ` J ) x ) = x /\ ( x ( .r ` J ) i ) = x ) <-> A. x e. ( Base ` J ) ( ( <. 1 , 0 >. ( .r ` J ) x ) = x /\ ( x ( .r ` J ) <. 1 , 0 >. ) = x ) ) )
18 id 
 |-  ( <. 1 , 0 >. e. ( Base ` J ) -> <. 1 , 0 >. e. ( Base ` J ) )
19 12 eleq2i 
 |-  ( x e. I <-> x e. ( Base ` J ) )
20 1 2 3 pzriprnglem6 
 |-  ( x e. I -> ( ( <. 1 , 0 >. ( .r ` J ) x ) = x /\ ( x ( .r ` J ) <. 1 , 0 >. ) = x ) )
21 19 20 sylbir 
 |-  ( x e. ( Base ` J ) -> ( ( <. 1 , 0 >. ( .r ` J ) x ) = x /\ ( x ( .r ` J ) <. 1 , 0 >. ) = x ) )
22 21 a1i 
 |-  ( <. 1 , 0 >. e. ( Base ` J ) -> ( x e. ( Base ` J ) -> ( ( <. 1 , 0 >. ( .r ` J ) x ) = x /\ ( x ( .r ` J ) <. 1 , 0 >. ) = x ) ) )
23 22 ralrimiv 
 |-  ( <. 1 , 0 >. e. ( Base ` J ) -> A. x e. ( Base ` J ) ( ( <. 1 , 0 >. ( .r ` J ) x ) = x /\ ( x ( .r ` J ) <. 1 , 0 >. ) = x ) )
24 17 18 23 rspcedvdw 
 |-  ( <. 1 , 0 >. e. ( Base ` J ) -> E. i e. ( Base ` J ) A. x e. ( Base ` J ) ( ( i ( .r ` J ) x ) = x /\ ( x ( .r ` J ) i ) = x ) )
25 14 24 ax-mp 
 |-  E. i e. ( Base ` J ) A. x e. ( Base ` J ) ( ( i ( .r ` J ) x ) = x /\ ( x ( .r ` J ) i ) = x )
26 eqid 
 |-  ( Base ` J ) = ( Base ` J )
27 eqid 
 |-  ( .r ` J ) = ( .r ` J )
28 26 27 isringrng 
 |-  ( J e. Ring <-> ( J e. Rng /\ E. i e. ( Base ` J ) A. x e. ( Base ` J ) ( ( i ( .r ` J ) x ) = x /\ ( x ( .r ` J ) i ) = x ) ) )
29 6 25 28 mpbir2an 
 |-  J e. Ring