Metamath Proof Explorer

Theorem pzriprng

Description: The non-unital ring ( ZZring Xs. ZZring ) is unital. Direct proof in contrast to pzriprngALT . (Contributed by AV, 25-Mar-2025)

Ref Expression
Assertion pzriprng 
|- ( ZZring Xs. ZZring ) e. Ring

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 xpsringd 
 |-  ( ZZring e. Ring -> ( ZZring Xs. ZZring ) e. Ring )
5 1 4 ax-mp 
 |-  ( ZZring Xs. ZZring ) e. Ring