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	⊢ 𝑅 = ( ℤring ×s ℤring )
	pzriprng.i	⊢ 𝐼 = ( ℤ × { 0 } )
	pzriprng.j	⊢ 𝐽 = ( 𝑅 ↾s 𝐼 )
	pzriprng.1	⊢ 1 = ( 1r ‘ 𝐽 )
Assertion	pzriprnglem9	⊢ 1 = ⟨ 1 , 0 ⟩

Proof

Step	Hyp	Ref	Expression
1		pzriprng.r	⊢ 𝑅 = ( ℤring ×s ℤring )
2		pzriprng.i	⊢ 𝐼 = ( ℤ × { 0 } )
3		pzriprng.j	⊢ 𝐽 = ( 𝑅 ↾s 𝐼 )
4		pzriprng.1	⊢ 1 = ( 1r ‘ 𝐽 )
5		1z	⊢ 1 ∈ ℤ
6		c0ex	⊢ 0 ∈ V
7	6	snid	⊢ 0 ∈ { 0 }
8	2	eleq2i	⊢ ( ⟨ 1 , 0 ⟩ ∈ 𝐼 ↔ ⟨ 1 , 0 ⟩ ∈ ( ℤ × { 0 } ) )
9		opelxp	⊢ ( ⟨ 1 , 0 ⟩ ∈ ( ℤ × { 0 } ) ↔ ( 1 ∈ ℤ ∧ 0 ∈ { 0 } ) )
10	8 9	bitri	⊢ ( ⟨ 1 , 0 ⟩ ∈ 𝐼 ↔ ( 1 ∈ ℤ ∧ 0 ∈ { 0 } ) )
11	5 7 10	mpbir2an	⊢ ⟨ 1 , 0 ⟩ ∈ 𝐼
12	1 2 3	pzriprnglem6	⊢ ( 𝑥 ∈ 𝐼 → ( ( ⟨ 1 , 0 ⟩ ( .r ‘ 𝐽 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝐽 ) ⟨ 1 , 0 ⟩ ) = 𝑥 ) )
13	12	rgen	⊢ ∀ 𝑥 ∈ 𝐼 ( ( ⟨ 1 , 0 ⟩ ( .r ‘ 𝐽 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝐽 ) ⟨ 1 , 0 ⟩ ) = 𝑥 )
14	11 13	pm3.2i	⊢ ( ⟨ 1 , 0 ⟩ ∈ 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( ( ⟨ 1 , 0 ⟩ ( .r ‘ 𝐽 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝐽 ) ⟨ 1 , 0 ⟩ ) = 𝑥 ) )
15	1 2 3	pzriprnglem7	⊢ 𝐽 ∈ Ring
16	1 2	pzriprnglem5	⊢ 𝐼 ∈ ( SubRng ‘ 𝑅 )
17	3	subrngbas	⊢ ( 𝐼 ∈ ( SubRng ‘ 𝑅 ) → 𝐼 = ( Base ‘ 𝐽 ) )
18	16 17	ax-mp	⊢ 𝐼 = ( Base ‘ 𝐽 )
19		eqid	⊢ ( .r ‘ 𝐽 ) = ( .r ‘ 𝐽 )
20	18 19 4	isringid	⊢ ( 𝐽 ∈ Ring → ( ( ⟨ 1 , 0 ⟩ ∈ 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( ( ⟨ 1 , 0 ⟩ ( .r ‘ 𝐽 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝐽 ) ⟨ 1 , 0 ⟩ ) = 𝑥 ) ) ↔ 1 = ⟨ 1 , 0 ⟩ ) )
21	15 20	ax-mp	⊢ ( ( ⟨ 1 , 0 ⟩ ∈ 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( ( ⟨ 1 , 0 ⟩ ( .r ‘ 𝐽 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝐽 ) ⟨ 1 , 0 ⟩ ) = 𝑥 ) ) ↔ 1 = ⟨ 1 , 0 ⟩ )
22	14 21	mpbi	⊢ 1 = ⟨ 1 , 0 ⟩