pzriprnglem12

Description: Lemma 12 for pzriprng : Q has a ring unity. (Contributed by AV, 23-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	pzriprnglem12	$⊢ X \in {Base}_{Q} \to ((ℤ \times \{1\}) \cdot_{Q} X = X \land X \cdot_{Q} (ℤ \times \{1\}) = X)$

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	1 2 3 4 5 6	pzriprnglem11	$⊢ {Base}_{Q} = ⋃_{y \in ℤ} \{ℤ \times \{y\}\}$
8	7	eleq2i	$⊢ X \in {Base}_{Q} \leftrightarrow X \in ⋃_{y \in ℤ} \{ℤ \times \{y\}\}$
9		eliun	$⊢ X \in ⋃_{y \in ℤ} \{ℤ \times \{y\}\} \leftrightarrow \exists y \in ℤ X \in \{ℤ \times \{y\}\}$
10	8 9	bitri	$⊢ X \in {Base}_{Q} \leftrightarrow \exists y \in ℤ X \in \{ℤ \times \{y\}\}$
11		elsni	$⊢ X \in \{ℤ \times \{y\}\} \to X = ℤ \times \{y\}$
12		1z	$⊢ 1 \in ℤ$
13	1 2 3 4 5	pzriprnglem10	$⊢ (1 \in ℤ \land y \in ℤ) \to [⟨1, y⟩] \underset{˙}{\sim} = ℤ \times \{y\}$
14	12 13	mpan	$⊢ y \in ℤ \to [⟨1, y⟩] \underset{˙}{\sim} = ℤ \times \{y\}$
15	14	eqcomd	$⊢ y \in ℤ \to ℤ \times \{y\} = [⟨1, y⟩] \underset{˙}{\sim}$
16	15	eqeq2d	$⊢ y \in ℤ \to (X = ℤ \times \{y\} \leftrightarrow X = [⟨1, y⟩] \underset{˙}{\sim})$
17	1	pzriprnglem1	$⊢ R \in Rng$
18	17	a1i	$⊢ y \in ℤ \to R \in Rng$
19	1 2 3	pzriprnglem8	$⊢ I \in 2Ideal (R)$
20	19	a1i	$⊢ y \in ℤ \to I \in 2Ideal (R)$
21	1 2	pzriprnglem4	$⊢ I \in SubGrp (R)$
22	21	a1i	$⊢ y \in ℤ \to I \in SubGrp (R)$
23	12	a1i	$⊢ y \in ℤ \to 1 \in ℤ$
24	23 23	opelxpd	$⊢ y \in ℤ \to ⟨1, 1⟩ \in (ℤ \times ℤ)$
25		id	$⊢ y \in ℤ \to y \in ℤ$
26	23 25	opelxpd	$⊢ y \in ℤ \to ⟨1, y⟩ \in (ℤ \times ℤ)$
27	1	pzriprnglem2	$⊢ {Base}_{R} = ℤ \times ℤ$
28	27	eqcomi	$⊢ ℤ \times ℤ = {Base}_{R}$
29		eqid	$⊢ \cdot_{R} = \cdot_{R}$
30		eqid	$⊢ \cdot_{Q} = \cdot_{Q}$
31	5 6 28 29 30	qusmulrng	$⊢ ((R \in Rng \land I \in 2Ideal (R) \land I \in SubGrp (R)) \land (⟨1, 1⟩ \in (ℤ \times ℤ) \land ⟨1, y⟩ \in (ℤ \times ℤ))) \to [⟨1, 1⟩] \underset{˙}{\sim} \cdot_{Q} [⟨1, y⟩] \underset{˙}{\sim} = [(⟨1, 1⟩ \cdot_{R} ⟨1, y⟩)] \underset{˙}{\sim}$
32	18 20 22 24 26 31	syl32anc	$⊢ y \in ℤ \to [⟨1, 1⟩] \underset{˙}{\sim} \cdot_{Q} [⟨1, y⟩] \underset{˙}{\sim} = [(⟨1, 1⟩ \cdot_{R} ⟨1, y⟩)] \underset{˙}{\sim}$
33		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
34		zringring	$⊢ ℤ_{ring} \in Ring$
35	34	a1i	$⊢ y \in ℤ \to ℤ_{ring} \in Ring$
36	23 23	zmulcld	$⊢ y \in ℤ \to 1 \cdot 1 \in ℤ$
37	23 25	zmulcld	$⊢ y \in ℤ \to 1 y \in ℤ$
38		zringmulr	$⊢ \times = \cdot_{ℤ_{ring}}$
39	1 33 33 35 35 23 23 23 25 36 37 38 38 29	xpsmul	$⊢ y \in ℤ \to ⟨1, 1⟩ \cdot_{R} ⟨1, y⟩ = ⟨1 \cdot 1, 1 y⟩$
40		1cnd	$⊢ y \in ℤ \to 1 \in ℂ$
41	40	mulridd	$⊢ y \in ℤ \to 1 \cdot 1 = 1$
42		zcn	$⊢ y \in ℤ \to y \in ℂ$
43	42	mullidd	$⊢ y \in ℤ \to 1 y = y$
44	41 43	opeq12d	$⊢ y \in ℤ \to ⟨1 \cdot 1, 1 y⟩ = ⟨1, y⟩$
45	39 44	eqtrd	$⊢ y \in ℤ \to ⟨1, 1⟩ \cdot_{R} ⟨1, y⟩ = ⟨1, y⟩$
46	45	eceq1d	$⊢ y \in ℤ \to [(⟨1, 1⟩ \cdot_{R} ⟨1, y⟩)] \underset{˙}{\sim} = [⟨1, y⟩] \underset{˙}{\sim}$
47	32 46	eqtrd	$⊢ y \in ℤ \to [⟨1, 1⟩] \underset{˙}{\sim} \cdot_{Q} [⟨1, y⟩] \underset{˙}{\sim} = [⟨1, y⟩] \underset{˙}{\sim}$
48	5 6 28 29 30	qusmulrng	$⊢ ((R \in Rng \land I \in 2Ideal (R) \land I \in SubGrp (R)) \land (⟨1, y⟩ \in (ℤ \times ℤ) \land ⟨1, 1⟩ \in (ℤ \times ℤ))) \to [⟨1, y⟩] \underset{˙}{\sim} \cdot_{Q} [⟨1, 1⟩] \underset{˙}{\sim} = [(⟨1, y⟩ \cdot_{R} ⟨1, 1⟩)] \underset{˙}{\sim}$
49	18 20 22 26 24 48	syl32anc	$⊢ y \in ℤ \to [⟨1, y⟩] \underset{˙}{\sim} \cdot_{Q} [⟨1, 1⟩] \underset{˙}{\sim} = [(⟨1, y⟩ \cdot_{R} ⟨1, 1⟩)] \underset{˙}{\sim}$
50	25 23	zmulcld	$⊢ y \in ℤ \to y \cdot 1 \in ℤ$
51	1 33 33 35 35 23 25 23 23 36 50 38 38 29	xpsmul	$⊢ y \in ℤ \to ⟨1, y⟩ \cdot_{R} ⟨1, 1⟩ = ⟨1 \cdot 1, y \cdot 1⟩$
52	42	mulridd	$⊢ y \in ℤ \to y \cdot 1 = y$
53	41 52	opeq12d	$⊢ y \in ℤ \to ⟨1 \cdot 1, y \cdot 1⟩ = ⟨1, y⟩$
54	51 53	eqtrd	$⊢ y \in ℤ \to ⟨1, y⟩ \cdot_{R} ⟨1, 1⟩ = ⟨1, y⟩$
55	54	eceq1d	$⊢ y \in ℤ \to [(⟨1, y⟩ \cdot_{R} ⟨1, 1⟩)] \underset{˙}{\sim} = [⟨1, y⟩] \underset{˙}{\sim}$
56	49 55	eqtrd	$⊢ y \in ℤ \to [⟨1, y⟩] \underset{˙}{\sim} \cdot_{Q} [⟨1, 1⟩] \underset{˙}{\sim} = [⟨1, y⟩] \underset{˙}{\sim}$
57	47 56	jca	$⊢ y \in ℤ \to ([⟨1, 1⟩] \underset{˙}{\sim} \cdot_{Q} [⟨1, y⟩] \underset{˙}{\sim} = [⟨1, y⟩] \underset{˙}{\sim} \land [⟨1, y⟩] \underset{˙}{\sim} \cdot_{Q} [⟨1, 1⟩] \underset{˙}{\sim} = [⟨1, y⟩] \underset{˙}{\sim})$
58	1 2 3 4 5	pzriprnglem10	$⊢ (1 \in ℤ \land 1 \in ℤ) \to [⟨1, 1⟩] \underset{˙}{\sim} = ℤ \times \{1\}$
59	12 12 58	mp2an	$⊢ [⟨1, 1⟩] \underset{˙}{\sim} = ℤ \times \{1\}$
60	59	eqcomi	$⊢ ℤ \times \{1\} = [⟨1, 1⟩] \underset{˙}{\sim}$
61	60	a1i	$⊢ X = [⟨1, y⟩] \underset{˙}{\sim} \to ℤ \times \{1\} = [⟨1, 1⟩] \underset{˙}{\sim}$
62		id	$⊢ X = [⟨1, y⟩] \underset{˙}{\sim} \to X = [⟨1, y⟩] \underset{˙}{\sim}$
63	61 62	oveq12d	$⊢ X = [⟨1, y⟩] \underset{˙}{\sim} \to (ℤ \times \{1\}) \cdot_{Q} X = [⟨1, 1⟩] \underset{˙}{\sim} \cdot_{Q} [⟨1, y⟩] \underset{˙}{\sim}$
64	63 62	eqeq12d	$⊢ X = [⟨1, y⟩] \underset{˙}{\sim} \to ((ℤ \times \{1\}) \cdot_{Q} X = X \leftrightarrow [⟨1, 1⟩] \underset{˙}{\sim} \cdot_{Q} [⟨1, y⟩] \underset{˙}{\sim} = [⟨1, y⟩] \underset{˙}{\sim})$
65	62 61	oveq12d	$⊢ X = [⟨1, y⟩] \underset{˙}{\sim} \to X \cdot_{Q} (ℤ \times \{1\}) = [⟨1, y⟩] \underset{˙}{\sim} \cdot_{Q} [⟨1, 1⟩] \underset{˙}{\sim}$
66	65 62	eqeq12d	$⊢ X = [⟨1, y⟩] \underset{˙}{\sim} \to (X \cdot_{Q} (ℤ \times \{1\}) = X \leftrightarrow [⟨1, y⟩] \underset{˙}{\sim} \cdot_{Q} [⟨1, 1⟩] \underset{˙}{\sim} = [⟨1, y⟩] \underset{˙}{\sim})$
67	64 66	anbi12d	$⊢ X = [⟨1, y⟩] \underset{˙}{\sim} \to (((ℤ \times \{1\}) \cdot_{Q} X = X \land X \cdot_{Q} (ℤ \times \{1\}) = X) \leftrightarrow ([⟨1, 1⟩] \underset{˙}{\sim} \cdot_{Q} [⟨1, y⟩] \underset{˙}{\sim} = [⟨1, y⟩] \underset{˙}{\sim} \land [⟨1, y⟩] \underset{˙}{\sim} \cdot_{Q} [⟨1, 1⟩] \underset{˙}{\sim} = [⟨1, y⟩] \underset{˙}{\sim}))$
68	57 67	syl5ibrcom	$⊢ y \in ℤ \to (X = [⟨1, y⟩] \underset{˙}{\sim} \to ((ℤ \times \{1\}) \cdot_{Q} X = X \land X \cdot_{Q} (ℤ \times \{1\}) = X))$
69	16 68	sylbid	$⊢ y \in ℤ \to (X = ℤ \times \{y\} \to ((ℤ \times \{1\}) \cdot_{Q} X = X \land X \cdot_{Q} (ℤ \times \{1\}) = X))$
70	11 69	syl5	$⊢ y \in ℤ \to (X \in \{ℤ \times \{y\}\} \to ((ℤ \times \{1\}) \cdot_{Q} X = X \land X \cdot_{Q} (ℤ \times \{1\}) = X))$
71	70	rexlimiv	$⊢ \exists y \in ℤ X \in \{ℤ \times \{y\}\} \to ((ℤ \times \{1\}) \cdot_{Q} X = X \land X \cdot_{Q} (ℤ \times \{1\}) = X)$
72	10 71	sylbi	$⊢ X \in {Base}_{Q} \to ((ℤ \times \{1\}) \cdot_{Q} X = X \land X \cdot_{Q} (ℤ \times \{1\}) = X)$

Metamath Proof Explorer

Theorem pzriprnglem12

Proof