Metamath Proof Explorer


Theorem opprnzr

Description: The opposite of a nonzero ring is nonzero. (Contributed by Mario Carneiro, 17-Jun-2015)

Ref Expression
Hypothesis opprnzr.1 O=opprR
Assertion opprnzr RNzRingONzRing

Proof

Step Hyp Ref Expression
1 opprnzr.1 O=opprR
2 nzrring RNzRingRRing
3 1 opprring RRingORing
4 2 3 syl RNzRingORing
5 eqid BaseR=BaseR
6 5 isnzr2 RNzRingRRing2𝑜BaseR
7 6 simprbi RNzRing2𝑜BaseR
8 1 5 opprbas BaseR=BaseO
9 8 isnzr2 ONzRingORing2𝑜BaseR
10 4 7 9 sylanbrc RNzRingONzRing