Metamath Proof Explorer

Theorem pzriprnglem6

Description: Lemma 6 for pzriprng : J has a ring unity. (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 pzriprnglem6 
|- ( X e. I -> ( ( <. 1 , 0 >. ( .r ` J ) X ) = X /\ ( X ( .r ` J ) <. 1 , 0 >. ) = X ) )

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 pzriprnglem3 
 |-  ( X e. I <-> E. a e. ZZ X = <. a , 0 >. )
5 1 2 pzriprnglem5 
 |-  I e. ( SubRng ` R )
6 eqid 
 |-  ( .r ` R ) = ( .r ` R )
7 3 6 ressmulr 
 |-  ( I e. ( SubRng ` R ) -> ( .r ` R ) = ( .r ` J ) )
8 7 eqcomd 
 |-  ( I e. ( SubRng ` R ) -> ( .r ` J ) = ( .r ` R ) )
9 5 8 ax-mp 
 |-  ( .r ` J ) = ( .r ` R )
10 9 oveqi 
 |-  ( <. 1 , 0 >. ( .r ` J ) <. a , 0 >. ) = ( <. 1 , 0 >. ( .r ` R ) <. a , 0 >. )
11 10 a1i 
 |-  ( a e. ZZ -> ( <. 1 , 0 >. ( .r ` J ) <. a , 0 >. ) = ( <. 1 , 0 >. ( .r ` R ) <. a , 0 >. ) )
12 zringbas 
 |-  ZZ = ( Base ` ZZring )
13 zringring 
 |-  ZZring e. Ring
14 13 a1i 
 |-  ( a e. ZZ -> ZZring e. Ring )
15 1zzd 
 |-  ( a e. ZZ -> 1 e. ZZ )
16 0z 
 |-  0 e. ZZ
17 16 a1i 
 |-  ( a e. ZZ -> 0 e. ZZ )
18 id 
 |-  ( a e. ZZ -> a e. ZZ )
19 zringmulr 
 |-  x. = ( .r ` ZZring )
20 19 oveqi 
 |-  ( 1 x. a ) = ( 1 ( .r ` ZZring ) a )
21 15 18 zmulcld 
 |-  ( a e. ZZ -> ( 1 x. a ) e. ZZ )
