Theorem pzriprng

Description: The non-unital ring ( ZZring Xs. ZZring ) is unital. Direct proof in contrast to pzriprngALT . (Contributed by AV, 25-Mar-2025)

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

Proof

Step	Hyp	Ref	Expression
1		zringring	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}$$
2		eqid	$$⊢{\mathbb{Z}}_{\mathrm{ring}}{\times }_{𝑠}{\mathbb{Z}}_{\mathrm{ring}}={\mathbb{Z}}_{\mathrm{ring}}{\times }_{𝑠}{\mathbb{Z}}_{\mathrm{ring}}$$
3		id	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}\to {\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}$$
4	2 3 3	xpsringd	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}\to {\mathbb{Z}}_{\mathrm{ring}}{\times }_{𝑠}{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}$$
5	1 4	ax-mp	$$⊢{\mathbb{Z}}_{\mathrm{ring}}{\times }_{𝑠}{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}$$