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	⊢ 𝑅 = ( ℤring ×s ℤring )
Assertion	pzriprnglem1	⊢ 𝑅 ∈ Rng

Proof

Step	Hyp	Ref	Expression
1		pzriprng.r	⊢ 𝑅 = ( ℤring ×s ℤring )
2		zringrng	⊢ ℤring ∈ Rng
3		id	⊢ ( ℤring ∈ Rng → ℤring ∈ Rng )
4	1 3 3	xpsrngd	⊢ ( ℤring ∈ Rng → 𝑅 ∈ Rng )
5	2 4	ax-mp	⊢ 𝑅 ∈ Rng