Metamath Proof Explorer

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 ` ( ZZring Xs. ZZring ) ) = <. 1 , 1 >.

Proof

Step Hyp Ref Expression
1 zringring 
 |-  ZZring e. Ring
2 eqid 
 |-  ( ZZring Xs. ZZring ) = ( ZZring Xs. ZZring )
3 id 
 |-  ( ZZring e. Ring -> ZZring e. Ring )
4 2 3 3 xpsring1d 
 |-  ( ZZring e. Ring -> ( 1r ` ( ZZring Xs. ZZring ) ) = <. ( 1r ` ZZring ) , ( 1r ` ZZring ) >. )
5 1 4 ax-mp 
 |-  ( 1r ` ( ZZring Xs. ZZring ) ) = <. ( 1r ` ZZring ) , ( 1r ` ZZring ) >.
6 zring1 
 |-  1 = ( 1r ` ZZring )
7 6 6 opeq12i 
 |-  <. 1 , 1 >. = <. ( 1r ` ZZring ) , ( 1r ` ZZring ) >.
8 5 7 eqtr4i 
 |-  ( 1r ` ( ZZring Xs. ZZring ) ) = <. 1 , 1 >.