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 ) ) |
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 ) ) |