Metamath Proof Explorer


Theorem lmimf1o

Description: An isomorphism of left modules is a bijection. (Contributed by Stefan O'Rear, 21-Jan-2015)

Ref Expression
Hypotheses islmim.b
|- B = ( Base ` R )
islmim.c
|- C = ( Base ` S )
Assertion lmimf1o
|- ( F e. ( R LMIso S ) -> F : B -1-1-onto-> C )

Proof

Step Hyp Ref Expression
1 islmim.b
 |-  B = ( Base ` R )
2 islmim.c
 |-  C = ( Base ` S )
3 1 2 islmim
 |-  ( F e. ( R LMIso S ) <-> ( F e. ( R LMHom S ) /\ F : B -1-1-onto-> C ) )
4 3 simprbi
 |-  ( F e. ( R LMIso S ) -> F : B -1-1-onto-> C )