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 ) )