This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ( 𝑆 ∈ LVec ↔ 𝑇 ∈ LVec ) )

Proof

Step Hyp Ref Expression
1 lmhmlmod1 ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝑆 ∈ LMod )
2 lmhmlmod2 ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝑇 ∈ LMod )
3 1 2 2thd ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ( 𝑆 ∈ LMod ↔ 𝑇 ∈ LMod ) )
4 eqid ⊢ ( Scalar ‘ 𝑆 ) = ( Scalar ‘ 𝑆 )
5 eqid ⊢ ( Scalar ‘ 𝑇 ) = ( Scalar ‘ 𝑇 )
6 4 5 lmhmsca ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ( Scalar ‘ 𝑇 ) = ( Scalar ‘ 𝑆 ) )
7 6 eqcomd ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ( Scalar ‘ 𝑆 ) = ( Scalar ‘ 𝑇 ) )
8 7 eleq1d ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ( ( Scalar ‘ 𝑆 ) ∈ DivRing ↔ ( Scalar ‘ 𝑇 ) ∈ DivRing ) )
9 3 8 anbi12d ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ( ( 𝑆 ∈ LMod ∧ ( Scalar ‘ 𝑆 ) ∈ DivRing ) ↔ ( 𝑇 ∈ LMod ∧ ( Scalar ‘ 𝑇 ) ∈ DivRing ) ) )
10 4 islvec ⊢ ( 𝑆 ∈ LVec ↔ ( 𝑆 ∈ LMod ∧ ( Scalar ‘ 𝑆 ) ∈ DivRing ) )
11 5 islvec ⊢ ( 𝑇 ∈ LVec ↔ ( 𝑇 ∈ LMod ∧ ( Scalar ‘ 𝑇 ) ∈ DivRing ) )
12 9 10 11 3bitr4g ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ( 𝑆 ∈ LVec ↔ 𝑇 ∈ LVec ) )