Metamath Proof Explorer

Theorem pzriprng1ALT

Description: The ring unity of the ring ( ZZring Xs. ZZring ) constructed from the ring unity of the two-sided ideal ( ZZ X. { 0 } ) and the ring unity of the quotient of the ring and the ideal (using ring2idlqus1 ). (Contributed by AV, 24-Mar-2025) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion pzriprng1ALT 
|- ( 1r ` ( ZZring Xs. ZZring ) ) = <. 1 , 1 >.

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( ZZring Xs. ZZring ) = ( ZZring Xs. ZZring )
2 1 pzriprnglem1 
 |-  ( ZZring Xs. ZZring ) e. Rng
3 eqid 
 |-  ( ZZ X. { 0 } ) = ( ZZ X. { 0 } )
4 eqid 
 |-  ( ( ZZring Xs. ZZring ) |`s ( ZZ X. { 0 } ) ) = ( ( ZZring Xs. ZZring ) |`s ( ZZ X. { 0 } ) )
5 1 3 4 pzriprnglem8 
 |-  ( ZZ X. { 0 } ) e. ( 2Ideal ` ( ZZring Xs. ZZring ) )
6 2 5 pm3.2i 
 |-  ( ( ZZring Xs. ZZring ) e. Rng /\ ( ZZ X. { 0 } ) e. ( 2Ideal ` ( ZZring Xs. ZZring ) ) )
7 1 3 4 pzriprnglem7 
 |-  ( ( ZZring Xs. ZZring ) |`s ( ZZ X. { 0 } ) ) e. Ring
8 eqid 
 |-  ( 1r ` ( ( ZZring Xs. ZZring ) |`s ( ZZ X. { 0 } ) ) ) = ( 1r ` ( ( ZZring Xs. ZZring ) |`s ( ZZ X. { 0 } ) ) )
9 eqid 
 |-  ( ( ZZring Xs. ZZring ) ~QG ( ZZ X. { 0 } ) ) = ( ( ZZring Xs. ZZring ) ~QG ( ZZ X. { 0 } ) )
10 eqid 
 |-  ( ( ZZring Xs. ZZring ) /s ( ( ZZring Xs. ZZring ) ~QG ( ZZ X. { 0 } ) ) ) = ( ( ZZring Xs. ZZring ) /s ( ( ZZring Xs. ZZring ) ~QG ( ZZ X. { 0 } ) ) )
11 1 3 4 8 9 10 pzriprnglem13 
 |-  ( ( ZZring Xs. ZZring ) /s ( ( ZZring Xs. ZZring ) ~QG ( ZZ X. { 0 } ) ) ) e. Ring
