Definition df-lmim 19789

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

Distinct variable group:   𝑡,𝑠,𝑔

Detailed syntax breakdown of Definition df-lmim

Step	Hyp	Ref	Expression
1		clmim 19786	. 2 class LMIso
2		vs	. . 3 setvar 𝑠
3		vt	. . 3 setvar 𝑡
4		clmod 19628	. . 3 class LMod
5	2	cv 1532	. . . . . 6 class 𝑠
6		cbs 16477	. . . . . 6 class Base
7	5, 6	cfv 6350	. . . . 5 class (Base‘𝑠)
8	3	cv 1532	. . . . . 6 class 𝑡
9	8, 6	cfv 6350	. . . . 5 class (Base‘𝑡)
10		vg	. . . . . 6 setvar 𝑔
11	10	cv 1532	. . . . 5 class 𝑔
12	7, 9, 11	wf1o 6349	. . . 4 wff 𝑔:(Base‘𝑠)–1-1-onto→(Base‘𝑡)
13		clmhm 19785	. . . . 5 class LMHom
14	5, 8, 13	co 7150	. . . 4 class (𝑠 LMHom 𝑡)
15	12, 10, 14	crab 3142	. . 3 class {𝑔 ∈ (𝑠 LMHom 𝑡) ∣ 𝑔:(Base‘𝑠)–1-1-onto→(Base‘𝑡)}
16	2, 3, 4, 4, 15	cmpo 7152	. 2 class (𝑠 ∈ LMod, 𝑡 ∈ LMod ↦ {𝑔 ∈ (𝑠 LMHom 𝑡) ∣ 𝑔:(Base‘𝑠)–1-1-onto→(Base‘𝑡)})
17	1, 16	wceq 1533	1 wff LMIso = (𝑠 ∈ LMod, 𝑡 ∈ LMod ↦ {𝑔 ∈ (𝑠 LMHom 𝑡) ∣ 𝑔:(Base‘𝑠)–1-1-onto→(Base‘𝑡)})

This definition is referenced by:  lmimfn  19792  islmim  19828