Metamath Proof Explorer

Theorem islmim

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

Ref Expression
Hypotheses islmim.b 
|- B = ( Base ` R )
islmim.c 
|- C = ( Base ` S )
Assertion islmim 
|- ( F e. ( R LMIso S ) <-> ( F e. ( R LMHom 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 df-lmim 
 |-  LMIso = ( a e. LMod , b e. LMod |-> { c e. ( a LMHom b ) | c : ( Base ` a ) -1-1-onto-> ( Base ` b ) } )
4 ovex 
 |-  ( a LMHom b ) e. _V
5 4 rabex 
 |-  { c e. ( a LMHom b ) | c : ( Base ` a ) -1-1-onto-> ( Base ` b ) } e. _V
6 oveq12 
 |-  ( ( a = R /\ b = S ) -> ( a LMHom b ) = ( R LMHom S ) )
7 fveq2 
 |-  ( a = R -> ( Base ` a ) = ( Base ` R ) )
8 7 1 eqtr4di 
 |-  ( a = R -> ( Base ` a ) = B )
9 fveq2 
 |-  ( b = S -> ( Base ` b ) = ( Base ` S ) )
10 9 2 eqtr4di 
 |-  ( b = S -> ( Base ` b ) = C )
11 f1oeq23 
 |-  ( ( ( Base ` a ) = B /\ ( Base ` b ) = C ) -> ( c : ( Base ` a ) -1-1-onto-> ( Base ` b ) <-> c : B -1-1-onto-> C ) )
12 8 10 11 syl2an 
 |-  ( ( a = R /\ b = S ) -> ( c : ( Base ` a ) -1-1-onto-> ( Base ` b ) <-> c : B -1-1-onto-> C ) )
13 6 12 rabeqbidv 
 |-  ( ( a = R /\ b = S ) -> { c e. ( a LMHom b ) | c : ( Base ` a ) -1-1-onto-> ( Base ` b ) } = { c e. ( R LMHom S ) | c : B -1-1-onto-> C } )
14 3 5 13 elovmpo 
 |-  ( F e. ( R LMIso S ) <-> ( R e. LMod /\ S e. LMod /\ F e. { c e. ( R LMHom S ) | c : B -1-1-onto-> C } ) )
15 df-3an 
 |-  ( ( R e. LMod /\ S e. LMod /\ F e. { c e. ( R LMHom S ) | c : B -1-1-onto-> C } ) <-> ( ( R e. LMod /\ S e. LMod ) /\ F e. { c e. ( R LMHom S ) | c : B -1-1-onto-> C } ) )
16 f1oeq1 
 |-  ( c = F -> ( c : B -1-1-onto-> C <-> F : B -1-1-onto-> C ) )
17 16 elrab 
 |-  ( F e. { c e. ( R LMHom S ) | c : B -1-1-onto-> C } <-> ( F e. ( R LMHom S ) /\ F : B -1-1-onto-> C ) )
18 17 anbi2i 
 |-  ( ( ( R e. LMod /\ S e. LMod ) /\ F e. { c e. ( R LMHom S ) | c : B -1-1-onto-> C } ) <-> ( ( R e. LMod /\ S e. LMod ) /\ ( F e. ( R LMHom S ) /\ F : B -1-1-onto-> C ) ) )
19 lmhmlmod1 
 |-  ( F e. ( R LMHom S ) -> R e. LMod )
20 lmhmlmod2 
 |-  ( F e. ( R LMHom S ) -> S e. LMod )
21 19 20 jca 
 |-  ( F e. ( R LMHom S ) -> ( R e. LMod /\ S e. LMod ) )
22 21 adantr 
 |-  ( ( F e. ( R LMHom S ) /\ F : B -1-1-onto-> C ) -> ( R e. LMod /\ S e. LMod ) )
23 22 pm4.71ri 
 |-  ( ( F e. ( R LMHom S ) /\ F : B -1-1-onto-> C ) <-> ( ( R e. LMod /\ S e. LMod ) /\ ( F e. ( R LMHom S ) /\ F : B -1-1-onto-> C ) ) )
24 18 23 bitr4i 
 |-  ( ( ( R e. LMod /\ S e. LMod ) /\ F e. { c e. ( R LMHom S ) | c : B -1-1-onto-> C } ) <-> ( F e. ( R LMHom S ) /\ F : B -1-1-onto-> C ) )
25 14 15 24 3bitri 
 |-  ( F e. ( R LMIso S ) <-> ( F e. ( R LMHom S ) /\ F : B -1-1-onto-> C ) )