Definition df-lmim

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)

	Ref	Expression
Assertion	df-lmim	|- LMIso = ( s e. LMod , t e. LMod |-> { g e. ( s LMHom t ) | g : ( Base ` s ) -1-1-onto-> ( Base ` t ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clmim	|- LMIso
1		vs	|- s
2		clmod	|- LMod
3		vt	|- t
4		vg	|- g
5	1	cv	|- s
6		clmhm	|- LMHom
7	3	cv	|- t
8	5 7 6	co	|- ( s LMHom t )
9	4	cv	|- g
10		cbs	|- Base
11	5 10	cfv	|- ( Base ` s )
12	7 10	cfv	|- ( Base ` t )
13	11 12 9	wf1o	|- g : ( Base ` s ) -1-1-onto-> ( Base ` t )
14	13 4 8	crab	|- { g e. ( s LMHom t ) | g : ( Base ` s ) -1-1-onto-> ( Base ` t ) }
15	1 3 2 2 14	cmpo	|- ( s e. LMod , t e. LMod |-> { g e. ( s LMHom t ) | g : ( Base ` s ) -1-1-onto-> ( Base ` t ) } )
16	0 15	wceq	|- LMIso = ( s e. LMod , t e. LMod |-> { g e. ( s LMHom t ) | g : ( Base ` s ) -1-1-onto-> ( Base ` t ) } )