Theorem pzriprnglem2

Description: Lemma 2 for pzriprng : The base set of R is the cartesian product of the integers. (Contributed by AV, 17-Mar-2025)

	Ref	Expression
Hypothesis	pzriprng.r	|- R = ( ZZring Xs. ZZring )
Assertion	pzriprnglem2	|- ( Base ` R ) = ( ZZ X. ZZ )

Proof

Step	Hyp	Ref	Expression
1		pzriprng.r	|- R = ( ZZring Xs. ZZring )
2		zringring	|- ZZring e. Ring
3		zringbas	|- ZZ = ( Base ` ZZring )
4		id	|- ( ZZring e. Ring -> ZZring e. Ring )
5	1 3 3 4 4	xpsbas	|- ( ZZring e. Ring -> ( ZZ X. ZZ ) = ( Base ` R ) )
6	2 5	ax-mp	|- ( ZZ X. ZZ ) = ( Base ` R )
7	6	eqcomi	|- ( Base ` R ) = ( ZZ X. ZZ )