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	$$⊢1_{\left({\mathbb{Z}}_{\mathrm{ring}}{\times }_{𝑠}{\mathbb{Z}}_{\mathrm{ring}}\right)}=⟨1,1⟩$$

Proof

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