Theorem pzriprnglem7

Description: Lemma 7 for pzriprng : J is a unital ring. (Contributed by AV, 19-Mar-2025)

	Ref	Expression
Hypotheses	pzriprng.r	⊢ 𝑅 = ( ℤring ×s ℤring )
	pzriprng.i	⊢ 𝐼 = ( ℤ × { 0 } )
	pzriprng.j	⊢ 𝐽 = ( 𝑅 ↾s 𝐼 )
Assertion	pzriprnglem7	⊢ 𝐽 ∈ Ring

Proof

Step	Hyp	Ref	Expression
1		pzriprng.r	⊢ 𝑅 = ( ℤring ×s ℤring )
2		pzriprng.i	⊢ 𝐼 = ( ℤ × { 0 } )
3		pzriprng.j	⊢ 𝐽 = ( 𝑅 ↾s 𝐼 )
4	1 2	pzriprnglem5	⊢ 𝐼 ∈ ( SubRng ‘ 𝑅 )
5	3	subrngrng	⊢ ( 𝐼 ∈ ( SubRng ‘ 𝑅 ) → 𝐽 ∈ Rng )
6	4 5	ax-mp	⊢ 𝐽 ∈ Rng
7		1z	⊢ 1 ∈ ℤ
8		c0ex	⊢ 0 ∈ V
9	8	snid	⊢ 0 ∈ { 0 }
10	7 9	opelxpii	⊢ ⟨ 1 , 0 ⟩ ∈ ( ℤ × { 0 } )
11	3	subrngbas	⊢ ( 𝐼 ∈ ( SubRng ‘ 𝑅 ) → 𝐼 = ( Base ‘ 𝐽 ) )
12	4 11	ax-mp	⊢ 𝐼 = ( Base ‘ 𝐽 )
13	12 2	eqtr3i	⊢ ( Base ‘ 𝐽 ) = ( ℤ × { 0 } )
14	10 13	eleqtrri	⊢ ⟨ 1 , 0 ⟩ ∈ ( Base ‘ 𝐽 )
15		oveq1	⊢ ( 𝑖 = ⟨ 1 , 0 ⟩ → ( 𝑖 ( .r ‘ 𝐽 ) 𝑥 ) = ( ⟨ 1 , 0 ⟩ ( .r ‘ 𝐽 ) 𝑥 ) )
16	15	eqeq1d	⊢ ( 𝑖 = ⟨ 1 , 0 ⟩ → ( ( 𝑖 ( .r ‘ 𝐽 ) 𝑥 ) = 𝑥 ↔ ( ⟨ 1 , 0 ⟩ ( .r ‘ 𝐽 ) 𝑥 ) = 𝑥 ) )
17	16	ovanraleqv	⊢ ( 𝑖 = ⟨ 1 , 0 ⟩ → ( ∀ 𝑥 ∈ ( Base ‘ 𝐽 ) ( ( 𝑖 ( .r ‘ 𝐽 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝐽 ) 𝑖 ) = 𝑥 ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐽 ) ( ( ⟨ 1 , 0 ⟩ ( .r ‘ 𝐽 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝐽 ) ⟨ 1 , 0 ⟩ ) = 𝑥 ) ) )
18		id	⊢ ( ⟨ 1 , 0 ⟩ ∈ ( Base ‘ 𝐽 ) → ⟨ 1 , 0 ⟩ ∈ ( Base ‘ 𝐽 ) )
19	12	eleq2i	⊢ ( 𝑥 ∈ 𝐼 ↔ 𝑥 ∈ ( Base ‘ 𝐽 ) )
20	1 2 3	pzriprnglem6	⊢ ( 𝑥 ∈ 𝐼 → ( ( ⟨ 1 , 0 ⟩ ( .r ‘ 𝐽 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝐽 ) ⟨ 1 , 0 ⟩ ) = 𝑥 ) )
21	19 20	sylbir	⊢ ( 𝑥 ∈ ( Base ‘ 𝐽 ) → ( ( ⟨ 1 , 0 ⟩ ( .r ‘ 𝐽 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝐽 ) ⟨ 1 , 0 ⟩ ) = 𝑥 ) )
22	21	a1i	⊢ ( ⟨ 1 , 0 ⟩ ∈ ( Base ‘ 𝐽 ) → ( 𝑥 ∈ ( Base ‘ 𝐽 ) → ( ( ⟨ 1 , 0 ⟩ ( .r ‘ 𝐽 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝐽 ) ⟨ 1 , 0 ⟩ ) = 𝑥 ) ) )
23	22	ralrimiv	⊢ ( ⟨ 1 , 0 ⟩ ∈ ( Base ‘ 𝐽 ) → ∀ 𝑥 ∈ ( Base ‘ 𝐽 ) ( ( ⟨ 1 , 0 ⟩ ( .r ‘ 𝐽 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝐽 ) ⟨ 1 , 0 ⟩ ) = 𝑥 ) )
24	17 18 23	rspcedvdw	⊢ ( ⟨ 1 , 0 ⟩ ∈ ( Base ‘ 𝐽 ) → ∃ 𝑖 ∈ ( Base ‘ 𝐽 ) ∀ 𝑥 ∈ ( Base ‘ 𝐽 ) ( ( 𝑖 ( .r ‘ 𝐽 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝐽 ) 𝑖 ) = 𝑥 ) )
25	14 24	ax-mp	⊢ ∃ 𝑖 ∈ ( Base ‘ 𝐽 ) ∀ 𝑥 ∈ ( Base ‘ 𝐽 ) ( ( 𝑖 ( .r ‘ 𝐽 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝐽 ) 𝑖 ) = 𝑥 )
26		eqid	⊢ ( Base ‘ 𝐽 ) = ( Base ‘ 𝐽 )
27		eqid	⊢ ( .r ‘ 𝐽 ) = ( .r ‘ 𝐽 )
28	26 27	isringrng	⊢ ( 𝐽 ∈ Ring ↔ ( 𝐽 ∈ Rng ∧ ∃ 𝑖 ∈ ( Base ‘ 𝐽 ) ∀ 𝑥 ∈ ( Base ‘ 𝐽 ) ( ( 𝑖 ( .r ‘ 𝐽 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝐽 ) 𝑖 ) = 𝑥 ) ) )
29	6 25 28	mpbir2an	⊢ 𝐽 ∈ Ring