Theorem pzriprngALT

Description: The non-unital ring ( ZZring Xs. ZZring ) is unital because it has the two-sided ideal ( ZZ X. { 0 } ) , which is unital, and the quotient of the ring and the ideal is also unital (using ring2idlqusb ). (Contributed by AV, 23-Mar-2025) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	pzriprngALT	$$⊢{\mathbb{Z}}_{\mathrm{ring}}{\times }_{𝑠}{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}$$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$$⊢i=\mathbb{Z}\times \left\{0\right\}\to \left({\mathbb{Z}}_{\mathrm{ring}}{\times }_{𝑠}{\mathbb{Z}}_{\mathrm{ring}}\right){\upharpoonright }_{𝑠}i=\left({\mathbb{Z}}_{\mathrm{ring}}{\times }_{𝑠}{\mathbb{Z}}_{\mathrm{ring}}\right){\upharpoonright }_{𝑠}\left(\mathbb{Z}\times \left\{0\right\}\right)$$
2	1	eleq1d	$$⊢i=\mathbb{Z}\times \left\{0\right\}\to \left(\left({\mathbb{Z}}_{\mathrm{ring}}{\times }_{𝑠}{\mathbb{Z}}_{\mathrm{ring}}\right){\upharpoonright }_{𝑠}i\in \mathrm{Ring}\leftrightarrow \left({\mathbb{Z}}_{\mathrm{ring}}{\times }_{𝑠}{\mathbb{Z}}_{\mathrm{ring}}\right){\upharpoonright }_{𝑠}\left(\mathbb{Z}\times \left\{0\right\}\right)\in \mathrm{Ring}\right)$$
3		oveq2	$$⊢i=\mathbb{Z}\times \left\{0\right\}\to \left({\mathbb{Z}}_{\mathrm{ring}}{\times }_{𝑠}{\mathbb{Z}}_{\mathrm{ring}}\right){~}_{\mathit{QG}}i=\left({\mathbb{Z}}_{\mathrm{ring}}{\times }_{𝑠}{\mathbb{Z}}_{\mathrm{ring}}\right){~}_{\mathit{QG}}\left(\mathbb{Z}\times \left\{0\right\}\right)$$
4	3	oveq2d	$$⊢i=\mathbb{Z}\times \left\{0\right\}\to \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}}i\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)$$
5	4	eleq1d	$$⊢i=\mathbb{Z}\times \left\{0\right\}\to \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}}i\right)\in \mathrm{Ring}\leftrightarrow \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)$$
6	2 5	anbi12d	$$⊢i=\mathbb{Z}\times \left\{0\right\}\to \left(\left(\left({\mathbb{Z}}_{\mathrm{ring}}{\times }_{𝑠}{\mathbb{Z}}_{\mathrm{ring}}\right){\upharpoonright }_{𝑠}i\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}}i\right)\in \mathrm{Ring}\right)\leftrightarrow \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)\right)$$
7		eqid	$$⊢{\mathbb{Z}}_{\mathrm{ring}}{\times }_{𝑠}{\mathbb{Z}}_{\mathrm{ring}}={\mathbb{Z}}_{\mathrm{ring}}{\times }_{𝑠}{\mathbb{Z}}_{\mathrm{ring}}$$
8		eqid	$$⊢\mathbb{Z}\times \left\{0\right\}=\mathbb{Z}\times \left\{0\right\}$$
9		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)$$
10	7 8 9	pzriprnglem8	$$⊢\mathbb{Z}\times \left\{0\right\}\in \mathrm{2Ideal}\left({\mathbb{Z}}_{\mathrm{ring}}{\times }_{𝑠}{\mathbb{Z}}_{\mathrm{ring}}\right)$$
11	10	a1i	$$⊢\top \to \mathbb{Z}\times \left\{0\right\}\in \mathrm{2Ideal}\left({\mathbb{Z}}_{\mathrm{ring}}{\times }_{𝑠}{\mathbb{Z}}_{\mathrm{ring}}\right)$$
12	7 8 9	pzriprnglem7	$$⊢\left({\mathbb{Z}}_{\mathrm{ring}}{\times }_{𝑠}{\mathbb{Z}}_{\mathrm{ring}}\right){\upharpoonright }_{𝑠}\left(\mathbb{Z}\times \left\{0\right\}\right)\in \mathrm{Ring}$$
13	12	a1i	$$⊢\top \to \left({\mathbb{Z}}_{\mathrm{ring}}{\times }_{𝑠}{\mathbb{Z}}_{\mathrm{ring}}\right){\upharpoonright }_{𝑠}\left(\mathbb{Z}\times \left\{0\right\}\right)\in \mathrm{Ring}$$
14		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)}$$
15		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)$$
16		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)$$
17	7 8 9 14 15 16	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}$$
18	13 17	jctir	$$⊢\top \to \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)$$
19	6 11 18	rspcedvdw	$$⊢\top \to \exists i\in \mathrm{2Ideal}\left({\mathbb{Z}}_{\mathrm{ring}}{\times }_{𝑠}{\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left({\mathbb{Z}}_{\mathrm{ring}}{\times }_{𝑠}{\mathbb{Z}}_{\mathrm{ring}}\right){\upharpoonright }_{𝑠}i\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}}i\right)\in \mathrm{Ring}\right)$$
20	19	mptru	$$⊢\exists i\in \mathrm{2Ideal}\left({\mathbb{Z}}_{\mathrm{ring}}{\times }_{𝑠}{\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left({\mathbb{Z}}_{\mathrm{ring}}{\times }_{𝑠}{\mathbb{Z}}_{\mathrm{ring}}\right){\upharpoonright }_{𝑠}i\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}}i\right)\in \mathrm{Ring}\right)$$
21	7	pzriprnglem1	$$⊢{\mathbb{Z}}_{\mathrm{ring}}{\times }_{𝑠}{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Rng}$$
22		ring2idlqusb	$$⊢{\mathbb{Z}}_{\mathrm{ring}}{\times }_{𝑠}{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Rng}\to \left({\mathbb{Z}}_{\mathrm{ring}}{\times }_{𝑠}{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}\leftrightarrow \exists i\in \mathrm{2Ideal}\left({\mathbb{Z}}_{\mathrm{ring}}{\times }_{𝑠}{\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left({\mathbb{Z}}_{\mathrm{ring}}{\times }_{𝑠}{\mathbb{Z}}_{\mathrm{ring}}\right){\upharpoonright }_{𝑠}i\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}}i\right)\in \mathrm{Ring}\right)\right)$$
23	21 22	ax-mp	$$⊢{\mathbb{Z}}_{\mathrm{ring}}{\times }_{𝑠}{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}\leftrightarrow \exists i\in \mathrm{2Ideal}\left({\mathbb{Z}}_{\mathrm{ring}}{\times }_{𝑠}{\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left({\mathbb{Z}}_{\mathrm{ring}}{\times }_{𝑠}{\mathbb{Z}}_{\mathrm{ring}}\right){\upharpoonright }_{𝑠}i\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}}i\right)\in \mathrm{Ring}\right)$$
24	20 23	mpbir	$$⊢{\mathbb{Z}}_{\mathrm{ring}}{\times }_{𝑠}{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}$$