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 \in (S LMHom T) \to (S \in LVec \leftrightarrow T \in LVec)$

Step	Hyp	Ref	Expression
1		lmhmlmod1	$⊢ F \in (S LMHom T) \to S \in LMod$
2		lmhmlmod2	$⊢ F \in (S LMHom T) \to T \in LMod$
3	1 2	2thd	$⊢ F \in (S LMHom T) \to (S \in LMod \leftrightarrow T \in LMod)$
4		eqid	$⊢ Scalar (S) = Scalar (S)$
5		eqid	$⊢ Scalar (T) = Scalar (T)$
6	4 5	lmhmsca	$⊢ F \in (S LMHom T) \to Scalar (T) = Scalar (S)$
7	6	eqcomd	$⊢ F \in (S LMHom T) \to Scalar (S) = Scalar (T)$
8	7	eleq1d	$⊢ F \in (S LMHom T) \to (Scalar (S) \in DivRing \leftrightarrow Scalar (T) \in DivRing)$
9	3 8	anbi12d	$⊢ F \in (S LMHom T) \to ((S \in LMod \land Scalar (S) \in DivRing) \leftrightarrow (T \in LMod \land Scalar (T) \in DivRing))$
10	4	islvec	$⊢ S \in LVec \leftrightarrow (S \in LMod \land Scalar (S) \in DivRing)$
11	5	islvec	$⊢ T \in LVec \leftrightarrow (T \in LMod \land Scalar (T) \in DivRing)$
12	9 10 11	3bitr4g	$⊢ F \in (S LMHom T) \to (S \in LVec \leftrightarrow T \in LVec)$

Metamath Proof Explorer