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 = ( 𝑠 ∈ LMod , 𝑡 ∈ LMod ↦ { 𝑔 ∈ ( 𝑠 LMHom 𝑡 ) ∣ 𝑔 : ( Base ‘ 𝑠 ) –1-1-onto→ ( Base ‘ 𝑡 ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clmim	⊢ LMIso
1		vs	⊢ 𝑠
2		clmod	⊢ LMod
3		vt	⊢ 𝑡
4		vg	⊢ 𝑔
5	1	cv	⊢ 𝑠
6		clmhm	⊢ LMHom
7	3	cv	⊢ 𝑡
8	5 7 6	co	⊢ ( 𝑠 LMHom 𝑡 )
9	4	cv	⊢ 𝑔
10		cbs	⊢ Base
11	5 10	cfv	⊢ ( Base ‘ 𝑠 )
12	7 10	cfv	⊢ ( Base ‘ 𝑡 )
13	11 12 9	wf1o	⊢ 𝑔 : ( Base ‘ 𝑠 ) –1-1-onto→ ( Base ‘ 𝑡 )
14	13 4 8	crab	⊢ { 𝑔 ∈ ( 𝑠 LMHom 𝑡 ) ∣ 𝑔 : ( Base ‘ 𝑠 ) –1-1-onto→ ( Base ‘ 𝑡 ) }
15	1 3 2 2 14	cmpo	⊢ ( 𝑠 ∈ LMod , 𝑡 ∈ LMod ↦ { 𝑔 ∈ ( 𝑠 LMHom 𝑡 ) ∣ 𝑔 : ( Base ‘ 𝑠 ) –1-1-onto→ ( Base ‘ 𝑡 ) } )
16	0 15	wceq	⊢ LMIso = ( 𝑠 ∈ LMod , 𝑡 ∈ LMod ↦ { 𝑔 ∈ ( 𝑠 LMHom 𝑡 ) ∣ 𝑔 : ( Base ‘ 𝑠 ) –1-1-onto→ ( Base ‘ 𝑡 ) } )