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	$$⊢\mathrm{LMIso}=\left(s\in \mathrm{LMod},t\in \mathrm{LMod}⟼\left\{g\in \left(s\mathrm{LMHom}t\right)|g:{\mathrm{Base}}_s\underset{1-1\; onto}{⟶}{\mathrm{Base}}_t\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clmim	$$class\mathrm{LMIso}$$
1		vs	$$setvars$$
2		clmod	$$class\mathrm{LMod}$$
3		vt	$$setvart$$
4		vg	$$setvarg$$
5	1	cv	$$setvars$$
6		clmhm	$$class\mathrm{LMHom}$$
7	3	cv	$$setvart$$
8	5 7 6	co	$$class\left(s\mathrm{LMHom}t\right)$$
9	4	cv	$$setvarg$$
10		cbs	$$class\mathrm{Base}$$
11	5 10	cfv	$$class{\mathrm{Base}}_s$$
12	7 10	cfv	$$class{\mathrm{Base}}_t$$
13	11 12 9	wf1o	$$wffg:{\mathrm{Base}}_s\underset{1-1\; onto}{⟶}{\mathrm{Base}}_t$$
14	13 4 8	crab	$$class\left\{g\in \left(s\mathrm{LMHom}t\right)|g:{\mathrm{Base}}_s\underset{1-1\; onto}{⟶}{\mathrm{Base}}_t\right\}$$
15	1 3 2 2 14	cmpo	$$class\left(s\in \mathrm{LMod},t\in \mathrm{LMod}⟼\left\{g\in \left(s\mathrm{LMHom}t\right)|g:{\mathrm{Base}}_s\underset{1-1\; onto}{⟶}{\mathrm{Base}}_t\right\}\right)$$
16	0 15	wceq	$$wff\mathrm{LMIso}=\left(s\in \mathrm{LMod},t\in \mathrm{LMod}⟼\left\{g\in \left(s\mathrm{LMHom}t\right)|g:{\mathrm{Base}}_s\underset{1-1\; onto}{⟶}{\mathrm{Base}}_t\right\}\right)$$