Theorem pzriprnglem11

Description: Lemma 11 for pzriprng : The base set of the quotient of R and J . (Contributed by AV, 22-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	pzriprnglem11	$$⊢{\mathrm{Base}}_Q=\bigcup _{r\in \mathbb{Z}}\left\{\mathbb{Z}\times \left\{r\right\}\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		df-qs	$$⊢\left(\mathbb{Z}\times \mathbb{Z}\right)/\underset{\dot{}}{\sim }=\left\{e|\exists p\in \left(\mathbb{Z}\times \mathbb{Z}\right)e=\left[p\right]\underset{\dot{}}{\sim }\right\}$$
8	6	a1i	$$⊢\underset{\dot{}}{\sim }=R{~}_{\mathit{QG}}I\to Q=R{/}_{𝑠}\underset{\dot{}}{\sim }$$
9	1	pzriprnglem2	$$⊢{\mathrm{Base}}_R=\mathbb{Z}\times \mathbb{Z}$$
10	9	eqcomi	$$⊢\mathbb{Z}\times \mathbb{Z}={\mathrm{Base}}_R$$
11	10	a1i	$$⊢\underset{\dot{}}{\sim }=R{~}_{\mathit{QG}}I\to \mathbb{Z}\times \mathbb{Z}={\mathrm{Base}}_R$$
12		ovexd	$$⊢\underset{\dot{}}{\sim }=R{~}_{\mathit{QG}}I\to R{~}_{\mathit{QG}}I\in \mathrm{V}$$
13	5 12	eqeltrid	$$⊢\underset{\dot{}}{\sim }=R{~}_{\mathit{QG}}I\to \underset{\dot{}}{\sim }\in \mathrm{V}$$
14	1	pzriprnglem1	$$⊢R\in \mathrm{Rng}$$
15	14	a1i	$$⊢\underset{\dot{}}{\sim }=R{~}_{\mathit{QG}}I\to R\in \mathrm{Rng}$$
16	8 11 13 15	qusbas	$$⊢\underset{\dot{}}{\sim }=R{~}_{\mathit{QG}}I\to \left(\mathbb{Z}\times \mathbb{Z}\right)/\underset{\dot{}}{\sim }={\mathrm{Base}}_Q$$
17	5 16	ax-mp	$$⊢\left(\mathbb{Z}\times \mathbb{Z}\right)/\underset{\dot{}}{\sim }={\mathrm{Base}}_Q$$
18		nfcv	$$⊢\underset{\_}{Ⅎ}s\left\{e|e=\left[p\right]\underset{\dot{}}{\sim }\right\}$$
19		nfcv	$$⊢\underset{\_}{Ⅎ}r\left\{e|e=\left[p\right]\underset{\dot{}}{\sim }\right\}$$
20		nfcv	$$⊢\underset{\_}{Ⅎ}p\left\{e|e=\left[⟨s,r⟩\right]\underset{\dot{}}{\sim }\right\}$$
21		eceq1	$$⊢p=⟨s,r⟩\to \left[p\right]\underset{\dot{}}{\sim }=\left[⟨s,r⟩\right]\underset{\dot{}}{\sim }$$
22	21	eqeq2d	$$⊢p=⟨s,r⟩\to \left(e=\left[p\right]\underset{\dot{}}{\sim }\leftrightarrow e=\left[⟨s,r⟩\right]\underset{\dot{}}{\sim }\right)$$
23	22	abbidv	$$⊢p=⟨s,r⟩\to \left\{e|e=\left[p\right]\underset{\dot{}}{\sim }\right\}=\left\{e|e=\left[⟨s,r⟩\right]\underset{\dot{}}{\sim }\right\}$$
24	18 19 20 23	iunxpf	$$⊢\bigcup _{p\in \mathbb{Z}\times \mathbb{Z}}\left\{e|e=\left[p\right]\underset{\dot{}}{\sim }\right\}=\bigcup _{s\in \mathbb{Z}}\bigcup _{r\in \mathbb{Z}}\left\{e|e=\left[⟨s,r⟩\right]\underset{\dot{}}{\sim }\right\}$$
25		iunab	$$⊢\bigcup _{p\in \mathbb{Z}\times \mathbb{Z}}\left\{e|e=\left[p\right]\underset{\dot{}}{\sim }\right\}=\left\{e|\exists p\in \left(\mathbb{Z}\times \mathbb{Z}\right)e=\left[p\right]\underset{\dot{}}{\sim }\right\}$$
26		iuncom	$$⊢\bigcup _{s\in \mathbb{Z}}\bigcup _{r\in \mathbb{Z}}\left\{e|e=\left[⟨s,r⟩\right]\underset{\dot{}}{\sim }\right\}=\bigcup _{r\in \mathbb{Z}}\bigcup _{s\in \mathbb{Z}}\left\{e|e=\left[⟨s,r⟩\right]\underset{\dot{}}{\sim }\right\}$$
27		df-sn	$$⊢\left\{\left[⟨s,r⟩\right]\underset{\dot{}}{\sim }\right\}=\left\{e|e=\left[⟨s,r⟩\right]\underset{\dot{}}{\sim }\right\}$$
28	27	eqcomi	$$⊢\left\{e|e=\left[⟨s,r⟩\right]\underset{\dot{}}{\sim }\right\}=\left\{\left[⟨s,r⟩\right]\underset{\dot{}}{\sim }\right\}$$
29	28	a1i	$$⊢s\in \mathbb{Z}\to \left\{e|e=\left[⟨s,r⟩\right]\underset{\dot{}}{\sim }\right\}=\left\{\left[⟨s,r⟩\right]\underset{\dot{}}{\sim }\right\}$$
30	29	iuneq2i	$$⊢\bigcup _{s\in \mathbb{Z}}\left\{e|e=\left[⟨s,r⟩\right]\underset{\dot{}}{\sim }\right\}=\bigcup _{s\in \mathbb{Z}}\left\{\left[⟨s,r⟩\right]\underset{\dot{}}{\sim }\right\}$$
31		simpr	$$⊢\left(\left(r\in \mathbb{Z}\wedge s\in \mathbb{Z}\right)\wedge p=\left[⟨s,r⟩\right]\underset{\dot{}}{\sim }\right)\to p=\left[⟨s,r⟩\right]\underset{\dot{}}{\sim }$$
32	1 2 3 4 5	pzriprnglem10	$$⊢\left(s\in \mathbb{Z}\wedge r\in \mathbb{Z}\right)\to \left[⟨s,r⟩\right]\underset{\dot{}}{\sim }=\mathbb{Z}\times \left\{r\right\}$$
33	32	ancoms	$$⊢\left(r\in \mathbb{Z}\wedge s\in \mathbb{Z}\right)\to \left[⟨s,r⟩\right]\underset{\dot{}}{\sim }=\mathbb{Z}\times \left\{r\right\}$$
34	33	adantr	$$⊢\left(\left(r\in \mathbb{Z}\wedge s\in \mathbb{Z}\right)\wedge p=\left[⟨s,r⟩\right]\underset{\dot{}}{\sim }\right)\to \left[⟨s,r⟩\right]\underset{\dot{}}{\sim }=\mathbb{Z}\times \left\{r\right\}$$
35	31 34	eqtrd	$$⊢\left(\left(r\in \mathbb{Z}\wedge s\in \mathbb{Z}\right)\wedge p=\left[⟨s,r⟩\right]\underset{\dot{}}{\sim }\right)\to p=\mathbb{Z}\times \left\{r\right\}$$
36	35	ex	$$⊢\left(r\in \mathbb{Z}\wedge s\in \mathbb{Z}\right)\to \left(p=\left[⟨s,r⟩\right]\underset{\dot{}}{\sim }\to p=\mathbb{Z}\times \left\{r\right\}\right)$$
37	36	rexlimdva	$$⊢r\in \mathbb{Z}\to \left(\exists s\in \mathbb{Z}p=\left[⟨s,r⟩\right]\underset{\dot{}}{\sim }\to p=\mathbb{Z}\times \left\{r\right\}\right)$$
38		0zd	$$⊢\left(r\in \mathbb{Z}\wedge p=\mathbb{Z}\times \left\{r\right\}\right)\to 0\in \mathbb{Z}$$
39		simpr	$$⊢\left(r\in \mathbb{Z}\wedge p=\mathbb{Z}\times \left\{r\right\}\right)\to p=\mathbb{Z}\times \left\{r\right\}$$
40		opeq1	$$⊢s=0\to ⟨s,r⟩=⟨0,r⟩$$
41	40	eceq1d	$$⊢s=0\to \left[⟨s,r⟩\right]\underset{\dot{}}{\sim }=\left[⟨0,r⟩\right]\underset{\dot{}}{\sim }$$
42	39 41	eqeqan12d	$$⊢\left(\left(r\in \mathbb{Z}\wedge p=\mathbb{Z}\times \left\{r\right\}\right)\wedge s=0\right)\to \left(p=\left[⟨s,r⟩\right]\underset{\dot{}}{\sim }\leftrightarrow \mathbb{Z}\times \left\{r\right\}=\left[⟨0,r⟩\right]\underset{\dot{}}{\sim }\right)$$
43		0zd	$$⊢r\in \mathbb{Z}\to 0\in \mathbb{Z}$$
44	1 2 3 4 5	pzriprnglem10	$$⊢\left(0\in \mathbb{Z}\wedge r\in \mathbb{Z}\right)\to \left[⟨0,r⟩\right]\underset{\dot{}}{\sim }=\mathbb{Z}\times \left\{r\right\}$$
45	43 44	mpancom	$$⊢r\in \mathbb{Z}\to \left[⟨0,r⟩\right]\underset{\dot{}}{\sim }=\mathbb{Z}\times \left\{r\right\}$$
46	45	eqcomd	$$⊢r\in \mathbb{Z}\to \mathbb{Z}\times \left\{r\right\}=\left[⟨0,r⟩\right]\underset{\dot{}}{\sim }$$
47	46	adantr	$$⊢\left(r\in \mathbb{Z}\wedge p=\mathbb{Z}\times \left\{r\right\}\right)\to \mathbb{Z}\times \left\{r\right\}=\left[⟨0,r⟩\right]\underset{\dot{}}{\sim }$$
48	38 42 47	rspcedvd	$$⊢\left(r\in \mathbb{Z}\wedge p=\mathbb{Z}\times \left\{r\right\}\right)\to \exists s\in \mathbb{Z}p=\left[⟨s,r⟩\right]\underset{\dot{}}{\sim }$$
49	48	ex	$$⊢r\in \mathbb{Z}\to \left(p=\mathbb{Z}\times \left\{r\right\}\to \exists s\in \mathbb{Z}p=\left[⟨s,r⟩\right]\underset{\dot{}}{\sim }\right)$$
50	37 49	impbid	$$⊢r\in \mathbb{Z}\to \left(\exists s\in \mathbb{Z}p=\left[⟨s,r⟩\right]\underset{\dot{}}{\sim }\leftrightarrow p=\mathbb{Z}\times \left\{r\right\}\right)$$
51	50	abbidv	$$⊢r\in \mathbb{Z}\to \left\{p|\exists s\in \mathbb{Z}p=\left[⟨s,r⟩\right]\underset{\dot{}}{\sim }\right\}=\left\{p|p=\mathbb{Z}\times \left\{r\right\}\right\}$$
52		iunsn	$$⊢\bigcup _{s\in \mathbb{Z}}\left\{\left[⟨s,r⟩\right]\underset{\dot{}}{\sim }\right\}=\left\{p|\exists s\in \mathbb{Z}p=\left[⟨s,r⟩\right]\underset{\dot{}}{\sim }\right\}$$
53		df-sn	$$⊢\left\{\mathbb{Z}\times \left\{r\right\}\right\}=\left\{p|p=\mathbb{Z}\times \left\{r\right\}\right\}$$
54	51 52 53	3eqtr4g	$$⊢r\in \mathbb{Z}\to \bigcup _{s\in \mathbb{Z}}\left\{\left[⟨s,r⟩\right]\underset{\dot{}}{\sim }\right\}=\left\{\mathbb{Z}\times \left\{r\right\}\right\}$$
55	30 54	eqtrid	$$⊢r\in \mathbb{Z}\to \bigcup _{s\in \mathbb{Z}}\left\{e|e=\left[⟨s,r⟩\right]\underset{\dot{}}{\sim }\right\}=\left\{\mathbb{Z}\times \left\{r\right\}\right\}$$
56	55	iuneq2i	$$⊢\bigcup _{r\in \mathbb{Z}}\bigcup _{s\in \mathbb{Z}}\left\{e|e=\left[⟨s,r⟩\right]\underset{\dot{}}{\sim }\right\}=\bigcup _{r\in \mathbb{Z}}\left\{\mathbb{Z}\times \left\{r\right\}\right\}$$
57	26 56	eqtri	$$⊢\bigcup _{s\in \mathbb{Z}}\bigcup _{r\in \mathbb{Z}}\left\{e|e=\left[⟨s,r⟩\right]\underset{\dot{}}{\sim }\right\}=\bigcup _{r\in \mathbb{Z}}\left\{\mathbb{Z}\times \left\{r\right\}\right\}$$
58	24 25 57	3eqtr3i	$$⊢\left\{e|\exists p\in \left(\mathbb{Z}\times \mathbb{Z}\right)e=\left[p\right]\underset{\dot{}}{\sim }\right\}=\bigcup _{r\in \mathbb{Z}}\left\{\mathbb{Z}\times \left\{r\right\}\right\}$$
59	7 17 58	3eqtr3i	$$⊢{\mathrm{Base}}_Q=\bigcup _{r\in \mathbb{Z}}\left\{\mathbb{Z}\times \left\{r\right\}\right\}$$