Metamath Proof Explorer

Theorem pzriprngALT

Description: The non-unital ring ( ZZring Xs. ZZring ) is unital because it has the two-sided ideal ( ZZ X. { 0 } ) , which is unital, and the quotient of the ring and the ideal is also unital (using ring2idlqusb ). (Contributed by AV, 23-Mar-2025) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion pzriprngALT 
|- ( ZZring Xs. ZZring ) e. Ring

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( i = ( ZZ X. { 0 } ) -> ( ( ZZring Xs. ZZring ) |`s i ) = ( ( ZZring Xs. ZZring ) |`s ( ZZ X. { 0 } ) ) )
2 1 eleq1d 
 |-  ( i = ( ZZ X. { 0 } ) -> ( ( ( ZZring Xs. ZZring ) |`s i ) e. Ring <-> ( ( ZZring Xs. ZZring ) |`s ( ZZ X. { 0 } ) ) e. Ring ) )
3 oveq2 
 |-  ( i = ( ZZ X. { 0 } ) -> ( ( ZZring Xs. ZZring ) ~QG i ) = ( ( ZZring Xs. ZZring ) ~QG ( ZZ X. { 0 } ) ) )
4 3 oveq2d 
 |-  ( i = ( ZZ X. { 0 } ) -> ( ( ZZring Xs. ZZring ) /s ( ( ZZring Xs. ZZring ) ~QG i ) ) = ( ( ZZring Xs. ZZring ) /s ( ( ZZring Xs. ZZring ) ~QG ( ZZ X. { 0 } ) ) ) )
5 4 eleq1d 
 |-  ( i = ( ZZ X. { 0 } ) -> ( ( ( ZZring Xs. ZZring ) /s ( ( ZZring Xs. ZZring ) ~QG i ) ) e. Ring <-> ( ( ZZring Xs. ZZring ) /s ( ( ZZring Xs. ZZring ) ~QG ( ZZ X. { 0 } ) ) ) e. Ring ) )
6 2 5 anbi12d 
 |-  ( i = ( ZZ X. { 0 } ) -> ( ( ( ( ZZring Xs. ZZring ) |`s i ) e. Ring /\ ( ( ZZring Xs. ZZring ) /s ( ( ZZring Xs. ZZring ) ~QG i ) ) e. Ring ) <-> ( ( ( ZZring Xs. ZZring ) |`s ( ZZ X. { 0 } ) ) e. Ring /\ ( ( ZZring Xs. ZZring ) /s ( ( ZZring Xs. ZZring ) ~QG ( ZZ X. { 0 } ) ) ) e. Ring ) ) )
7 eqid 
 |-  ( ZZring Xs. ZZring ) = ( ZZring Xs. ZZring )
8 eqid 
 |-  ( ZZ X. { 0 } ) = ( ZZ X. { 0 } )
9 eqid 
 |-  ( ( ZZring Xs. ZZring ) |`s ( ZZ X. { 0 } ) ) = ( ( ZZring Xs. ZZring ) |`s ( ZZ X. { 0 } ) )
10 7 8 9 pzriprnglem8 
 |-  ( ZZ X. { 0 } ) e. ( 2Ideal ` ( ZZring Xs. ZZring ) )
11 10 a1i 
 |-  ( T. -> ( ZZ X. { 0 } ) e. ( 2Ideal ` ( ZZring Xs. ZZring ) ) )
12 7 8 9 pzriprnglem7 
 |-  ( ( ZZring Xs. ZZring ) |`s ( ZZ X. { 0 } ) ) e. Ring
13 12 a1i 
 |-  ( T. -> ( ( ZZring Xs. ZZring ) |`s ( ZZ X. { 0 } ) ) e. Ring )
14 eqid 
 |-  ( 1r ` ( ( ZZring Xs. ZZring ) |`s ( ZZ X. { 0 } ) ) ) = ( 1r ` ( ( ZZring Xs. ZZring ) |`s ( ZZ X. { 0 } ) ) )
15 eqid 
 |-  ( ( ZZring Xs. ZZring ) ~QG ( ZZ X. { 0 } ) ) = ( ( ZZring Xs. ZZring ) ~QG ( ZZ X. { 0 } ) )
16 eqid 
 |-  ( ( ZZring Xs. ZZring ) /s ( ( ZZring Xs. ZZring ) ~QG ( ZZ X. { 0 } ) ) ) = ( ( ZZring Xs. ZZring ) /s ( ( ZZring Xs. ZZring ) ~QG ( ZZ X. { 0 } ) ) )
17 7 8 9 14 15 16 pzriprnglem13 
 |-  ( ( ZZring Xs. ZZring ) /s ( ( ZZring Xs. ZZring ) ~QG ( ZZ X. { 0 } ) ) ) e. Ring
18 13 17 jctir 
 |-  ( T. -> ( ( ( ZZring Xs. ZZring ) |`s ( ZZ X. { 0 } ) ) e. Ring /\ ( ( ZZring Xs. ZZring ) /s ( ( ZZring Xs. ZZring ) ~QG ( ZZ X. { 0 } ) ) ) e. Ring ) )
19 6 11 18 rspcedvdw 
 |-  ( T. -> E. i e. ( 2Ideal ` ( ZZring Xs. ZZring ) ) ( ( ( ZZring Xs. ZZring ) |`s i ) e. Ring /\ ( ( ZZring Xs. ZZring ) /s ( ( ZZring Xs. ZZring ) ~QG i ) ) e. Ring ) )
20 19 mptru 
 |-  E. i e. ( 2Ideal ` ( ZZring Xs. ZZring ) ) ( ( ( ZZring Xs. ZZring ) |`s i ) e. Ring /\ ( ( ZZring Xs. ZZring ) /s ( ( ZZring Xs. ZZring ) ~QG i ) ) e. Ring )
21 7 pzriprnglem1 
 |-  ( ZZring Xs. ZZring ) e. Rng
22 ring2idlqusb 
 |-  ( ( ZZring Xs. ZZring ) e. Rng -> ( ( ZZring Xs. ZZring ) e. Ring <-> E. i e. ( 2Ideal ` ( ZZring Xs. ZZring ) ) ( ( ( ZZring Xs. ZZring ) |`s i ) e. Ring /\ ( ( ZZring Xs. ZZring ) /s ( ( ZZring Xs. ZZring ) ~QG i ) ) e. Ring ) ) )
23 21 22 ax-mp 
 |-  ( ( ZZring Xs. ZZring ) e. Ring <-> E. i e. ( 2Ideal ` ( ZZring Xs. ZZring ) ) ( ( ( ZZring Xs. ZZring ) |`s i ) e. Ring /\ ( ( ZZring Xs. ZZring ) /s ( ( ZZring Xs. ZZring ) ~QG i ) ) e. Ring ) )
24 20 23 mpbir 
 |-  ( ZZring Xs. ZZring ) e. Ring