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	⊢ ( ℤring ×s ℤring ) ∈ Ring

Proof

Step	Hyp	Ref	Expression
1		zringring	⊢ ℤring ∈ Ring
2		eqid	⊢ ( ℤring ×s ℤring ) = ( ℤring ×s ℤring )
3		id	⊢ ( ℤring ∈ Ring → ℤring ∈ Ring )
4	2 3 3	xpsringd	⊢ ( ℤring ∈ Ring → ( ℤring ×s ℤring ) ∈ Ring )
5	1 4	ax-mp	⊢ ( ℤring ×s ℤring ) ∈ Ring