Metamath Proof Explorer

Theorem pzriprnglem14

Description: Lemma 14 for pzriprng : The ring unity of the ring Q . (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 pzriprnglem14 
|- ( 1r ` Q ) = ( ZZ X. { 1 } )

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 1z 
 |-  1 e. ZZ
8 sneq 
 |-  ( y = 1 -> { y } = { 1 } )
9 8 xpeq2d 
 |-  ( y = 1 -> ( ZZ X. { y } ) = ( ZZ X. { 1 } ) )
10 9 sneqd 
 |-  ( y = 1 -> { ( ZZ X. { y } ) } = { ( ZZ X. { 1 } ) } )
11 10 eleq2d 
 |-  ( y = 1 -> ( ( ZZ X. { 1 } ) e. { ( ZZ X. { y } ) } <-> ( ZZ X. { 1 } ) e. { ( ZZ X. { 1 } ) } ) )
12 id 
 |-  ( 1 e. ZZ -> 1 e. ZZ )
13 zex 
 |-  ZZ e. _V
14 snex 
 |-  { 1 } e. _V
15 13 14 xpex 
 |-  ( ZZ X. { 1 } ) e. _V
16 15 snid 
 |-  ( ZZ X. { 1 } ) e. { ( ZZ X. { 1 } ) }
17 16 a1i 
 |-  ( 1 e. ZZ -> ( ZZ X. { 1 } ) e. { ( ZZ X. { 1 } ) } )
18 11 12 17 rspcedvdw 
 |-  ( 1 e. ZZ -> E. y e. ZZ ( ZZ X. { 1 } ) e. { ( ZZ X. { y } ) } )
19 7 18 ax-mp 
 |-  E. y e. ZZ ( ZZ X. { 1 } ) e. { ( ZZ X. { y } ) }
20 1 2 3 4 5 6 pzriprnglem11 
 |-  ( Base ` Q ) = U_ y e. ZZ { ( ZZ X. { y } ) }
21 20 eleq2i 
 |-  ( ( ZZ X. { 1 } ) e. ( Base ` Q ) <-> ( ZZ X. { 1 } ) e. U_ y e. ZZ { ( ZZ X. { y } ) } )
22 eliun 
 |-  ( ( ZZ X. { 1 } ) e. U_ y e. ZZ { ( ZZ X. { y } ) } <-> E. y e. ZZ ( ZZ X. { 1 } ) e. { ( ZZ X. { y } ) } )
23 21 22 bitri 
 |-  ( ( ZZ X. { 1 } ) e. ( Base ` Q ) <-> E. y e. ZZ ( ZZ X. { 1 } ) e. { ( ZZ X. { y } ) } )
24 19 23 mpbir 
 |-  ( ZZ X. { 1 } ) e. ( Base ` Q )
25 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 ) )
26 25 rgen 
 |-  A. x e. ( Base ` Q ) ( ( ( ZZ X. { 1 } ) ( .r ` Q ) x ) = x /\ ( x ( .r ` Q ) ( ZZ X. { 1 } ) ) = x )
27 24 26 pm3.2i 
 |-  ( ( 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 ) )
28 1 2 3 4 5 6 pzriprnglem13 
 |-  Q e. Ring
29 eqid 
 |-  ( Base ` Q ) = ( Base ` Q )
30 eqid 
 |-  ( .r ` Q ) = ( .r ` Q )
31 eqid 
 |-  ( 1r ` Q ) = ( 1r ` Q )
32 29 30 31 isringid 
 |-  ( Q e. Ring -> ( ( ( 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 ) ) <-> ( 1r ` Q ) = ( ZZ X. { 1 } ) ) )
33 28 32 ax-mp 
 |-  ( ( ( 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 ) ) <-> ( 1r ` Q ) = ( ZZ X. { 1 } ) )
34 27 33 mpbi 
 |-  ( 1r ` Q ) = ( ZZ X. { 1 } )