Theorem pzriprnglem13

Description: Lemma 13 for pzriprng : Q is a unital ring. (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	pzriprnglem13	$$⊢Q\in \mathrm{Ring}$$

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	1	pzriprnglem1	$$⊢R\in \mathrm{Rng}$$
8	1 2 3	pzriprnglem8	$$⊢I\in \mathrm{2Ideal}\left(R\right)$$
9	1 2	pzriprnglem4	$$⊢I\in \mathrm{SubGrp}\left(R\right)$$
10	5	oveq2i	$$⊢R{/}_{𝑠}\underset{\dot{}}{\sim }=R{/}_{𝑠}\left(R{~}_{\mathit{QG}}I\right)$$
11	6 10	eqtri	$$⊢Q=R{/}_{𝑠}\left(R{~}_{\mathit{QG}}I\right)$$
12		eqid	$$⊢\mathrm{2Ideal}\left(R\right)=\mathrm{2Ideal}\left(R\right)$$
13	11 12	qus2idrng	$$⊢\left(R\in \mathrm{Rng}\wedge I\in \mathrm{2Ideal}\left(R\right)\wedge I\in \mathrm{SubGrp}\left(R\right)\right)\to Q\in \mathrm{Rng}$$
14	7 8 9 13	mp3an	$$⊢Q\in \mathrm{Rng}$$
15		1z	$$⊢1\in \mathbb{Z}$$
16		zex	$$⊢\mathbb{Z}\in \mathrm{V}$$
17		snex	$$⊢\left\{1\right\}\in \mathrm{V}$$
18	16 17	xpex	$$⊢\mathbb{Z}\times \left\{1\right\}\in \mathrm{V}$$
19	18	snid	$$⊢\mathbb{Z}\times \left\{1\right\}\in \left\{\mathbb{Z}\times \left\{1\right\}\right\}$$
20		sneq	$$⊢y=1\to \left\{y\right\}=\left\{1\right\}$$
21	20	xpeq2d	$$⊢y=1\to \mathbb{Z}\times \left\{y\right\}=\mathbb{Z}\times \left\{1\right\}$$
22	21	sneqd	$$⊢y=1\to \left\{\mathbb{Z}\times \left\{y\right\}\right\}=\left\{\mathbb{Z}\times \left\{1\right\}\right\}$$
23	22	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)$$
24	23	rspcev	$$⊢\left(1\in \mathbb{Z}\wedge \mathbb{Z}\times \left\{1\right\}\in \left\{\mathbb{Z}\times \left\{1\right\}\right\}\right)\to \exists y\in \mathbb{Z}\mathbb{Z}\times \left\{1\right\}\in \left\{\mathbb{Z}\times \left\{y\right\}\right\}$$
25	15 19 24	mp2an	$$⊢\exists y\in \mathbb{Z}\mathbb{Z}\times \left\{1\right\}\in \left\{\mathbb{Z}\times \left\{y\right\}\right\}$$
26		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\}$$
27	25 26	mpbir	$$⊢\mathbb{Z}\times \left\{1\right\}\in \bigcup _{y\in \mathbb{Z}}\left\{\mathbb{Z}\times \left\{y\right\}\right\}$$
28	1 2 3 4 5 6	pzriprnglem11	$$⊢{\mathrm{Base}}_Q=\bigcup _{y\in \mathbb{Z}}\left\{\mathbb{Z}\times \left\{y\right\}\right\}$$
29	27 28	eleqtrri	$$⊢\mathbb{Z}\times \left\{1\right\}\in {\mathrm{Base}}_Q$$
30		oveq1	$$⊢i=\mathbb{Z}\times \left\{1\right\}\to i{\cdot }_{Q}x=\left(\mathbb{Z}\times \left\{1\right\}\right){\cdot }_{Q}x$$
31	30	eqeq1d	$$⊢i=\mathbb{Z}\times \left\{1\right\}\to \left(i{\cdot }_{Q}x=x\leftrightarrow \left(\mathbb{Z}\times \left\{1\right\}\right){\cdot }_{Q}x=x\right)$$
32	31	ovanraleqv	$$⊢i=\mathbb{Z}\times \left\{1\right\}\to \left(\forall x\in {\mathrm{Base}}_Q\left(i{\cdot }_{Q}x=x\wedge x{\cdot }_{Q}i=x\right)\leftrightarrow \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)$$
33		id	$$⊢\mathbb{Z}\times \left\{1\right\}\in {\mathrm{Base}}_Q\to \mathbb{Z}\times \left\{1\right\}\in {\mathrm{Base}}_Q$$
34	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)$$
35	34	a1i	$$⊢\mathbb{Z}\times \left\{1\right\}\in {\mathrm{Base}}_Q\to \left(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)\right)$$
36	35	ralrimiv	$$⊢\mathbb{Z}\times \left\{1\right\}\in {\mathrm{Base}}_Q\to \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)$$
37	32 33 36	rspcedvdw	$$⊢\mathbb{Z}\times \left\{1\right\}\in {\mathrm{Base}}_Q\to \exists i\in {\mathrm{Base}}_Q\forall x\in {\mathrm{Base}}_Q\left(i{\cdot }_{Q}x=x\wedge x{\cdot }_{Q}i=x\right)$$
38	29 37	ax-mp	$$⊢\exists i\in {\mathrm{Base}}_Q\forall x\in {\mathrm{Base}}_Q\left(i{\cdot }_{Q}x=x\wedge x{\cdot }_{Q}i=x\right)$$
39		eqid	$$⊢{\mathrm{Base}}_Q={\mathrm{Base}}_Q$$
40		eqid	$$⊢{\cdot }_Q={\cdot }_Q$$
41	39 40	isringrng	$$⊢Q\in \mathrm{Ring}\leftrightarrow \left(Q\in \mathrm{Rng}\wedge \exists i\in {\mathrm{Base}}_Q\forall x\in {\mathrm{Base}}_Q\left(i{\cdot }_{Q}x=x\wedge x{\cdot }_{Q}i=x\right)\right)$$
42	14 38 41	mpbir2an	$$⊢Q\in \mathrm{Ring}$$