22 20 21 eqeltrrid 
 |-  ( a e. ZZ -> ( 1 ( .r ` ZZring ) a ) e. ZZ )
23 19 eqcomi 
 |-  ( .r ` ZZring ) = x.
24 23 oveqi 
 |-  ( 0 ( .r ` ZZring ) 0 ) = ( 0 x. 0 )
25 id 
 |-  ( 0 e. ZZ -> 0 e. ZZ )
26 25 25 zmulcld 
 |-  ( 0 e. ZZ -> ( 0 x. 0 ) e. ZZ )
27 16 26 ax-mp 
 |-  ( 0 x. 0 ) e. ZZ
28 24 27 eqeltri 
 |-  ( 0 ( .r ` ZZring ) 0 ) e. ZZ
29 28 a1i 
 |-  ( a e. ZZ -> ( 0 ( .r ` ZZring ) 0 ) e. ZZ )
30 eqid 
 |-  ( .r ` ZZring ) = ( .r ` ZZring )
31 1 12 12 14 14 15 17 18 17 22 29 30 30 6 xpsmul 
 |-  ( a e. ZZ -> ( <. 1 , 0 >. ( .r ` R ) <. a , 0 >. ) = <. ( 1 ( .r ` ZZring ) a ) , ( 0 ( .r ` ZZring ) 0 ) >. )
32 zcn 
 |-  ( a e. ZZ -> a e. CC )
33 32 mullidd 
 |-  ( a e. ZZ -> ( 1 x. a ) = a )
34 20 33 eqtr3id 
 |-  ( a e. ZZ -> ( 1 ( .r ` ZZring ) a ) = a )
35 0cn 
 |-  0 e. CC
36 35 mul02i 
 |-  ( 0 x. 0 ) = 0
37 24 36 eqtri 
 |-  ( 0 ( .r ` ZZring ) 0 ) = 0
38 37 a1i 
 |-  ( a e. ZZ -> ( 0 ( .r ` ZZring ) 0 ) = 0 )
39 34 38 opeq12d 
 |-  ( a e. ZZ -> <. ( 1 ( .r ` ZZring ) a ) , ( 0 ( .r ` ZZring ) 0 ) >. = <. a , 0 >. )
40 11 31 39 3eqtrd 
 |-  ( a e. ZZ -> ( <. 1 , 0 >. ( .r ` J ) <. a , 0 >. ) = <. a , 0 >. )
41 9 oveqi 
 |-  ( <. a , 0 >. ( .r ` J ) <. 1 , 0 >. ) = ( <. a , 0 >. ( .r ` R ) <. 1 , 0 >. )
42 41 a1i 
 |-  ( a e. ZZ -> ( <. a , 0 >. ( .r ` J ) <. 1 , 0 >. ) = ( <. a , 0 >. ( .r ` R ) <. 1 , 0 >. ) )
43 19 oveqi 
 |-  ( a x. 1 ) = ( a ( .r ` ZZring ) 1 )
44 18 15 zmulcld 
 |-  ( a e. ZZ -> ( a x. 1 ) e. ZZ )
45 43 44 eqeltrrid 
 |-  ( a e. ZZ -> ( a ( .r ` ZZring ) 1 ) e. ZZ )
46 1 12 12 14 14 18 17 15 17 45 29 30 30 6 xpsmul 
 |-  ( a e. ZZ -> ( <. a , 0 >. ( .r ` R ) <. 1 , 0 >. ) = <. ( a ( .r ` ZZring ) 1 ) , ( 0 ( .r ` ZZring ) 0 ) >. )
47 23 oveqi 
 |-  ( a ( .r ` ZZring ) 1 ) = ( a x. 1 )
48 32 mulridd 
 |-  ( a e. ZZ -> ( a x. 1 ) = a )
49 47 48 eqtrid 
 |-  ( a e. ZZ -> ( a ( .r ` ZZring ) 1 ) = a )
50 49 38 opeq12d 
 |-  ( a e. ZZ -> <. ( a ( .r ` ZZring ) 1 ) , ( 0 ( .r ` ZZring ) 0 ) >. = <. a , 0 >. )
51 42 46 50 3eqtrd 
 |-  ( a e. ZZ -> ( <. a , 0 >. ( .r ` J ) <. 1 , 0 >. ) = <. a , 0 >. )
52 40 51 jca 
 |-  ( a e. ZZ -> ( ( <. 1 , 0 >. ( .r ` J ) <. a , 0 >. ) = <. a , 0 >. /\ ( <. a , 0 >. ( .r ` J ) <. 1 , 0 >. ) = <. a , 0 >. ) )
53 oveq2 
 |-  ( X = <. a , 0 >. -> ( <. 1 , 0 >. ( .r ` J ) X ) = ( <. 1 , 0 >. ( .r ` J ) <. a , 0 >. ) )
54 id 
 |-  ( X = <. a , 0 >. -> X = <. a , 0 >. )
55 53 54 eqeq12d 
 |-  ( X = <. a , 0 >. -> ( ( <. 1 , 0 >. ( .r ` J ) X ) = X <-> ( <. 1 , 0 >. ( .r ` J ) <. a , 0 >. ) = <. a , 0 >. ) )
56 oveq1 
 |-  ( X = <. a , 0 >. -> ( X ( .r ` J ) <. 1 , 0 >. ) = ( <. a , 0 >. ( .r ` J ) <. 1 , 0 >. ) )
57 56 54 eqeq12d 
 |-  ( X = <. a , 0 >. -> ( ( X ( .r ` J ) <. 1 , 0 >. ) = X <-> ( <. a , 0 >. ( .r ` J ) <. 1 , 0 >. ) = <. a , 0 >. ) )
58 55 57 anbi12d 
 |-  ( X = <. a , 0 >. -> ( ( ( <. 1 , 0 >. ( .r ` J ) X ) = X /\ ( X ( .r ` J ) <. 1 , 0 >. ) = X ) <-> ( ( <. 1 , 0 >. ( .r ` J ) <. a , 0 >. ) = <. a , 0 >. /\ ( <. a , 0 >. ( .r ` J ) <. 1 , 0 >. ) = <. a , 0 >. ) ) )
59 52 58 syl5ibrcom 
 |-  ( a e. ZZ -> ( X = <. a , 0 >. -> ( ( <. 1 , 0 >. ( .r ` J ) X ) = X /\ ( X ( .r ` J ) <. 1 , 0 >. ) = X ) ) )
60 59 rexlimiv 
 |-  ( E. a e. ZZ X = <. a , 0 >. -> ( ( <. 1 , 0 >. ( .r ` J ) X ) = X /\ ( X ( .r ` J ) <. 1 , 0 >. ) = X ) )
61 4 60 sylbi 
 |-  ( X e. I -> ( ( <. 1 , 0 >. ( .r ` J ) X ) = X /\ ( X ( .r ` J ) <. 1 , 0 >. ) = X ) )