pzriprnglem10

Description: Lemma 10 for pzriprng : The equivalence classes of R modulo 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$
Assertion	pzriprnglem10	$⊢ (X \in ℤ \land Y \in ℤ) \to [⟨X, Y⟩] \underset{˙}{\sim} = ℤ \times \{Y\}$

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	1	pzriprnglem1	$⊢ R \in Rng$
7		rnggrp	$⊢ R \in Rng \to R \in Grp$
8	6 7	ax-mp	$⊢ R \in Grp$
9		0z	$⊢ 0 \in ℤ$
10		snssi	$⊢ 0 \in ℤ \to \{0\} \subseteq ℤ$
11		xpss2	$⊢ \{0\} \subseteq ℤ \to ℤ \times \{0\} \subseteq ℤ \times ℤ$
12	9 10 11	mp2b	$⊢ ℤ \times \{0\} \subseteq ℤ \times ℤ$
13	2 12	eqsstri	$⊢ I \subseteq ℤ \times ℤ$
14	13	a1i	$⊢ (X \in ℤ \land Y \in ℤ) \to I \subseteq ℤ \times ℤ$
15		opelxpi	$⊢ (X \in ℤ \land Y \in ℤ) \to ⟨X, Y⟩ \in (ℤ \times ℤ)$
16	1	pzriprnglem2	$⊢ {Base}_{R} = ℤ \times ℤ$
17	16	eqcomi	$⊢ ℤ \times ℤ = {Base}_{R}$
18		eqid	$⊢ +_{R} = +_{R}$
19	17 5 18	eqglact	$⊢ (R \in Grp \land I \subseteq ℤ \times ℤ \land ⟨X, Y⟩ \in (ℤ \times ℤ)) \to [⟨X, Y⟩] \underset{˙}{\sim} = (x \in (ℤ \times ℤ) ⟼ ⟨X, Y⟩ +_{R} x) [I]$
20	8 14 15 19	mp3an2i	$⊢ (X \in ℤ \land Y \in ℤ) \to [⟨X, Y⟩] \underset{˙}{\sim} = (x \in (ℤ \times ℤ) ⟼ ⟨X, Y⟩ +_{R} x) [I]$
21	14	mptimass	$⊢ (X \in ℤ \land Y \in ℤ) \to (x \in (ℤ \times ℤ) ⟼ ⟨X, Y⟩ +_{R} x) [I] = ran (x \in I ⟼ ⟨X, Y⟩ +_{R} x)$
22		eqid	$⊢ (x \in I ⟼ ⟨X, Y⟩ +_{R} x) = (x \in I ⟼ ⟨X, Y⟩ +_{R} x)$
23	22	rnmpt	$⊢ ran (x \in I ⟼ ⟨X, Y⟩ +_{R} x) = \{e \| \exists x \in I e = ⟨X, Y⟩ +_{R} x\}$
24	23	a1i	$⊢ (X \in ℤ \land Y \in ℤ) \to ran (x \in I ⟼ ⟨X, Y⟩ +_{R} x) = \{e \| \exists x \in I e = ⟨X, Y⟩ +_{R} x\}$
25	2	rexeqi	$⊢ \exists x \in I e = ⟨X, Y⟩ +_{R} x \leftrightarrow \exists x \in (ℤ \times \{0\}) e = ⟨X, Y⟩ +_{R} x$
26		oveq2	$⊢ x = ⟨a, b⟩ \to ⟨X, Y⟩ +_{R} x = ⟨X, Y⟩ +_{R} ⟨a, b⟩$
27	26	eqeq2d	$⊢ x = ⟨a, b⟩ \to (e = ⟨X, Y⟩ +_{R} x \leftrightarrow e = ⟨X, Y⟩ +_{R} ⟨a, b⟩)$
28	27	rexxp	$⊢ \exists x \in (ℤ \times \{0\}) e = ⟨X, Y⟩ +_{R} x \leftrightarrow \exists a \in ℤ \exists b \in \{0\} e = ⟨X, Y⟩ +_{R} ⟨a, b⟩$
29	25 28	bitri	$⊢ \exists x \in I e = ⟨X, Y⟩ +_{R} x \leftrightarrow \exists a \in ℤ \exists b \in \{0\} e = ⟨X, Y⟩ +_{R} ⟨a, b⟩$
30	29	a1i	$⊢ (X \in ℤ \land Y \in ℤ) \to (\exists x \in I e = ⟨X, Y⟩ +_{R} x \leftrightarrow \exists a \in ℤ \exists b \in \{0\} e = ⟨X, Y⟩ +_{R} ⟨a, b⟩)$
31	30	abbidv	$⊢ (X \in ℤ \land Y \in ℤ) \to \{e \| \exists x \in I e = ⟨X, Y⟩ +_{R} x\} = \{e \| \exists a \in ℤ \exists b \in \{0\} e = ⟨X, Y⟩ +_{R} ⟨a, b⟩\}$
32		c0ex	$⊢ 0 \in V$
33		opeq2	$⊢ b = 0 \to ⟨a, b⟩ = ⟨a, 0⟩$
34	33	oveq2d	$⊢ b = 0 \to ⟨X, Y⟩ +_{R} ⟨a, b⟩ = ⟨X, Y⟩ +_{R} ⟨a, 0⟩$
35	34	eqeq2d	$⊢ b = 0 \to (e = ⟨X, Y⟩ +_{R} ⟨a, b⟩ \leftrightarrow e = ⟨X, Y⟩ +_{R} ⟨a, 0⟩)$
36	32 35	rexsn	$⊢ \exists b \in \{0\} e = ⟨X, Y⟩ +_{R} ⟨a, b⟩ \leftrightarrow e = ⟨X, Y⟩ +_{R} ⟨a, 0⟩$
37		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
38		zringring	$⊢ ℤ_{ring} \in Ring$
39	38	a1i	$⊢ ((X \in ℤ \land Y \in ℤ) \land a \in ℤ) \to ℤ_{ring} \in Ring$
40		simpll	$⊢ ((X \in ℤ \land Y \in ℤ) \land a \in ℤ) \to X \in ℤ$
41		simplr	$⊢ ((X \in ℤ \land Y \in ℤ) \land a \in ℤ) \to Y \in ℤ$
42		simpr	$⊢ ((X \in ℤ \land Y \in ℤ) \land a \in ℤ) \to a \in ℤ$
43		0zd	$⊢ ((X \in ℤ \land Y \in ℤ) \land a \in ℤ) \to 0 \in ℤ$
44	40 42	zaddcld	$⊢ ((X \in ℤ \land Y \in ℤ) \land a \in ℤ) \to X + a \in ℤ$
45		simpr	$⊢ (X \in ℤ \land Y \in ℤ) \to Y \in ℤ$
46		0zd	$⊢ (X \in ℤ \land Y \in ℤ) \to 0 \in ℤ$
47	45 46	zaddcld	$⊢ (X \in ℤ \land Y \in ℤ) \to Y + 0 \in ℤ$
48	47	adantr	$⊢ ((X \in ℤ \land Y \in ℤ) \land a \in ℤ) \to Y + 0 \in ℤ$
49		zringplusg	$⊢ + = +_{ℤ_{ring}}$
50	1 37 37 39 39 40 41 42 43 44 48 49 49 18	xpsadd	$⊢ ((X \in ℤ \land Y \in ℤ) \land a \in ℤ) \to ⟨X, Y⟩ +_{R} ⟨a, 0⟩ = ⟨X + a, Y + 0⟩$
51	50	eqeq2d	$⊢ ((X \in ℤ \land Y \in ℤ) \land a \in ℤ) \to (e = ⟨X, Y⟩ +_{R} ⟨a, 0⟩ \leftrightarrow e = ⟨X + a, Y + 0⟩)$
52	36 51	bitrid	$⊢ ((X \in ℤ \land Y \in ℤ) \land a \in ℤ) \to (\exists b \in \{0\} e = ⟨X, Y⟩ +_{R} ⟨a, b⟩ \leftrightarrow e = ⟨X + a, Y + 0⟩)$
53	52	rexbidva	$⊢ (X \in ℤ \land Y \in ℤ) \to (\exists a \in ℤ \exists b \in \{0\} e = ⟨X, Y⟩ +_{R} ⟨a, b⟩ \leftrightarrow \exists a \in ℤ e = ⟨X + a, Y + 0⟩)$
54	53	abbidv	$⊢ (X \in ℤ \land Y \in ℤ) \to \{e \| \exists a \in ℤ \exists b \in \{0\} e = ⟨X, Y⟩ +_{R} ⟨a, b⟩\} = \{e \| \exists a \in ℤ e = ⟨X + a, Y + 0⟩\}$
55		iunab	$⊢ ⋃_{a \in ℤ} \{e \| e = ⟨X + a, Y + 0⟩\} = \{e \| \exists a \in ℤ e = ⟨X + a, Y + 0⟩\}$
56	55	eqcomi	$⊢ \{e \| \exists a \in ℤ e = ⟨X + a, Y + 0⟩\} = ⋃_{a \in ℤ} \{e \| e = ⟨X + a, Y + 0⟩\}$
57	56	a1i	$⊢ (X \in ℤ \land Y \in ℤ) \to \{e \| \exists a \in ℤ e = ⟨X + a, Y + 0⟩\} = ⋃_{a \in ℤ} \{e \| e = ⟨X + a, Y + 0⟩\}$
58		zcn	$⊢ Y \in ℤ \to Y \in ℂ$
59	58	adantl	$⊢ (X \in ℤ \land Y \in ℤ) \to Y \in ℂ$
60	59	addridd	$⊢ (X \in ℤ \land Y \in ℤ) \to Y + 0 = Y$
61	60	opeq2d	$⊢ (X \in ℤ \land Y \in ℤ) \to ⟨X + a, Y + 0⟩ = ⟨X + a, Y⟩$
62	61	eqeq2d	$⊢ (X \in ℤ \land Y \in ℤ) \to (e = ⟨X + a, Y + 0⟩ \leftrightarrow e = ⟨X + a, Y⟩)$
63	62	abbidv	$⊢ (X \in ℤ \land Y \in ℤ) \to \{e \| e = ⟨X + a, Y + 0⟩\} = \{e \| e = ⟨X + a, Y⟩\}$
64	63	iuneq2d	$⊢ (X \in ℤ \land Y \in ℤ) \to ⋃_{a \in ℤ} \{e \| e = ⟨X + a, Y + 0⟩\} = ⋃_{a \in ℤ} \{e \| e = ⟨X + a, Y⟩\}$
65		df-sn	$⊢ \{⟨X + a, Y⟩\} = \{e \| e = ⟨X + a, Y⟩\}$
66	65	eqcomi	$⊢ \{e \| e = ⟨X + a, Y⟩\} = \{⟨X + a, Y⟩\}$
67	66	a1i	$⊢ a \in ℤ \to \{e \| e = ⟨X + a, Y⟩\} = \{⟨X + a, Y⟩\}$
68	67	iuneq2i	$⊢ ⋃_{a \in ℤ} \{e \| e = ⟨X + a, Y⟩\} = ⋃_{a \in ℤ} \{⟨X + a, Y⟩\}$
69	68	a1i	$⊢ (X \in ℤ \land Y \in ℤ) \to ⋃_{a \in ℤ} \{e \| e = ⟨X + a, Y⟩\} = ⋃_{a \in ℤ} \{⟨X + a, Y⟩\}$
70		velsn	$⊢ y \in \{⟨X + a, Y⟩\} \leftrightarrow y = ⟨X + a, Y⟩$
71	70	rexbii	$⊢ \exists a \in ℤ y \in \{⟨X + a, Y⟩\} \leftrightarrow \exists a \in ℤ y = ⟨X + a, Y⟩$
72	44	adantr	$⊢ (((X \in ℤ \land Y \in ℤ) \land a \in ℤ) \land y = ⟨X + a, Y⟩) \to X + a \in ℤ$
73		simplr	$⊢ ((((X \in ℤ \land Y \in ℤ) \land a \in ℤ) \land y = ⟨X + a, Y⟩) \land b = X + a) \to y = ⟨X + a, Y⟩$
74		opeq1	$⊢ b = X + a \to ⟨b, Y⟩ = ⟨X + a, Y⟩$
75	74	adantl	$⊢ ((((X \in ℤ \land Y \in ℤ) \land a \in ℤ) \land y = ⟨X + a, Y⟩) \land b = X + a) \to ⟨b, Y⟩ = ⟨X + a, Y⟩$
76	73 75	eqeq12d	$⊢ ((((X \in ℤ \land Y \in ℤ) \land a \in ℤ) \land y = ⟨X + a, Y⟩) \land b = X + a) \to (y = ⟨b, Y⟩ \leftrightarrow ⟨X + a, Y⟩ = ⟨X + a, Y⟩)$
77		eqidd	$⊢ (((X \in ℤ \land Y \in ℤ) \land a \in ℤ) \land y = ⟨X + a, Y⟩) \to ⟨X + a, Y⟩ = ⟨X + a, Y⟩$
78	72 76 77	rspcedvd	$⊢ (((X \in ℤ \land Y \in ℤ) \land a \in ℤ) \land y = ⟨X + a, Y⟩) \to \exists b \in ℤ y = ⟨b, Y⟩$
79	78	ex	$⊢ ((X \in ℤ \land Y \in ℤ) \land a \in ℤ) \to (y = ⟨X + a, Y⟩ \to \exists b \in ℤ y = ⟨b, Y⟩)$
80	79	rexlimdva	$⊢ (X \in ℤ \land Y \in ℤ) \to (\exists a \in ℤ y = ⟨X + a, Y⟩ \to \exists b \in ℤ y = ⟨b, Y⟩)$
81		simpr	$⊢ ((X \in ℤ \land Y \in ℤ) \land b \in ℤ) \to b \in ℤ$
82		simpll	$⊢ ((X \in ℤ \land Y \in ℤ) \land b \in ℤ) \to X \in ℤ$
83	81 82	zsubcld	$⊢ ((X \in ℤ \land Y \in ℤ) \land b \in ℤ) \to b - X \in ℤ$
84	83	adantr	$⊢ (((X \in ℤ \land Y \in ℤ) \land b \in ℤ) \land y = ⟨b, Y⟩) \to b - X \in ℤ$
85		simplr	$⊢ ((((X \in ℤ \land Y \in ℤ) \land b \in ℤ) \land y = ⟨b, Y⟩) \land a = b - X) \to y = ⟨b, Y⟩$
86		oveq2	$⊢ a = b - X \to X + a = X + b - X$
87	86	adantl	$⊢ ((((X \in ℤ \land Y \in ℤ) \land b \in ℤ) \land y = ⟨b, Y⟩) \land a = b - X) \to X + a = X + b - X$
88	87	opeq1d	$⊢ ((((X \in ℤ \land Y \in ℤ) \land b \in ℤ) \land y = ⟨b, Y⟩) \land a = b - X) \to ⟨X + a, Y⟩ = ⟨X + b - X, Y⟩$
89	85 88	eqeq12d	$⊢ ((((X \in ℤ \land Y \in ℤ) \land b \in ℤ) \land y = ⟨b, Y⟩) \land a = b - X) \to (y = ⟨X + a, Y⟩ \leftrightarrow ⟨b, Y⟩ = ⟨X + b - X, Y⟩)$
90		zcn	$⊢ X \in ℤ \to X \in ℂ$
91	90	adantr	$⊢ (X \in ℤ \land Y \in ℤ) \to X \in ℂ$
92	91	adantr	$⊢ ((X \in ℤ \land Y \in ℤ) \land b \in ℤ) \to X \in ℂ$
93		zcn	$⊢ b \in ℤ \to b \in ℂ$
94	93	adantl	$⊢ ((X \in ℤ \land Y \in ℤ) \land b \in ℤ) \to b \in ℂ$
95	92 94	pncan3d	$⊢ ((X \in ℤ \land Y \in ℤ) \land b \in ℤ) \to X + b - X = b$
96	95	eqcomd	$⊢ ((X \in ℤ \land Y \in ℤ) \land b \in ℤ) \to b = X + b - X$
97	96	adantr	$⊢ (((X \in ℤ \land Y \in ℤ) \land b \in ℤ) \land y = ⟨b, Y⟩) \to b = X + b - X$
98	97	opeq1d	$⊢ (((X \in ℤ \land Y \in ℤ) \land b \in ℤ) \land y = ⟨b, Y⟩) \to ⟨b, Y⟩ = ⟨X + b - X, Y⟩$
99	84 89 98	rspcedvd	$⊢ (((X \in ℤ \land Y \in ℤ) \land b \in ℤ) \land y = ⟨b, Y⟩) \to \exists a \in ℤ y = ⟨X + a, Y⟩$
100	99	ex	$⊢ ((X \in ℤ \land Y \in ℤ) \land b \in ℤ) \to (y = ⟨b, Y⟩ \to \exists a \in ℤ y = ⟨X + a, Y⟩)$
101	100	rexlimdva	$⊢ (X \in ℤ \land Y \in ℤ) \to (\exists b \in ℤ y = ⟨b, Y⟩ \to \exists a \in ℤ y = ⟨X + a, Y⟩)$
102	80 101	impbid	$⊢ (X \in ℤ \land Y \in ℤ) \to (\exists a \in ℤ y = ⟨X + a, Y⟩ \leftrightarrow \exists b \in ℤ y = ⟨b, Y⟩)$
103	71 102	bitrid	$⊢ (X \in ℤ \land Y \in ℤ) \to (\exists a \in ℤ y \in \{⟨X + a, Y⟩\} \leftrightarrow \exists b \in ℤ y = ⟨b, Y⟩)$
104		opeq2	$⊢ c = Y \to ⟨b, c⟩ = ⟨b, Y⟩$
105	104	eqeq2d	$⊢ c = Y \to (y = ⟨b, c⟩ \leftrightarrow y = ⟨b, Y⟩)$
106	105	rexsng	$⊢ Y \in ℤ \to (\exists c \in \{Y\} y = ⟨b, c⟩ \leftrightarrow y = ⟨b, Y⟩)$
107	106	adantl	$⊢ (X \in ℤ \land Y \in ℤ) \to (\exists c \in \{Y\} y = ⟨b, c⟩ \leftrightarrow y = ⟨b, Y⟩)$
108	107	bicomd	$⊢ (X \in ℤ \land Y \in ℤ) \to (y = ⟨b, Y⟩ \leftrightarrow \exists c \in \{Y\} y = ⟨b, c⟩)$
109	108	rexbidv	$⊢ (X \in ℤ \land Y \in ℤ) \to (\exists b \in ℤ y = ⟨b, Y⟩ \leftrightarrow \exists b \in ℤ \exists c \in \{Y\} y = ⟨b, c⟩)$
110	103 109	bitrd	$⊢ (X \in ℤ \land Y \in ℤ) \to (\exists a \in ℤ y \in \{⟨X + a, Y⟩\} \leftrightarrow \exists b \in ℤ \exists c \in \{Y\} y = ⟨b, c⟩)$
111		eliun	$⊢ y \in ⋃_{a \in ℤ} \{⟨X + a, Y⟩\} \leftrightarrow \exists a \in ℤ y \in \{⟨X + a, Y⟩\}$
112		elxp2	$⊢ y \in (ℤ \times \{Y\}) \leftrightarrow \exists b \in ℤ \exists c \in \{Y\} y = ⟨b, c⟩$
113	110 111 112	3bitr4g	$⊢ (X \in ℤ \land Y \in ℤ) \to (y \in ⋃_{a \in ℤ} \{⟨X + a, Y⟩\} \leftrightarrow y \in (ℤ \times \{Y\}))$
114	113	eqrdv	$⊢ (X \in ℤ \land Y \in ℤ) \to ⋃_{a \in ℤ} \{⟨X + a, Y⟩\} = ℤ \times \{Y\}$
115	64 69 114	3eqtrd	$⊢ (X \in ℤ \land Y \in ℤ) \to ⋃_{a \in ℤ} \{e \| e = ⟨X + a, Y + 0⟩\} = ℤ \times \{Y\}$
116	54 57 115	3eqtrd	$⊢ (X \in ℤ \land Y \in ℤ) \to \{e \| \exists a \in ℤ \exists b \in \{0\} e = ⟨X, Y⟩ +_{R} ⟨a, b⟩\} = ℤ \times \{Y\}$
117	24 31 116	3eqtrd	$⊢ (X \in ℤ \land Y \in ℤ) \to ran (x \in I ⟼ ⟨X, Y⟩ +_{R} x) = ℤ \times \{Y\}$
118	20 21 117	3eqtrd	$⊢ (X \in ℤ \land Y \in ℤ) \to [⟨X, Y⟩] \underset{˙}{\sim} = ℤ \times \{Y\}$

Metamath Proof Explorer

Theorem pzriprnglem10

Proof