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 ‘ ( ℤring ×s ℤring ) ) = ⟨ 1 , 1 ⟩

Proof

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