Theorem pzriprnglem6

Description: Lemma 6 for pzriprng : J has a ring unity. (Contributed by AV, 19-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$$
Assertion	pzriprnglem6	$$⊢X\in I\to \left(⟨1,0⟩{\cdot }_{J}X=X\wedge X{\cdot }_J⟨1,0⟩=X\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	1 2	pzriprnglem3	$$⊢X\in I\leftrightarrow \exists a\in \mathbb{Z}X=⟨a,0⟩$$
5	1 2	pzriprnglem5	Could not format I e. ( SubRng ` R ) : No typesetting found for |- I e. ( SubRng ` R ) with typecode |-
6		eqid	$$⊢{\cdot }_R={\cdot }_R$$
7	3 6	ressmulr	Could not format ( I e. ( SubRng ` R ) -> ( .r ` R ) = ( .r ` J ) ) : No typesetting found for |- ( I e. ( SubRng ` R ) -> ( .r ` R ) = ( .r ` J ) ) with typecode |-
8	7	eqcomd	Could not format ( I e. ( SubRng ` R ) -> ( .r ` J ) = ( .r ` R ) ) : No typesetting found for |- ( I e. ( SubRng ` R ) -> ( .r ` J ) = ( .r ` R ) ) with typecode |-
9	5 8	ax-mp	$$⊢{\cdot }_J={\cdot }_R$$
10	9	oveqi	$$⊢⟨1,0⟩{\cdot }_J⟨a,0⟩=⟨1,0⟩{\cdot }_R⟨a,0⟩$$
11	10	a1i	$$⊢a\in \mathbb{Z}\to ⟨1,0⟩{\cdot }_J⟨a,0⟩=⟨1,0⟩{\cdot }_R⟨a,0⟩$$
12		zringbas	$$⊢\mathbb{Z}={\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
13		zringring	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}$$
14	13	a1i	$$⊢a\in \mathbb{Z}\to {\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}$$
15		1zzd	$$⊢a\in \mathbb{Z}\to 1\in \mathbb{Z}$$
16		0z	$$⊢0\in \mathbb{Z}$$
17	16	a1i	$$⊢a\in \mathbb{Z}\to 0\in \mathbb{Z}$$
18		id	$$⊢a\in \mathbb{Z}\to a\in \mathbb{Z}$$
19		zringmulr	$$⊢\times ={\cdot }_{{\mathbb{Z}}_{\mathrm{ring}}}$$
20	19	oveqi	$$⊢1a=1{\cdot }_{{\mathbb{Z}}_{\mathrm{ring}}}a$$
21	15 18	zmulcld	$$⊢a\in \mathbb{Z}\to 1a\in \mathbb{Z}$$
22	20 21	eqeltrrid	$$⊢a\in \mathbb{Z}\to 1{\cdot }_{{\mathbb{Z}}_{\mathrm{ring}}}a\in \mathbb{Z}$$
23	19	eqcomi	$$⊢{\cdot }_{{\mathbb{Z}}_{\mathrm{ring}}}=\times$$
24	23	oveqi	$$⊢0{\cdot }_{{\mathbb{Z}}_{\mathrm{ring}}}0=0\cdot 0$$
25		id	$$⊢0\in \mathbb{Z}\to 0\in \mathbb{Z}$$
26	25 25	zmulcld	$$⊢0\in \mathbb{Z}\to 0\cdot 0\in \mathbb{Z}$$
27	16 26	ax-mp	$$⊢0\cdot 0\in \mathbb{Z}$$
28	24 27	eqeltri	$$⊢0{\cdot }_{{\mathbb{Z}}_{\mathrm{ring}}}0\in \mathbb{Z}$$
29	28	a1i	$$⊢a\in \mathbb{Z}\to 0{\cdot }_{{\mathbb{Z}}_{\mathrm{ring}}}0\in \mathbb{Z}$$
30		eqid	$$⊢{\cdot }_{{\mathbb{Z}}_{\mathrm{ring}}}={\cdot }_{{\mathbb{Z}}_{\mathrm{ring}}}$$
31	1 12 12 14 14 15 17 18 17 22 29 30 30 6	xpsmul	$$⊢a\in \mathbb{Z}\to ⟨1,0⟩{\cdot }_R⟨a,0⟩=⟨1{\cdot }_{{\mathbb{Z}}_{\mathrm{ring}}}a,0{\cdot }_{{\mathbb{Z}}_{\mathrm{ring}}}0⟩$$
32		zcn	$$⊢a\in \mathbb{Z}\to a\in ℂ$$
33	32	mullidd	$$⊢a\in \mathbb{Z}\to 1a=a$$
34	20 33	eqtr3id	$$⊢a\in \mathbb{Z}\to 1{\cdot }_{{\mathbb{Z}}_{\mathrm{ring}}}a=a$$
35		0cn	$$⊢0\in ℂ$$
36	35	mul02i	$$⊢0\cdot 0=0$$
37	24 36	eqtri	$$⊢0{\cdot }_{{\mathbb{Z}}_{\mathrm{ring}}}0=0$$
38	37	a1i	$$⊢a\in \mathbb{Z}\to 0{\cdot }_{{\mathbb{Z}}_{\mathrm{ring}}}0=0$$
39	34 38	opeq12d	$$⊢a\in \mathbb{Z}\to ⟨1{\cdot }_{{\mathbb{Z}}_{\mathrm{ring}}}a,0{\cdot }_{{\mathbb{Z}}_{\mathrm{ring}}}0⟩=⟨a,0⟩$$
40	11 31 39	3eqtrd	$$⊢a\in \mathbb{Z}\to ⟨1,0⟩{\cdot }_J⟨a,0⟩=⟨a,0⟩$$
41	9	oveqi	$$⊢⟨a,0⟩{\cdot }_J⟨1,0⟩=⟨a,0⟩{\cdot }_R⟨1,0⟩$$
42	41	a1i	$$⊢a\in \mathbb{Z}\to ⟨a,0⟩{\cdot }_J⟨1,0⟩=⟨a,0⟩{\cdot }_R⟨1,0⟩$$
43	19	oveqi	$$⊢a\cdot 1=a{\cdot }_{{\mathbb{Z}}_{\mathrm{ring}}}1$$
44	18 15	zmulcld	$$⊢a\in \mathbb{Z}\to a\cdot 1\in \mathbb{Z}$$
45	43 44	eqeltrrid	$$⊢a\in \mathbb{Z}\to a{\cdot }_{{\mathbb{Z}}_{\mathrm{ring}}}1\in \mathbb{Z}$$
46	1 12 12 14 14 18 17 15 17 45 29 30 30 6	xpsmul	$$⊢a\in \mathbb{Z}\to ⟨a,0⟩{\cdot }_R⟨1,0⟩=⟨a{\cdot }_{{\mathbb{Z}}_{\mathrm{ring}}}1,0{\cdot }_{{\mathbb{Z}}_{\mathrm{ring}}}0⟩$$
47	23	oveqi	$$⊢a{\cdot }_{{\mathbb{Z}}_{\mathrm{ring}}}1=a\cdot 1$$
48	32	mulridd	$$⊢a\in \mathbb{Z}\to a\cdot 1=a$$
49	47 48	eqtrid	$$⊢a\in \mathbb{Z}\to a{\cdot }_{{\mathbb{Z}}_{\mathrm{ring}}}1=a$$
50	49 38	opeq12d	$$⊢a\in \mathbb{Z}\to ⟨a{\cdot }_{{\mathbb{Z}}_{\mathrm{ring}}}1,0{\cdot }_{{\mathbb{Z}}_{\mathrm{ring}}}0⟩=⟨a,0⟩$$
51	42 46 50	3eqtrd	$$⊢a\in \mathbb{Z}\to ⟨a,0⟩{\cdot }_J⟨1,0⟩=⟨a,0⟩$$
52	40 51	jca	$$⊢a\in \mathbb{Z}\to \left(⟨1,0⟩{\cdot }_J⟨a,0⟩=⟨a,0⟩\wedge ⟨a,0⟩{\cdot }_J⟨1,0⟩=⟨a,0⟩\right)$$
53		oveq2	$$⊢X=⟨a,0⟩\to ⟨1,0⟩{\cdot }_{J}X=⟨1,0⟩{\cdot }_J⟨a,0⟩$$
54		id	$$⊢X=⟨a,0⟩\to X=⟨a,0⟩$$
55	53 54	eqeq12d	$$⊢X=⟨a,0⟩\to \left(⟨1,0⟩{\cdot }_{J}X=X\leftrightarrow ⟨1,0⟩{\cdot }_J⟨a,0⟩=⟨a,0⟩\right)$$
56		oveq1	$$⊢X=⟨a,0⟩\to X{\cdot }_J⟨1,0⟩=⟨a,0⟩{\cdot }_J⟨1,0⟩$$
57	56 54	eqeq12d	$$⊢X=⟨a,0⟩\to \left(X{\cdot }_J⟨1,0⟩=X\leftrightarrow ⟨a,0⟩{\cdot }_J⟨1,0⟩=⟨a,0⟩\right)$$
58	55 57	anbi12d	$$⊢X=⟨a,0⟩\to \left(\left(⟨1,0⟩{\cdot }_{J}X=X\wedge X{\cdot }_J⟨1,0⟩=X\right)\leftrightarrow \left(⟨1,0⟩{\cdot }_J⟨a,0⟩=⟨a,0⟩\wedge ⟨a,0⟩{\cdot }_J⟨1,0⟩=⟨a,0⟩\right)\right)$$
59	52 58	syl5ibrcom	$$⊢a\in \mathbb{Z}\to \left(X=⟨a,0⟩\to \left(⟨1,0⟩{\cdot }_{J}X=X\wedge X{\cdot }_J⟨1,0⟩=X\right)\right)$$
60	59	rexlimiv	$$⊢\exists a\in \mathbb{Z}X=⟨a,0⟩\to \left(⟨1,0⟩{\cdot }_{J}X=X\wedge X{\cdot }_J⟨1,0⟩=X\right)$$
61	4 60	sylbi	$$⊢X\in I\to \left(⟨1,0⟩{\cdot }_{J}X=X\wedge X{\cdot }_J⟨1,0⟩=X\right)$$