Metamath Proof Explorer


Definition df-ric

Description: Define the ring isomorphism relation, analogous to df-gic : Two (unital) rings are said to beisomorphic iff they are connected by at least one isomorphism. Isomorphic rings share all global ring properties, but to relate local properties requires knowledge of a specific isomorphism. (Contributed by AV, 24-Dec-2019)

Ref Expression
Assertion df-ric
|- ~=r = ( `' RingIso " ( _V \ 1o ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cric
 |-  ~=r
1 crs
 |-  RingIso
2 1 ccnv
 |-  `' RingIso
3 cvv
 |-  _V
4 c1o
 |-  1o
5 3 4 cdif
 |-  ( _V \ 1o )
6 2 5 cima
 |-  ( `' RingIso " ( _V \ 1o ) )
7 0 6 wceq
 |-  ~=r = ( `' RingIso " ( _V \ 1o ) )