This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∈ LMod , t ∈ LMod ⟼ g ∈ s LMHom t | g : Base s ⟶ 1-1 onto Base t

Detailed syntax breakdown

Step Hyp Ref Expression
0 clmim class LMIso
1 vs setvar s
2 clmod class LMod
3 vt setvar t
4 vg setvar g
5 1 cv setvar s
6 clmhm class LMHom
7 3 cv setvar t
8 5 7 6 co class s LMHom t
9 4 cv setvar g
10 cbs class Base
11 5 10 cfv class Base s
12 7 10 cfv class Base t
13 11 12 9 wf1o wff g : Base s ⟶ 1-1 onto Base t
14 13 4 8 crab class g ∈ s LMHom t | g : Base s ⟶ 1-1 onto Base t
15 1 3 2 2 14 cmpo class s ∈ LMod , t ∈ LMod ⟼ g ∈ s LMHom t | g : Base s ⟶ 1-1 onto Base t
16 0 15 wceq wff LMIso = s ∈ LMod , t ∈ LMod ⟼ g ∈ s LMHom t | g : Base s ⟶ 1-1 onto Base t