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 = ℤ_{ring} \times_{𝑠} ℤ_{ring}$
	pzriprng.i	$⊢ I = ℤ \times \{0\}$
	pzriprng.j	$⊢ J = R ↾_{𝑠} I$
	pzriprng.1	$⊢ \underset{˙}{1} = 1_{J}$
	pzriprng.g	$⊢ \underset{˙}{\sim} = R ~_{QG} I$
	pzriprng.q	$⊢ Q = R /_{𝑠} \underset{˙}{\sim}$
Assertion	pzriprnglem11	$⊢ {Base}_{Q} = ⋃_{r \in ℤ} \{ℤ \times \{r\}\}$

Proof

Step	Hyp	Ref	Expression
1		pzriprng.r	$⊢ R = ℤ_{ring} \times_{𝑠} ℤ_{ring}$
2		pzriprng.i	$⊢ I = ℤ \times \{0\}$
3		pzriprng.j	$⊢ J = R ↾_{𝑠} I$
4		pzriprng.1	$⊢ \underset{˙}{1} = 1_{J}$
5		pzriprng.g	$⊢ \underset{˙}{\sim} = R ~_{QG} I$
6		pzriprng.q	$⊢ Q = R /_{𝑠} \underset{˙}{\sim}$
7		df-qs	$⊢ (ℤ \times ℤ) / \underset{˙}{\sim} = \{e \| \exists p \in (ℤ \times ℤ) e = [p] \underset{˙}{\sim}\}$
8	6	a1i	$⊢ \underset{˙}{\sim} = R ~_{QG} I \to Q = R /_{𝑠} \underset{˙}{\sim}$
9	1	pzriprnglem2	$⊢ {Base}_{R} = ℤ \times ℤ$
10	9	eqcomi	$⊢ ℤ \times ℤ = {Base}_{R}$
11	10	a1i	$⊢ \underset{˙}{\sim} = R ~_{QG} I \to ℤ \times ℤ = {Base}_{R}$
12		ovexd	$⊢ \underset{˙}{\sim} = R ~_{QG} I \to R ~_{QG} I \in V$
13	5 12	eqeltrid	$⊢ \underset{˙}{\sim} = R ~_{QG} I \to \underset{˙}{\sim} \in V$
14	1	pzriprnglem1	$⊢ R \in Rng$
15	14	a1i	$⊢ \underset{˙}{\sim} = R ~_{QG} I \to R \in Rng$
16	8 11 13 15	qusbas	$⊢ \underset{˙}{\sim} = R ~_{QG} I \to (ℤ \times ℤ) / \underset{˙}{\sim} = {Base}_{Q}$
17	5 16	ax-mp	$⊢ (ℤ \times ℤ) / \underset{˙}{\sim} = {Base}_{Q}$
18		nfcv	$⊢ \underline{Ⅎ} s \{e \| e = [p] \underset{˙}{\sim}\}$
19		nfcv	$⊢ \underline{Ⅎ} r \{e \| e = [p] \underset{˙}{\sim}\}$
20		nfcv	$⊢ \underline{Ⅎ} p \{e \| e = [⟨s, r⟩] \underset{˙}{\sim}\}$
21		eceq1	$⊢ p = ⟨s, r⟩ \to [p] \underset{˙}{\sim} = [⟨s, r⟩] \underset{˙}{\sim}$
22	21	eqeq2d	$⊢ p = ⟨s, r⟩ \to (e = [p] \underset{˙}{\sim} \leftrightarrow e = [⟨s, r⟩] \underset{˙}{\sim})$
23	22	abbidv	$⊢ p = ⟨s, r⟩ \to \{e \| e = [p] \underset{˙}{\sim}\} = \{e \| e = [⟨s, r⟩] \underset{˙}{\sim}\}$
24	18 19 20 23	iunxpf	$⊢ ⋃_{p \in ℤ \times ℤ} \{e \| e = [p] \underset{˙}{\sim}\} = ⋃_{s \in ℤ} ⋃_{r \in ℤ} \{e \| e = [⟨s, r⟩] \underset{˙}{\sim}\}$
25		iunab	$⊢ ⋃_{p \in ℤ \times ℤ} \{e \| e = [p] \underset{˙}{\sim}\} = \{e \| \exists p \in (ℤ \times ℤ) e = [p] \underset{˙}{\sim}\}$
26		iuncom	$⊢ ⋃_{s \in ℤ} ⋃_{r \in ℤ} \{e \| e = [⟨s, r⟩] \underset{˙}{\sim}\} = ⋃_{r \in ℤ} ⋃_{s \in ℤ} \{e \| e = [⟨s, r⟩] \underset{˙}{\sim}\}$
27		df-sn	$⊢ \{[⟨s, r⟩] \underset{˙}{\sim}\} = \{e \| e = [⟨s, r⟩] \underset{˙}{\sim}\}$
28	27	eqcomi	$⊢ \{e \| e = [⟨s, r⟩] \underset{˙}{\sim}\} = \{[⟨s, r⟩] \underset{˙}{\sim}\}$
29	28	a1i	$⊢ s \in ℤ \to \{e \| e = [⟨s, r⟩] \underset{˙}{\sim}\} = \{[⟨s, r⟩] \underset{˙}{\sim}\}$
30	29	iuneq2i	$⊢ ⋃_{s \in ℤ} \{e \| e = [⟨s, r⟩] \underset{˙}{\sim}\} = ⋃_{s \in ℤ} \{[⟨s, r⟩] \underset{˙}{\sim}\}$
31		simpr	$⊢ ((r \in ℤ \land s \in ℤ) \land p = [⟨s, r⟩] \underset{˙}{\sim}) \to p = [⟨s, r⟩] \underset{˙}{\sim}$
32	1 2 3 4 5	pzriprnglem10	$⊢ (s \in ℤ \land r \in ℤ) \to [⟨s, r⟩] \underset{˙}{\sim} = ℤ \times \{r\}$
33	32	ancoms	$⊢ (r \in ℤ \land s \in ℤ) \to [⟨s, r⟩] \underset{˙}{\sim} = ℤ \times \{r\}$
34	33	adantr	$⊢ ((r \in ℤ \land s \in ℤ) \land p = [⟨s, r⟩] \underset{˙}{\sim}) \to [⟨s, r⟩] \underset{˙}{\sim} = ℤ \times \{r\}$
35	31 34	eqtrd	$⊢ ((r \in ℤ \land s \in ℤ) \land p = [⟨s, r⟩] \underset{˙}{\sim}) \to p = ℤ \times \{r\}$
36	35	ex	$⊢ (r \in ℤ \land s \in ℤ) \to (p = [⟨s, r⟩] \underset{˙}{\sim} \to p = ℤ \times \{r\})$
37	36	rexlimdva	$⊢ r \in ℤ \to (\exists s \in ℤ p = [⟨s, r⟩] \underset{˙}{\sim} \to p = ℤ \times \{r\})$
38		0zd	$⊢ (r \in ℤ \land p = ℤ \times \{r\}) \to 0 \in ℤ$
39		simpr	$⊢ (r \in ℤ \land p = ℤ \times \{r\}) \to p = ℤ \times \{r\}$
40		opeq1	$⊢ s = 0 \to ⟨s, r⟩ = ⟨0, r⟩$
41	40	eceq1d	$⊢ s = 0 \to [⟨s, r⟩] \underset{˙}{\sim} = [⟨0, r⟩] \underset{˙}{\sim}$
42	39 41	eqeqan12d	$⊢ ((r \in ℤ \land p = ℤ \times \{r\}) \land s = 0) \to (p = [⟨s, r⟩] \underset{˙}{\sim} \leftrightarrow ℤ \times \{r\} = [⟨0, r⟩] \underset{˙}{\sim})$
43		0zd	$⊢ r \in ℤ \to 0 \in ℤ$
44	1 2 3 4 5	pzriprnglem10	$⊢ (0 \in ℤ \land r \in ℤ) \to [⟨0, r⟩] \underset{˙}{\sim} = ℤ \times \{r\}$
45	43 44	mpancom	$⊢ r \in ℤ \to [⟨0, r⟩] \underset{˙}{\sim} = ℤ \times \{r\}$
46	45	eqcomd	$⊢ r \in ℤ \to ℤ \times \{r\} = [⟨0, r⟩] \underset{˙}{\sim}$
47	46	adantr	$⊢ (r \in ℤ \land p = ℤ \times \{r\}) \to ℤ \times \{r\} = [⟨0, r⟩] \underset{˙}{\sim}$
48	38 42 47	rspcedvd	$⊢ (r \in ℤ \land p = ℤ \times \{r\}) \to \exists s \in ℤ p = [⟨s, r⟩] \underset{˙}{\sim}$
49	48	ex	$⊢ r \in ℤ \to (p = ℤ \times \{r\} \to \exists s \in ℤ p = [⟨s, r⟩] \underset{˙}{\sim})$
50	37 49	impbid	$⊢ r \in ℤ \to (\exists s \in ℤ p = [⟨s, r⟩] \underset{˙}{\sim} \leftrightarrow p = ℤ \times \{r\})$
51	50	abbidv	$⊢ r \in ℤ \to \{p \| \exists s \in ℤ p = [⟨s, r⟩] \underset{˙}{\sim}\} = \{p \| p = ℤ \times \{r\}\}$
52		iunsn	$⊢ ⋃_{s \in ℤ} \{[⟨s, r⟩] \underset{˙}{\sim}\} = \{p \| \exists s \in ℤ p = [⟨s, r⟩] \underset{˙}{\sim}\}$
53		df-sn	$⊢ \{ℤ \times \{r\}\} = \{p \| p = ℤ \times \{r\}\}$
54	51 52 53	3eqtr4g	$⊢ r \in ℤ \to ⋃_{s \in ℤ} \{[⟨s, r⟩] \underset{˙}{\sim}\} = \{ℤ \times \{r\}\}$
55	30 54	eqtrid	$⊢ r \in ℤ \to ⋃_{s \in ℤ} \{e \| e = [⟨s, r⟩] \underset{˙}{\sim}\} = \{ℤ \times \{r\}\}$
56	55	iuneq2i	$⊢ ⋃_{r \in ℤ} ⋃_{s \in ℤ} \{e \| e = [⟨s, r⟩] \underset{˙}{\sim}\} = ⋃_{r \in ℤ} \{ℤ \times \{r\}\}$
57	26 56	eqtri	$⊢ ⋃_{s \in ℤ} ⋃_{r \in ℤ} \{e \| e = [⟨s, r⟩] \underset{˙}{\sim}\} = ⋃_{r \in ℤ} \{ℤ \times \{r\}\}$
58	24 25 57	3eqtr3i	$⊢ \{e \| \exists p \in (ℤ \times ℤ) e = [p] \underset{˙}{\sim}\} = ⋃_{r \in ℤ} \{ℤ \times \{r\}\}$
59	7 17 58	3eqtr3i	$⊢ {Base}_{Q} = ⋃_{r \in ℤ} \{ℤ \times \{r\}\}$

Metamath Proof Explorer

Theorem pzriprnglem11

Proof