Definition df-lmim 19798

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 19795	. 2 class LMIso
2		vs	. . 3 setvar 𝑠
3		vt	. . 3 setvar 𝑡
4		clmod 19637	. . 3 class LMod
5	2	cv 1535	. . . . . 6 class 𝑠
6		cbs 16486	. . . . . 6 class Base
7	5, 6	cfv 6358	. . . . 5 class (Base‘𝑠)
8	3	cv 1535	. . . . . 6 class 𝑡
9	8, 6	cfv 6358	. . . . 5 class (Base‘𝑡)
10		vg	. . . . . 6 setvar 𝑔
11	10	cv 1535	. . . . 5 class 𝑔
12	7, 9, 11	wf1o 6357	. . . 4 wff 𝑔:(Base‘𝑠)–1-1-onto→(Base‘𝑡)
13		clmhm 19794	. . . . 5 class LMHom
14	5, 8, 13	co 7159	. . . 4 class (𝑠 LMHom 𝑡)
15	12, 10, 14	crab 3145	. . 3 class {𝑔 ∈ (𝑠 LMHom 𝑡) ∣ 𝑔:(Base‘𝑠)–1-1-onto→(Base‘𝑡)}
16	2, 3, 4, 4, 15	cmpo 7161	. 2 class (𝑠 ∈ LMod, 𝑡 ∈ LMod ↦ {𝑔 ∈ (𝑠 LMHom 𝑡) ∣ 𝑔:(Base‘𝑠)–1-1-onto→(Base‘𝑡)})
17	1, 16	wceq 1536	1 wff LMIso = (𝑠 ∈ LMod, 𝑡 ∈ LMod ↦ {𝑔 ∈ (𝑠 LMHom 𝑡) ∣ 𝑔:(Base‘𝑠)–1-1-onto→(Base‘𝑡)})

This definition is referenced by:  lmimfn  19801  islmim  19837