Definition df-lmim 19023

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

Step	Hyp	Ref	Expression
1		clmim 19020	. 2 class LMIso
2		vs	. . 3 setvar s
3		vt	. . 3 setvar t
4		clmod 18863	. . 3 class LMod
5	2	cv 1482	. . . . . 6 class s
6		cbs 15857	. . . . . 6 class Base
7	5, 6	cfv 5888	. . . . 5 class ( Base ` s )
8	3	cv 1482	. . . . . 6 class t
9	8, 6	cfv 5888	. . . . 5 class ( Base ` t )
10		vg	. . . . . 6 setvar g
11	10	cv 1482	. . . . 5 class g
12	7, 9, 11	wf1o 5887	. . . 4 wff g : ( Base ` s ) -1-1-onto-> ( Base ` t )
13		clmhm 19019	. . . . 5 class LMHom
14	5, 8, 13	co 6650	. . . 4 class ( s LMHom t )
15	12, 10, 14	crab 2916	. . 3 class { g e. ( s LMHom t ) | g : ( Base ` s ) -1-1-onto-> ( Base ` t ) }
16	2, 3, 4, 4, 15	cmpt2 6652	. 2 class ( s e. LMod , t e. LMod |-> { g e. ( s LMHom t ) | g : ( Base ` s ) -1-1-onto-> ( Base ` t ) } )
17	1, 16	wceq 1483	1 wff LMIso = ( s e. LMod , t e. LMod |-> { g e. ( s LMHom t ) | g : ( Base ` s ) -1-1-onto-> ( Base ` t ) } )

This definition is referenced by:  lmimfn  19026  islmim  19062