Theorem brlmic

Description: The relation "is isomorphic to" for modules. (Contributed by Stefan O'Rear, 25-Jan-2015)

	Ref	Expression
Assertion	brlmic	$$⊢R{\simeq }_{𝑚}S\leftrightarrow R\mathrm{LMIso}S\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		df-lmic	$$⊢{\simeq }_{𝑚}={\mathrm{LMIso}}^{-1}\left[\mathrm{V}\setminus 1_{𝑜}\right]$$
2		lmimfn	$$⊢\mathrm{LMIso}Fn\left(\mathrm{LMod}\times \mathrm{LMod}\right)$$
3	1 2	brwitnlem	$$⊢R{\simeq }_{𝑚}S\leftrightarrow R\mathrm{LMIso}S\ne \varnothing$$