Metamath Proof Explorer

Theorem lmimcnv

Description: The converse of a bijective module homomorphism is a bijective module homomorphism. (Contributed by Stefan O'Rear, 25-Jan-2015) (Revised by Mario Carneiro, 6-May-2015)

Ref Expression
Assertion lmimcnv ⊢ F ∈ S LMIso T → F -1 ∈ T LMIso S

Proof

Step Hyp Ref Expression
1 eqid ⊢ Base S = Base S
2 eqid ⊢ Base T = Base T
3 1 2 lmhmf ⊢ F ∈ S LMHom T → F : Base S ⟶ Base T
4 frel ⊢ F : Base S ⟶ Base T → Rel ⁡ F
5 3 4 syl ⊢ F ∈ S LMHom T → Rel ⁡ F
6 dfrel2 ⊢ Rel ⁡ F ↔ F -1 -1 = F
7 5 6 sylib ⊢ F ∈ S LMHom T → F -1 -1 = F
8 id ⊢ F ∈ S LMHom T → F ∈ S LMHom T
9 7 8 eqeltrd ⊢ F ∈ S LMHom T → F -1 -1 ∈ S LMHom T
10 9 anim1ci ⊢ F ∈ S LMHom T ∧ F -1 ∈ T LMHom S → F -1 ∈ T LMHom S ∧ F -1 -1 ∈ S LMHom T
11 islmim2 ⊢ F ∈ S LMIso T ↔ F ∈ S LMHom T ∧ F -1 ∈ T LMHom S
12 islmim2 ⊢ F -1 ∈ T LMIso S ↔ F -1 ∈ T LMHom S ∧ F -1 -1 ∈ S LMHom T
13 10 11 12 3imtr4i ⊢ F ∈ S LMIso T → F -1 ∈ T LMIso S