Theorem pzriprnglem7

Description: Lemma 7 for pzriprng : J is a unital ring. (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	pzriprnglem7	$$⊢J\in \mathrm{Ring}$$

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	pzriprnglem5	Could not format I e. ( SubRng ` R ) : No typesetting found for |- I e. ( SubRng ` R ) with typecode |-
5	3	subrngrng	Could not format ( I e. ( SubRng ` R ) -> J e. Rng ) : No typesetting found for |- ( I e. ( SubRng ` R ) -> J e. Rng ) with typecode |-
6	4 5	ax-mp	$$⊢J\in \mathrm{Rng}$$
7		1z	$$⊢1\in \mathbb{Z}$$
8		c0ex	$$⊢0\in \mathrm{V}$$
9	8	snid	$$⊢0\in \left\{0\right\}$$
10	7 9	opelxpii	$$⊢⟨1,0⟩\in \left(\mathbb{Z}\times \left\{0\right\}\right)$$
11	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 |-
12	4 11	ax-mp	$$⊢I={\mathrm{Base}}_J$$
13	12 2	eqtr3i	$$⊢{\mathrm{Base}}_J=\mathbb{Z}\times \left\{0\right\}$$
14	10 13	eleqtrri	$$⊢⟨1,0⟩\in {\mathrm{Base}}_J$$
15		oveq1	$$⊢i=⟨1,0⟩\to i{\cdot }_{J}x=⟨1,0⟩{\cdot }_{J}x$$
16	15	eqeq1d	$$⊢i=⟨1,0⟩\to \left(i{\cdot }_{J}x=x\leftrightarrow ⟨1,0⟩{\cdot }_{J}x=x\right)$$
17	16	ovanraleqv	$$⊢i=⟨1,0⟩\to \left(\forall x\in {\mathrm{Base}}_J\left(i{\cdot }_{J}x=x\wedge x{\cdot }_{J}i=x\right)\leftrightarrow \forall x\in {\mathrm{Base}}_J\left(⟨1,0⟩{\cdot }_{J}x=x\wedge x{\cdot }_J⟨1,0⟩=x\right)\right)$$
18		id	$$⊢⟨1,0⟩\in {\mathrm{Base}}_J\to ⟨1,0⟩\in {\mathrm{Base}}_J$$
19	12	eleq2i	$$⊢x\in I\leftrightarrow x\in {\mathrm{Base}}_J$$
20	1 2 3	pzriprnglem6	$$⊢x\in I\to \left(⟨1,0⟩{\cdot }_{J}x=x\wedge x{\cdot }_J⟨1,0⟩=x\right)$$
21	19 20	sylbir	$$⊢x\in {\mathrm{Base}}_J\to \left(⟨1,0⟩{\cdot }_{J}x=x\wedge x{\cdot }_J⟨1,0⟩=x\right)$$
22	21	a1i	$$⊢⟨1,0⟩\in {\mathrm{Base}}_J\to \left(x\in {\mathrm{Base}}_J\to \left(⟨1,0⟩{\cdot }_{J}x=x\wedge x{\cdot }_J⟨1,0⟩=x\right)\right)$$
23	22	ralrimiv	$$⊢⟨1,0⟩\in {\mathrm{Base}}_J\to \forall x\in {\mathrm{Base}}_J\left(⟨1,0⟩{\cdot }_{J}x=x\wedge x{\cdot }_J⟨1,0⟩=x\right)$$
24	17 18 23	rspcedvdw	$$⊢⟨1,0⟩\in {\mathrm{Base}}_J\to \exists i\in {\mathrm{Base}}_J\forall x\in {\mathrm{Base}}_J\left(i{\cdot }_{J}x=x\wedge x{\cdot }_{J}i=x\right)$$
25	14 24	ax-mp	$$⊢\exists i\in {\mathrm{Base}}_J\forall x\in {\mathrm{Base}}_J\left(i{\cdot }_{J}x=x\wedge x{\cdot }_{J}i=x\right)$$
26		eqid	$$⊢{\mathrm{Base}}_J={\mathrm{Base}}_J$$
27		eqid	$$⊢{\cdot }_J={\cdot }_J$$
28	26 27	isringrng	$$⊢J\in \mathrm{Ring}\leftrightarrow \left(J\in \mathrm{Rng}\wedge \exists i\in {\mathrm{Base}}_J\forall x\in {\mathrm{Base}}_J\left(i{\cdot }_{J}x=x\wedge x{\cdot }_{J}i=x\right)\right)$$
29	6 25 28	mpbir2an	$$⊢J\in \mathrm{Ring}$$