Theorem pzriprnglem9

Description: Lemma 9 for pzriprng : The ring unity of the ring 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$$
Assertion	pzriprnglem9	$$⊢\underset{\dot{}}{1}=⟨1,0⟩$$

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		1z	$$⊢1\in \mathbb{Z}$$
6		c0ex	$$⊢0\in \mathrm{V}$$
7	6	snid	$$⊢0\in \left\{0\right\}$$
8	2	eleq2i	$$⊢⟨1,0⟩\in I\leftrightarrow ⟨1,0⟩\in \left(\mathbb{Z}\times \left\{0\right\}\right)$$
9		opelxp	$$⊢⟨1,0⟩\in \left(\mathbb{Z}\times \left\{0\right\}\right)\leftrightarrow \left(1\in \mathbb{Z}\wedge 0\in \left\{0\right\}\right)$$
10	8 9	bitri	$$⊢⟨1,0⟩\in I\leftrightarrow \left(1\in \mathbb{Z}\wedge 0\in \left\{0\right\}\right)$$
11	5 7 10	mpbir2an	$$⊢⟨1,0⟩\in I$$
12	1 2 3	pzriprnglem6	$$⊢x\in I\to \left(⟨1,0⟩{\cdot }_{J}x=x\wedge x{\cdot }_J⟨1,0⟩=x\right)$$
13	12	rgen	$$⊢\forall x\in I\left(⟨1,0⟩{\cdot }_{J}x=x\wedge x{\cdot }_J⟨1,0⟩=x\right)$$
14	11 13	pm3.2i	$$⊢\left(⟨1,0⟩\in I\wedge \forall x\in I\left(⟨1,0⟩{\cdot }_{J}x=x\wedge x{\cdot }_J⟨1,0⟩=x\right)\right)$$
15	1 2 3	pzriprnglem7	$$⊢J\in \mathrm{Ring}$$
16	1 2	pzriprnglem5	Could not format I e. ( SubRng ` R ) : No typesetting found for |- I e. ( SubRng ` R ) with typecode |-
17	3	subrngbas	Could not format ( I e. ( SubRng ` R ) -> I = ( Base ` J ) ) : No typesetting found for |- ( I e. ( SubRng ` R ) -> I = ( Base ` J ) ) with typecode |-
18	16 17	ax-mp	$$⊢I={\mathrm{Base}}_J$$
19		eqid	$$⊢{\cdot }_J={\cdot }_J$$
20	18 19 4	isringid	$$⊢J\in \mathrm{Ring}\to \left(\left(⟨1,0⟩\in I\wedge \forall x\in I\left(⟨1,0⟩{\cdot }_{J}x=x\wedge x{\cdot }_J⟨1,0⟩=x\right)\right)\leftrightarrow \underset{\dot{}}{1}=⟨1,0⟩\right)$$
21	15 20	ax-mp	$$⊢\left(⟨1,0⟩\in I\wedge \forall x\in I\left(⟨1,0⟩{\cdot }_{J}x=x\wedge x{\cdot }_J⟨1,0⟩=x\right)\right)\leftrightarrow \underset{\dot{}}{1}=⟨1,0⟩$$
22	14 21	mpbi	$$⊢\underset{\dot{}}{1}=⟨1,0⟩$$