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	$$⊢{\simeq }_{𝑟}={\mathrm{RingIso}}^{-1}\left[\mathrm{V}\setminus 1_{𝑜}\right]$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cric	$$class{\simeq }_{𝑟}$$
1		crs	$$class\mathrm{RingIso}$$
2	1	ccnv	$$class{\mathrm{RingIso}}^{-1}$$
3		cvv	$$class\mathrm{V}$$
4		c1o	$$class{1}_{𝑜}$$
5	3 4	cdif	$$class\left(\mathrm{V}\setminus 1_{𝑜}\right)$$
6	2 5	cima	$$class{\mathrm{RingIso}}^{-1}\left[\mathrm{V}\setminus 1_{𝑜}\right]$$
7	0 6	wceq	$$wff{\simeq }_{𝑟}={\mathrm{RingIso}}^{-1}\left[\mathrm{V}\setminus 1_{𝑜}\right]$$