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 R LMIso S F 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 LMod , b LMod c a LMHom b | c : Base a 1-1 onto Base b
4 ovex a LMHom b V
5 4 rabex c a LMHom b | c : Base a 1-1 onto Base b 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 a LMHom b | c : Base a 1-1 onto Base b = c R LMHom S | c : B 1-1 onto C
14 3 5 13 elovmpo F R LMIso S R LMod S LMod F c R LMHom S | c : B 1-1 onto C
15 df-3an R LMod S LMod F c R LMHom S | c : B 1-1 onto C R LMod S LMod F c 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 c R LMHom S | c : B 1-1 onto C F R LMHom S F : B 1-1 onto C
18 17 anbi2i R LMod S LMod F c R LMHom S | c : B 1-1 onto C R LMod S LMod F R LMHom S F : B 1-1 onto C
19 lmhmlmod1 F R LMHom S R LMod
20 lmhmlmod2 F R LMHom S S LMod
21 19 20 jca F R LMHom S R LMod S LMod
22 21 adantr F R LMHom S F : B 1-1 onto C R LMod S LMod
23 22 pm4.71ri F R LMHom S F : B 1-1 onto C R LMod S LMod F R LMHom S F : B 1-1 onto C
24 18 23 bitr4i R LMod S LMod F c R LMHom S | c : B 1-1 onto C F R LMHom S F : B 1-1 onto C
25 14 15 24 3bitri F R LMIso S F R LMHom S F : B 1-1 onto C