Metamath Proof Explorer


Definition df-lmic

Description: Two modules are said to be isomorphic iff they are connected by at least one isomorphism. (Contributed by Stefan O'Rear, 25-Jan-2015)

Ref Expression
Assertion df-lmic
|- ~=m = ( `' LMIso " ( _V \ 1o ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 clmic
 |-  ~=m
1 clmim
 |-  LMIso
2 1 ccnv
 |-  `' LMIso
3 cvv
 |-  _V
4 c1o
 |-  1o
5 3 4 cdif
 |-  ( _V \ 1o )
6 2 5 cima
 |-  ( `' LMIso " ( _V \ 1o ) )
7 0 6 wceq
 |-  ~=m = ( `' LMIso " ( _V \ 1o ) )