Theorem pzriprng1

Description: The ring unity of the ring ( ZZring Xs. ZZring ) . Direct proof in contrast to pzriprng1ALT . (Contributed by AV, 25-Mar-2025)

	Ref	Expression
Assertion	pzriprng1	$$⊢1_{\left({\mathbb{Z}}_{\mathrm{ring}}{\times }_{𝑠}{\mathbb{Z}}_{\mathrm{ring}}\right)}=⟨1,1⟩$$

Proof

Step	Hyp	Ref	Expression
1		zringring	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}$$
2		eqid	$$⊢{\mathbb{Z}}_{\mathrm{ring}}{\times }_{𝑠}{\mathbb{Z}}_{\mathrm{ring}}={\mathbb{Z}}_{\mathrm{ring}}{\times }_{𝑠}{\mathbb{Z}}_{\mathrm{ring}}$$
3		id	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}\to {\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}$$
4	2 3 3	xpsring1d	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}\to 1_{\left({\mathbb{Z}}_{\mathrm{ring}}{\times }_{𝑠}{\mathbb{Z}}_{\mathrm{ring}}\right)}=⟨1_{{\mathbb{Z}}_{\mathrm{ring}}},1_{{\mathbb{Z}}_{\mathrm{ring}}}⟩$$
5	1 4	ax-mp	$$⊢1_{\left({\mathbb{Z}}_{\mathrm{ring}}{\times }_{𝑠}{\mathbb{Z}}_{\mathrm{ring}}\right)}=⟨1_{{\mathbb{Z}}_{\mathrm{ring}}},1_{{\mathbb{Z}}_{\mathrm{ring}}}⟩$$
6		zring1	$$⊢1=1_{{\mathbb{Z}}_{\mathrm{ring}}}$$
7	6 6	opeq12i	$$⊢⟨1,1⟩=⟨1_{{\mathbb{Z}}_{\mathrm{ring}}},1_{{\mathbb{Z}}_{\mathrm{ring}}}⟩$$
8	5 7	eqtr4i	$$⊢1_{\left({\mathbb{Z}}_{\mathrm{ring}}{\times }_{𝑠}{\mathbb{Z}}_{\mathrm{ring}}\right)}=⟨1,1⟩$$