MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-lmim Unicode version

Definition df-lmim 15780
Description: An isomorphism of modules is a homomorphism which is also a bijection, i.e. it preserves equality as well as the group and scalar operations. (Contributed by Stefan O'Rear, 21-Jan-2015.)
Assertion
Ref Expression
df-lmim  |- LMIso  =  ( s  e.  LMod ,  t  e.  LMod  |->  { g  e.  ( s LMHom  t
)  |  g : ( Base `  s
)
-1-1-onto-> ( Base `  t ) } )
Distinct variable group:    t, s, g

Detailed syntax breakdown of Definition df-lmim
StepHypRef Expression
1 clmim 15777 . 2  class LMIso
2 vs . . 3  set  s
3 vt . . 3  set  t
4 clmod 15627 . . 3  class  LMod
52cv 1622 . . . . . 6  class  s
6 cbs 13148 . . . . . 6  class  Base
75, 6cfv 5255 . . . . 5  class  ( Base `  s )
83cv 1622 . . . . . 6  class  t
98, 6cfv 5255 . . . . 5  class  ( Base `  t )
10 vg . . . . . 6  set  g
1110cv 1622 . . . . 5  class  g
127, 9, 11wf1o 5254 . . . 4  wff  g : ( Base `  s
)
-1-1-onto-> ( Base `  t )
13 clmhm 15776 . . . . 5  class LMHom
145, 8, 13co 5858 . . . 4  class  ( s LMHom 
t )
1512, 10, 14crab 2547 . . 3  class  { g  e.  ( s LMHom  t
)  |  g : ( Base `  s
)
-1-1-onto-> ( Base `  t ) }
162, 3, 4, 4, 15cmpt2 5860 . 2  class  ( s  e.  LMod ,  t  e. 
LMod  |->  { g  e.  ( s LMHom  t )  |  g : (
Base `  s ) -1-1-onto-> ( Base `  t ) } )
171, 16wceq 1623 1  wff LMIso  =  ( s  e.  LMod ,  t  e.  LMod  |->  { g  e.  ( s LMHom  t
)  |  g : ( Base `  s
)
-1-1-onto-> ( Base `  t ) } )
Colors of variables: wff set class
This definition is referenced by:  lmimfn  15783  islmim  15815
  Copyright terms: Public domain W3C validator