12 7 11 pm3.2i 
 |-  ( ( ( ZZring Xs. ZZring ) |`s ( ZZ X. { 0 } ) ) e. Ring /\ ( ( ZZring Xs. ZZring ) /s ( ( ZZring Xs. ZZring ) ~QG ( ZZ X. { 0 } ) ) ) e. Ring )
13 1z 
 |-  1 e. ZZ
14 1ex 
 |-  1 e. _V
15 14 snid 
 |-  1 e. { 1 }
16 13 15 opelxpii 
 |-  <. 1 , 1 >. e. ( ZZ X. { 1 } )
17 1 3 4 8 9 10 pzriprnglem14 
 |-  ( 1r ` ( ( ZZring Xs. ZZring ) /s ( ( ZZring Xs. ZZring ) ~QG ( ZZ X. { 0 } ) ) ) ) = ( ZZ X. { 1 } )
18 16 17 eleqtrri 
 |-  <. 1 , 1 >. e. ( 1r ` ( ( ZZring Xs. ZZring ) /s ( ( ZZring Xs. ZZring ) ~QG ( ZZ X. { 0 } ) ) ) )
19 eqid 
 |-  ( .r ` ( ZZring Xs. ZZring ) ) = ( .r ` ( ZZring Xs. ZZring ) )
20 eqid 
 |-  ( -g ` ( ZZring Xs. ZZring ) ) = ( -g ` ( ZZring Xs. ZZring ) )
21 eqid 
 |-  ( +g ` ( ZZring Xs. ZZring ) ) = ( +g ` ( ZZring Xs. ZZring ) )
22 19 8 20 21 ring2idlqus1 
 |-  ( ( ( ( ZZring Xs. ZZring ) e. Rng /\ ( ZZ X. { 0 } ) e. ( 2Ideal ` ( ZZring Xs. ZZring ) ) ) /\ ( ( ( ZZring Xs. ZZring ) |`s ( ZZ X. { 0 } ) ) e. Ring /\ ( ( ZZring Xs. ZZring ) /s ( ( ZZring Xs. ZZring ) ~QG ( ZZ X. { 0 } ) ) ) e. Ring ) /\ <. 1 , 1 >. e. ( 1r ` ( ( ZZring Xs. ZZring ) /s ( ( ZZring Xs. ZZring ) ~QG ( ZZ X. { 0 } ) ) ) ) ) -> ( ( ZZring Xs. ZZring ) e. Ring /\ ( 1r ` ( ZZring Xs. ZZring ) ) = ( ( <. 1 , 1 >. ( -g ` ( ZZring Xs. ZZring ) ) ( ( 1r ` ( ( ZZring Xs. ZZring ) |`s ( ZZ X. { 0 } ) ) ) ( .r ` ( ZZring Xs. ZZring ) ) <. 1 , 1 >. ) ) ( +g ` ( ZZring Xs. ZZring ) ) ( 1r ` ( ( ZZring Xs. ZZring ) |`s ( ZZ X. { 0 } ) ) ) ) ) )
