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