Theorem pzriprng1

Description: The ring unity of the ring ( ZZring Xs. ZZring ) . Direct proof in contrast to pzriprng1ALT . (Contributed by AV, 25-Mar-2025)

	Ref	Expression
Assertion	pzriprng1	⊢ ( 1r ‘ ( ℤring ×s ℤring ) ) = ⟨ 1 , 1 ⟩

Proof

Step	Hyp	Ref	Expression
1		zringring	⊢ ℤring ∈ Ring
2		eqid	⊢ ( ℤring ×s ℤring ) = ( ℤring ×s ℤring )
3		id	⊢ ( ℤring ∈ Ring → ℤring ∈ Ring )
4	2 3 3	xpsring1d	⊢ ( ℤring ∈ Ring → ( 1r ‘ ( ℤring ×s ℤring ) ) = ⟨ ( 1r ‘ ℤring ) , ( 1r ‘ ℤring ) ⟩ )
5	1 4	ax-mp	⊢ ( 1r ‘ ( ℤring ×s ℤring ) ) = ⟨ ( 1r ‘ ℤring ) , ( 1r ‘ ℤring ) ⟩
6		zring1	⊢ 1 = ( 1r ‘ ℤring )
7	6 6	opeq12i	⊢ ⟨ 1 , 1 ⟩ = ⟨ ( 1r ‘ ℤring ) , ( 1r ‘ ℤring ) ⟩
8	5 7	eqtr4i	⊢ ( 1r ‘ ( ℤring ×s ℤring ) ) = ⟨ 1 , 1 ⟩