23 22 simprd 
 |-  ( ( ( ( ZZring Xs. ZZring ) e. Rng /\ ( ZZ X. { 0 } ) e. ( 2Ideal ` ( ZZring Xs. ZZring ) ) ) /\ ( ( ( ZZring Xs. ZZring ) |`s ( ZZ X. { 0 } ) ) e. Ring /\ ( ( ZZring Xs. ZZring ) /s ( ( ZZring Xs. ZZring ) ~QG ( ZZ X. { 0 } ) ) ) e. Ring ) /\ <. 1 , 1 >. e. ( 1r ` ( ( ZZring Xs. ZZring ) /s ( ( ZZring Xs. ZZring ) ~QG ( ZZ X. { 0 } ) ) ) ) ) -> ( 1r ` ( ZZring Xs. ZZring ) ) = ( ( <. 1 , 1 >. ( -g ` ( ZZring Xs. ZZring ) ) ( ( 1r ` ( ( ZZring Xs. ZZring ) |`s ( ZZ X. { 0 } ) ) ) ( .r ` ( ZZring Xs. ZZring ) ) <. 1 , 1 >. ) ) ( +g ` ( ZZring Xs. ZZring ) ) ( 1r ` ( ( ZZring Xs. ZZring ) |`s ( ZZ X. { 0 } ) ) ) ) )
24 6 12 18 23 mp3an 
 |-  ( 1r ` ( ZZring Xs. ZZring ) ) = ( ( <. 1 , 1 >. ( -g ` ( ZZring Xs. ZZring ) ) ( ( 1r ` ( ( ZZring Xs. ZZring ) |`s ( ZZ X. { 0 } ) ) ) ( .r ` ( ZZring Xs. ZZring ) ) <. 1 , 1 >. ) ) ( +g ` ( ZZring Xs. ZZring ) ) ( 1r ` ( ( ZZring Xs. ZZring ) |`s ( ZZ X. { 0 } ) ) ) )
25 1 3 4 8 pzriprnglem9 
 |-  ( 1r ` ( ( ZZring Xs. ZZring ) |`s ( ZZ X. { 0 } ) ) ) = <. 1 , 0 >.
26 25 oveq1i 
 |-  ( ( 1r ` ( ( ZZring Xs. ZZring ) |`s ( ZZ X. { 0 } ) ) ) ( .r ` ( ZZring Xs. ZZring ) ) <. 1 , 1 >. ) = ( <. 1 , 0 >. ( .r ` ( ZZring Xs. ZZring ) ) <. 1 , 1 >. )
27 26 oveq2i 
 |-  ( <. 1 , 1 >. ( -g ` ( ZZring Xs. ZZring ) ) ( ( 1r ` ( ( ZZring Xs. ZZring ) |`s ( ZZ X. { 0 } ) ) ) ( .r ` ( ZZring Xs. ZZring ) ) <. 1 , 1 >. ) ) = ( <. 1 , 1 >. ( -g ` ( ZZring Xs. ZZring ) ) ( <. 1 , 0 >. ( .r ` ( ZZring Xs. ZZring ) ) <. 1 , 1 >. ) )
28 27 25 oveq12i 
 |-  ( ( <. 1 , 1 >. ( -g ` ( ZZring Xs. ZZring ) ) ( ( 1r ` ( ( ZZring Xs. ZZring ) |`s ( ZZ X. { 0 } ) ) ) ( .r ` ( ZZring Xs. ZZring ) ) <. 1 , 1 >. ) ) ( +g ` ( ZZring Xs. ZZring ) ) ( 1r ` ( ( ZZring Xs. ZZring ) |`s ( ZZ X. { 0 } ) ) ) ) = ( ( <. 1 , 1 >. ( -g ` ( ZZring Xs. ZZring ) ) ( <. 1 , 0 >. ( .r ` ( ZZring Xs. ZZring ) ) <. 1 , 1 >. ) ) ( +g ` ( ZZring Xs. ZZring ) ) <. 1 , 0 >. )
29 zringring 
 |-  ZZring e. Ring
30 zringbas 
 |-  ZZ = ( Base ` ZZring )
31 id 
 |-  ( ZZring e. Ring -> ZZring e. Ring )
32 13 a1i 
 |-  ( ZZring e. Ring -> 1 e. ZZ )
33 0zd 
 |-  ( ZZring e. Ring -> 0 e. ZZ )
34 zmulcl 
 |-  ( ( 1 e. ZZ /\ 1 e. ZZ ) -> ( 1 x. 1 ) e. ZZ )
35 13 13 34 mp2an 
 |-  ( 1 x. 1 ) e. ZZ
36 35 a1i 
 |-  ( ZZring e. Ring -> ( 1 x. 1 ) e. ZZ )
37 zringmulr 
 |-  x. = ( .r ` ZZring )
38 37 eqcomi 
 |-  ( .r ` ZZring ) = x.
39 38 oveqi 
 |-  ( 0 ( .r ` ZZring ) 1 ) = ( 0 x. 1 )
40 0z 
 |-  0 e. ZZ
41 zmulcl 
 |-  ( ( 0 e. ZZ /\ 1 e. ZZ ) -> ( 0 x. 1 ) e. ZZ )
42 40 13 41 mp2an 
 |-  ( 0 x. 1 ) e. ZZ
43 39 42 eqeltri 
 |-  ( 0 ( .r ` ZZring ) 1 ) e. ZZ
44 43 a1i 
 |-  ( ZZring e. Ring -> ( 0 ( .r ` ZZring ) 1 ) e. ZZ )
45 eqid 
 |-  ( .r ` ZZring ) = ( .r ` ZZring )
46 1 30 30 31 31 32 33 32 32 36 44 37 45 19 xpsmul 
 |-  ( ZZring e. Ring -> ( <. 1 , 0 >. ( .r ` ( ZZring Xs. ZZring ) ) <. 1 , 1 >. ) = <. ( 1 x. 1 ) , ( 0 ( .r ` ZZring ) 1 ) >. )
47 29 46 ax-mp 
 |-  ( <. 1 , 0 >. ( .r ` ( ZZring Xs. ZZring ) ) <. 1 , 1 >. ) = <. ( 1 x. 1 ) , ( 0 ( .r ` ZZring ) 1 ) >.
48 47 oveq2i 
 |-  ( <. 1 , 1 >. ( -g ` ( ZZring Xs. ZZring ) ) ( <. 1 , 0 >. ( .r ` ( ZZring Xs. ZZring ) ) <. 1 , 1 >. ) ) = ( <. 1 , 1 >. ( -g ` ( ZZring Xs. ZZring ) ) <. ( 1 x. 1 ) , ( 0 ( .r ` ZZring ) 1 ) >. )
49 1t1e1 
 |-  ( 1 x. 1 ) = 1
50 ax-1cn 
 |-  1 e. CC
51 50 mul02i 
 |-  ( 0 x. 1 ) = 0
52 39 51 eqtri 
 |-  ( 0 ( .r ` ZZring ) 1 ) = 0
53 49 52 opeq12i 
 |-  <. ( 1 x. 1 ) , ( 0 ( .r ` ZZring ) 1 ) >. = <. 1 , 0 >.
54 53 oveq2i 
 |-  ( <. 1 , 1 >. ( -g ` ( ZZring Xs. ZZring ) ) <. ( 1 x. 1 ) , ( 0 ( .r ` ZZring ) 1 ) >. ) = ( <. 1 , 1 >. ( -g ` ( ZZring Xs. ZZring ) ) <. 1 , 0 >. )
55 zringgrp 
 |-  ZZring e. Grp
56 55 a1i 
 |-  ( 1 e. ZZ -> ZZring e. Grp )
57 id 
 |-  ( 1 e. ZZ -> 1 e. ZZ )
58 0zd 
 |-  ( 1 e. ZZ -> 0 e. ZZ )
59 eqid 
 |-  ( -g ` ZZring ) = ( -g ` ZZring )
60 1 30 30 56 56 57 57 57 58 59 59 20 xpsgrpsub 
 |-  ( 1 e. ZZ -> ( <. 1 , 1 >. ( -g ` ( ZZring Xs. ZZring ) ) <. 1 , 0 >. ) = <. ( 1 ( -g ` ZZring ) 1 ) , ( 1 ( -g ` ZZring ) 0 ) >. )
61 13 60 ax-mp 
 |-  ( <. 1 , 1 >. ( -g ` ( ZZring Xs. ZZring ) ) <. 1 , 0 >. ) = <. ( 1 ( -g ` ZZring ) 1 ) , ( 1 ( -g ` ZZring ) 0 ) >.
62 48 54 61 3eqtri 
 |-  ( <. 1 , 1 >. ( -g ` ( ZZring Xs. ZZring ) ) ( <. 1 , 0 >. ( .r ` ( ZZring Xs. ZZring ) ) <. 1 , 1 >. ) ) = <. ( 1 ( -g ` ZZring ) 1 ) , ( 1 ( -g ` ZZring ) 0 ) >.
63 62 oveq1i 
 |-  ( ( <. 1 , 1 >. ( -g ` ( ZZring Xs. ZZring ) ) ( <. 1 , 0 >. ( .r ` ( ZZring Xs. ZZring ) ) <. 1 , 1 >. ) ) ( +g ` ( ZZring Xs. ZZring ) ) <. 1 , 0 >. ) = ( <. ( 1 ( -g ` ZZring ) 1 ) , ( 1 ( -g ` ZZring ) 0 ) >. ( +g ` ( ZZring Xs. ZZring ) ) <. 1 , 0 >. )
64 59 zringsub 
 |-  ( ( 1 e. ZZ /\ 1 e. ZZ ) -> ( 1 ( -g ` ZZring ) 1 ) = ( 1 - 1 ) )
65 13 13 64 mp2an 
 |-  ( 1 ( -g ` ZZring ) 1 ) = ( 1 - 1 )
66 1m1e0 
 |-  ( 1 - 1 ) = 0
67 65 66 eqtri 
 |-  ( 1 ( -g ` ZZring ) 1 ) = 0
68 59 zringsub 
 |-  ( ( 1 e. ZZ /\ 0 e. ZZ ) -> ( 1 ( -g ` ZZring ) 0 ) = ( 1 - 0 ) )
69 13 40 68 mp2an 
 |-  ( 1 ( -g ` ZZring ) 0 ) = ( 1 - 0 )
70 67 69 opeq12i 
 |-  <. ( 1 ( -g ` ZZring ) 1 ) , ( 1 ( -g ` ZZring ) 0 ) >. = <. 0 , ( 1 - 0 ) >.
71 70 oveq1i 
 |-  ( <. ( 1 ( -g ` ZZring ) 1 ) , ( 1 ( -g ` ZZring ) 0 ) >. ( +g ` ( ZZring Xs. ZZring ) ) <. 1 , 0 >. ) = ( <. 0 , ( 1 - 0 ) >. ( +g ` ( ZZring Xs. ZZring ) ) <. 1 , 0 >. )
72 1m0e1 
 |-  ( 1 - 0 ) = 1
73 72 opeq2i 
 |-  <. 0 , ( 1 - 0 ) >. = <. 0 , 1 >.
74 73 oveq1i 
 |-  ( <. 0 , ( 1 - 0 ) >. ( +g ` ( ZZring Xs. ZZring ) ) <. 1 , 0 >. ) = ( <. 0 , 1 >. ( +g ` ( ZZring Xs. ZZring ) ) <. 1 , 0 >. )
75 29 a1i 
 |-  ( 1 e. ZZ -> ZZring e. Ring )
76 58 57 zaddcld 
 |-  ( 1 e. ZZ -> ( 0 + 1 ) e. ZZ )
77 57 58 zaddcld 
 |-  ( 1 e. ZZ -> ( 1 + 0 ) e. ZZ )
78 zringplusg 
 |-  + = ( +g ` ZZring )
79 1 30 30 75 75 58 57 57 58 76 77 78 78 21 xpsadd 
 |-  ( 1 e. ZZ -> ( <. 0 , 1 >. ( +g ` ( ZZring Xs. ZZring ) ) <. 1 , 0 >. ) = <. ( 0 + 1 ) , ( 1 + 0 ) >. )
80 13 79 ax-mp 
 |-  ( <. 0 , 1 >. ( +g ` ( ZZring Xs. ZZring ) ) <. 1 , 0 >. ) = <. ( 0 + 1 ) , ( 1 + 0 ) >.
81 0p1e1 
 |-  ( 0 + 1 ) = 1
82 1p0e1 
 |-  ( 1 + 0 ) = 1
83 81 82 opeq12i 
 |-  <. ( 0 + 1 ) , ( 1 + 0 ) >. = <. 1 , 1 >.
84 74 80 83 3eqtri 
 |-  ( <. 0 , ( 1 - 0 ) >. ( +g ` ( ZZring Xs. ZZring ) ) <. 1 , 0 >. ) = <. 1 , 1 >.
85 63 71 84 3eqtri 
 |-  ( ( <. 1 , 1 >. ( -g ` ( ZZring Xs. ZZring ) ) ( <. 1 , 0 >. ( .r ` ( ZZring Xs. ZZring ) ) <. 1 , 1 >. ) ) ( +g ` ( ZZring Xs. ZZring ) ) <. 1 , 0 >. ) = <. 1 , 1 >.
86 24 28 85 3eqtri 
 |-  ( 1r ` ( ZZring Xs. ZZring ) ) = <. 1 , 1 >.