Metamath Proof Explorer

Theorem brlmic

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

Ref Expression
Assertion brlmic 
|- ( R ~=m S <-> ( R LMIso S ) =/= (/) )

Proof

Step Hyp Ref Expression
1 df-lmic 
 |-  ~=m = ( `' LMIso " ( _V \ 1o ) )
2 lmimfn 
 |-  LMIso Fn ( LMod X. LMod )
3 1 2 brwitnlem 
 |-  ( R ~=m S <-> ( R LMIso S ) =/= (/) )