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={\mathbb{Z}}_{\mathrm{ring}}{\times }_{𝑠}{\mathbb{Z}}_{\mathrm{ring}}$$
Assertion	pzriprnglem2	$$⊢{\mathrm{Base}}_R=\mathbb{Z}\times \mathbb{Z}$$

Proof

Step	Hyp	Ref	Expression
1		pzriprng.r	$$⊢R={\mathbb{Z}}_{\mathrm{ring}}{\times }_{𝑠}{\mathbb{Z}}_{\mathrm{ring}}$$
2		zringring	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}$$
3		zringbas	$$⊢\mathbb{Z}={\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
4		id	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}\to {\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}$$
5	1 3 3 4 4	xpsbas	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}\to \mathbb{Z}\times \mathbb{Z}={\mathrm{Base}}_R$$
6	2 5	ax-mp	$$⊢\mathbb{Z}\times \mathbb{Z}={\mathrm{Base}}_R$$
7	6	eqcomi	$$⊢{\mathrm{Base}}_R=\mathbb{Z}\times \mathbb{Z}$$