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 = ( ZZring Xs. ZZring )
Assertion	pzriprnglem1	|- R e. Rng

Proof

Step	Hyp	Ref	Expression
1		pzriprng.r	|- R = ( ZZring Xs. ZZring )
2		zringrng	|- ZZring e. Rng
3		id	|- ( ZZring e. Rng -> ZZring e. Rng )
4	1 3 3	xpsrngd	|- ( ZZring e. Rng -> R e. Rng )
5	2 4	ax-mp	|- R e. Rng