Theorem pzriprnglem14

Description: Lemma 14 for pzriprng : The ring unity of the ring Q . (Contributed by AV, 23-Mar-2025)

	Ref	Expression
Hypotheses	pzriprng.r	$$⊢R={\mathbb{Z}}_{\mathrm{ring}}{\times }_{𝑠}{\mathbb{Z}}_{\mathrm{ring}}$$
	pzriprng.i	$$⊢I=\mathbb{Z}\times \left\{0\right\}$$
	pzriprng.j	$$⊢J=R{\upharpoonright }_{𝑠}I$$
	pzriprng.1	$$⊢\underset{\dot{}}{1}=1_J$$
	pzriprng.g	$$⊢\underset{\dot{}}{\sim }=R{~}_{\mathit{QG}}I$$
	pzriprng.q	$$⊢Q=R{/}_{𝑠}\underset{\dot{}}{\sim }$$
Assertion	pzriprnglem14	$$⊢1_Q=\mathbb{Z}\times \left\{1\right\}$$

Proof

Step	Hyp	Ref	Expression
1		pzriprng.r	$$⊢R={\mathbb{Z}}_{\mathrm{ring}}{\times }_{𝑠}{\mathbb{Z}}_{\mathrm{ring}}$$
2		pzriprng.i	$$⊢I=\mathbb{Z}\times \left\{0\right\}$$
3		pzriprng.j	$$⊢J=R{\upharpoonright }_{𝑠}I$$
4		pzriprng.1	$$⊢\underset{\dot{}}{1}=1_J$$
5		pzriprng.g	$$⊢\underset{\dot{}}{\sim }=R{~}_{\mathit{QG}}I$$
6		pzriprng.q	$$⊢Q=R{/}_{𝑠}\underset{\dot{}}{\sim }$$
7		1z	$$⊢1\in \mathbb{Z}$$
8		sneq	$$⊢y=1\to \left\{y\right\}=\left\{1\right\}$$
9	8	xpeq2d	$$⊢y=1\to \mathbb{Z}\times \left\{y\right\}=\mathbb{Z}\times \left\{1\right\}$$
10	9	sneqd	$$⊢y=1\to \left\{\mathbb{Z}\times \left\{y\right\}\right\}=\left\{\mathbb{Z}\times \left\{1\right\}\right\}$$
11	10	eleq2d	$$⊢y=1\to \left(\mathbb{Z}\times \left\{1\right\}\in \left\{\mathbb{Z}\times \left\{y\right\}\right\}\leftrightarrow \mathbb{Z}\times \left\{1\right\}\in \left\{\mathbb{Z}\times \left\{1\right\}\right\}\right)$$
12		id	$$⊢1\in \mathbb{Z}\to 1\in \mathbb{Z}$$
13		zex	$$⊢\mathbb{Z}\in \mathrm{V}$$
14		snex	$$⊢\left\{1\right\}\in \mathrm{V}$$
15	13 14	xpex	$$⊢\mathbb{Z}\times \left\{1\right\}\in \mathrm{V}$$
16	15	snid	$$⊢\mathbb{Z}\times \left\{1\right\}\in \left\{\mathbb{Z}\times \left\{1\right\}\right\}$$
17	16	a1i	$$⊢1\in \mathbb{Z}\to \mathbb{Z}\times \left\{1\right\}\in \left\{\mathbb{Z}\times \left\{1\right\}\right\}$$
18	11 12 17	rspcedvdw	$$⊢1\in \mathbb{Z}\to \exists y\in \mathbb{Z}\mathbb{Z}\times \left\{1\right\}\in \left\{\mathbb{Z}\times \left\{y\right\}\right\}$$
19	7 18	ax-mp	$$⊢\exists y\in \mathbb{Z}\mathbb{Z}\times \left\{1\right\}\in \left\{\mathbb{Z}\times \left\{y\right\}\right\}$$
20	1 2 3 4 5 6	pzriprnglem11	$$⊢{\mathrm{Base}}_Q=\bigcup _{y\in \mathbb{Z}}\left\{\mathbb{Z}\times \left\{y\right\}\right\}$$
21	20	eleq2i	$$⊢\mathbb{Z}\times \left\{1\right\}\in {\mathrm{Base}}_Q\leftrightarrow \mathbb{Z}\times \left\{1\right\}\in \bigcup _{y\in \mathbb{Z}}\left\{\mathbb{Z}\times \left\{y\right\}\right\}$$
22		eliun	$$⊢\mathbb{Z}\times \left\{1\right\}\in \bigcup _{y\in \mathbb{Z}}\left\{\mathbb{Z}\times \left\{y\right\}\right\}\leftrightarrow \exists y\in \mathbb{Z}\mathbb{Z}\times \left\{1\right\}\in \left\{\mathbb{Z}\times \left\{y\right\}\right\}$$
23	21 22	bitri	$$⊢\mathbb{Z}\times \left\{1\right\}\in {\mathrm{Base}}_Q\leftrightarrow \exists y\in \mathbb{Z}\mathbb{Z}\times \left\{1\right\}\in \left\{\mathbb{Z}\times \left\{y\right\}\right\}$$
24	19 23	mpbir	$$⊢\mathbb{Z}\times \left\{1\right\}\in {\mathrm{Base}}_Q$$
25	1 2 3 4 5 6	pzriprnglem12	$$⊢x\in {\mathrm{Base}}_Q\to \left(\left(\mathbb{Z}\times \left\{1\right\}\right){\cdot }_{Q}x=x\wedge x{\cdot }_Q\left(\mathbb{Z}\times \left\{1\right\}\right)=x\right)$$
26	25	rgen	$$⊢\forall x\in {\mathrm{Base}}_Q\left(\left(\mathbb{Z}\times \left\{1\right\}\right){\cdot }_{Q}x=x\wedge x{\cdot }_Q\left(\mathbb{Z}\times \left\{1\right\}\right)=x\right)$$
27	24 26	pm3.2i	$$⊢\left(\mathbb{Z}\times \left\{1\right\}\in {\mathrm{Base}}_Q\wedge \forall x\in {\mathrm{Base}}_Q\left(\left(\mathbb{Z}\times \left\{1\right\}\right){\cdot }_{Q}x=x\wedge x{\cdot }_Q\left(\mathbb{Z}\times \left\{1\right\}\right)=x\right)\right)$$
28	1 2 3 4 5 6	pzriprnglem13	$$⊢Q\in \mathrm{Ring}$$
29		eqid	$$⊢{\mathrm{Base}}_Q={\mathrm{Base}}_Q$$
30		eqid	$$⊢{\cdot }_Q={\cdot }_Q$$
31		eqid	$$⊢1_Q=1_Q$$
32	29 30 31	isringid	$$⊢Q\in \mathrm{Ring}\to \left(\left(\mathbb{Z}\times \left\{1\right\}\in {\mathrm{Base}}_Q\wedge \forall x\in {\mathrm{Base}}_Q\left(\left(\mathbb{Z}\times \left\{1\right\}\right){\cdot }_{Q}x=x\wedge x{\cdot }_Q\left(\mathbb{Z}\times \left\{1\right\}\right)=x\right)\right)\leftrightarrow 1_Q=\mathbb{Z}\times \left\{1\right\}\right)$$
33	28 32	ax-mp	$$⊢\left(\mathbb{Z}\times \left\{1\right\}\in {\mathrm{Base}}_Q\wedge \forall x\in {\mathrm{Base}}_Q\left(\left(\mathbb{Z}\times \left\{1\right\}\right){\cdot }_{Q}x=x\wedge x{\cdot }_Q\left(\mathbb{Z}\times \left\{1\right\}\right)=x\right)\right)\leftrightarrow 1_Q=\mathbb{Z}\times \left\{1\right\}$$
34	27 33	mpbi	$$⊢1_Q=\mathbb{Z}\times \left\{1\right\}$$