Metamath Proof Explorer

Theorem pzriprnglem13

Description: Lemma 13 for pzriprng : Q is a unital ring. (Contributed by AV, 23-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 )
pzriprng.g 
|- .~ = ( R ~QG I )
pzriprng.q 
|- Q = ( R /s .~ )
Assertion pzriprnglem13 
|- Q 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 pzriprng.1 
 |-  .1. = ( 1r ` J )
5 pzriprng.g 
 |-  .~ = ( R ~QG I )
6 pzriprng.q 
 |-  Q = ( R /s .~ )
7 1 pzriprnglem1 
 |-  R e. Rng
8 1 2 3 pzriprnglem8 
 |-  I e. ( 2Ideal ` R )
9 1 2 pzriprnglem4 
 |-  I e. ( SubGrp ` R )
10 5 oveq2i 
 |-  ( R /s .~ ) = ( R /s ( R ~QG I ) )
11 6 10 eqtri 
 |-  Q = ( R /s ( R ~QG I ) )
12 eqid 
 |-  ( 2Ideal ` R ) = ( 2Ideal ` R )
13 11 12 qus2idrng 
 |-  ( ( R e. Rng /\ I e. ( 2Ideal ` R ) /\ I e. ( SubGrp ` R ) ) -> Q e. Rng )
14 7 8 9 13 mp3an 
 |-  Q e. Rng
15 1z 
 |-  1 e. ZZ
16 zex 
 |-  ZZ e. _V
17 snex 
 |-  { 1 } e. _V
18 16 17 xpex 
 |-  ( ZZ X. { 1 } ) e. _V
19 18 snid 
 |-  ( ZZ X. { 1 } ) e. { ( ZZ X. { 1 } ) }
20 sneq 
 |-  ( y = 1 -> { y } = { 1 } )
21 20 xpeq2d 
 |-  ( y = 1 -> ( ZZ X. { y } ) = ( ZZ X. { 1 } ) )
22 21 sneqd 
 |-  ( y = 1 -> { ( ZZ X. { y } ) } = { ( ZZ X. { 1 } ) } )
23 22 eleq2d 
 |-  ( y = 1 -> ( ( ZZ X. { 1 } ) e. { ( ZZ X. { y } ) } <-> ( ZZ X. { 1 } ) e. { ( ZZ X. { 1 } ) } ) )
24 23 rspcev 
 |-  ( ( 1 e. ZZ /\ ( ZZ X. { 1 } ) e. { ( ZZ X. { 1 } ) } ) -> E. y e. ZZ ( ZZ X. { 1 } ) e. { ( ZZ X. { y } ) } )
25 15 19 24 mp2an 
 |-  E. y e. ZZ ( ZZ X. { 1 } ) e. { ( ZZ X. { y } ) }
26 eliun 
 |-  ( ( ZZ X. { 1 } ) e. U_ y e. ZZ { ( ZZ X. { y } ) } <-> E. y e. ZZ ( ZZ X. { 1 } ) e. { ( ZZ X. { y } ) } )
27 25 26 mpbir 
 |-  ( ZZ X. { 1 } ) e. U_ y e. ZZ { ( ZZ X. { y } ) }
28 1 2 3 4 5 6 pzriprnglem11 
 |-  ( Base ` Q ) = U_ y e. ZZ { ( ZZ X. { y } ) }
29 27 28 eleqtrri 
 |-  ( ZZ X. { 1 } ) e. ( Base ` Q )
30 oveq1 
 |-  ( i = ( ZZ X. { 1 } ) -> ( i ( .r ` Q ) x ) = ( ( ZZ X. { 1 } ) ( .r ` Q ) x ) )
31 30 eqeq1d 
 |-  ( i = ( ZZ X. { 1 } ) -> ( ( i ( .r ` Q ) x ) = x <-> ( ( ZZ X. { 1 } ) ( .r ` Q ) x ) = x ) )
32 31 ovanraleqv 
 |-  ( i = ( ZZ X. { 1 } ) -> ( A. x e. ( Base ` Q ) ( ( i ( .r ` Q ) x ) = x /\ ( x ( .r ` Q ) i ) = x ) <-> A. x e. ( Base ` Q ) ( ( ( ZZ X. { 1 } ) ( .r ` Q ) x ) = x /\ ( x ( .r ` Q ) ( ZZ X. { 1 } ) ) = x ) ) )
33 id 
 |-  ( ( ZZ X. { 1 } ) e. ( Base ` Q ) -> ( ZZ X. { 1 } ) e. ( Base ` Q ) )
34 1 2 3 4 5 6 pzriprnglem12 
 |-  ( x e. ( Base ` Q ) -> ( ( ( ZZ X. { 1 } ) ( .r ` Q ) x ) = x /\ ( x ( .r ` Q ) ( ZZ X. { 1 } ) ) = x ) )
35 34 a1i 
 |-  ( ( ZZ X. { 1 } ) e. ( Base ` Q ) -> ( x e. ( Base ` Q ) -> ( ( ( ZZ X. { 1 } ) ( .r ` Q ) x ) = x /\ ( x ( .r ` Q ) ( ZZ X. { 1 } ) ) = x ) ) )
36 35 ralrimiv 
 |-  ( ( ZZ X. { 1 } ) e. ( Base ` Q ) -> A. x e. ( Base ` Q ) ( ( ( ZZ X. { 1 } ) ( .r ` Q ) x ) = x /\ ( x ( .r ` Q ) ( ZZ X. { 1 } ) ) = x ) )
37 32 33 36 rspcedvdw 
 |-  ( ( ZZ X. { 1 } ) e. ( Base ` Q ) -> E. i e. ( Base ` Q ) A. x e. ( Base ` Q ) ( ( i ( .r ` Q ) x ) = x /\ ( x ( .r ` Q ) i ) = x ) )
38 29 37 ax-mp 
 |-  E. i e. ( Base ` Q ) A. x e. ( Base ` Q ) ( ( i ( .r ` Q ) x ) = x /\ ( x ( .r ` Q ) i ) = x )
39 eqid 
 |-  ( Base ` Q ) = ( Base ` Q )
40 eqid 
 |-  ( .r ` Q ) = ( .r ` Q )
41 39 40 isringrng 
 |-  ( Q e. Ring <-> ( Q e. Rng /\ E. i e. ( Base ` Q ) A. x e. ( Base ` Q ) ( ( i ( .r ` Q ) x ) = x /\ ( x ( .r ` Q ) i ) = x ) ) )
42 14 38 41 mpbir2an 
 |-  Q e. Ring