Metamath Proof Explorer

Theorem lmhmlvec

Description: The property for modules to be vector spaces is invariant under module isomorphism. (Contributed by Steven Nguyen, 15-Aug-2023)

Ref Expression
Assertion lmhmlvec ⊢ F ∈ S LMHom T → S ∈ LVec ↔ T ∈ LVec

Proof

Step Hyp Ref Expression
1 lmhmlmod1 ⊢ F ∈ S LMHom T → S ∈ LMod
2 lmhmlmod2 ⊢ F ∈ S LMHom T → T ∈ LMod
3 1 2 2thd ⊢ F ∈ S LMHom T → S ∈ LMod ↔ T ∈ LMod
4 eqid ⊢ Scalar ⁡ S = Scalar ⁡ S
5 eqid ⊢ Scalar ⁡ T = Scalar ⁡ T
6 4 5 lmhmsca ⊢ F ∈ S LMHom T → Scalar ⁡ T = Scalar ⁡ S
7 6 eqcomd ⊢ F ∈ S LMHom T → Scalar ⁡ S = Scalar ⁡ T
8 7 eleq1d ⊢ F ∈ S LMHom T → Scalar ⁡ S ∈ DivRing ↔ Scalar ⁡ T ∈ DivRing
9 3 8 anbi12d ⊢ F ∈ S LMHom T → S ∈ LMod ∧ Scalar ⁡ S ∈ DivRing ↔ T ∈ LMod ∧ Scalar ⁡ T ∈ DivRing
10 4 islvec ⊢ S ∈ LVec ↔ S ∈ LMod ∧ Scalar ⁡ S ∈ DivRing
11 5 islvec ⊢ T ∈ LVec ↔ T ∈ LMod ∧ Scalar ⁡ T ∈ DivRing
12 9 10 11 3bitr4g ⊢ F ∈ S LMHom T → S ∈ LVec ↔ T ∈ LVec