Theorem pzriprnglem1

Description: Lemma 1 for pzriprng : R is a non-unital (actually a unital!) ring. (Contributed by AV, 17-Mar-2025)

	Ref	Expression
Hypothesis	pzriprng.r	$$⊢R={\mathbb{Z}}_{\mathrm{ring}}{\times }_{𝑠}{\mathbb{Z}}_{\mathrm{ring}}$$
Assertion	pzriprnglem1	$$⊢R\in \mathrm{Rng}$$

Proof

Step	Hyp	Ref	Expression
1		pzriprng.r	$$⊢R={\mathbb{Z}}_{\mathrm{ring}}{\times }_{𝑠}{\mathbb{Z}}_{\mathrm{ring}}$$
2		zringrng	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Rng}$$
3		id	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Rng}\to {\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Rng}$$
4	1 3 3	xpsrngd	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Rng}\to R\in \mathrm{Rng}$$
5	2 4	ax-mp	$$⊢R\in \mathrm{Rng}$$