Metamath Proof Explorer

Theorem lvecpropd

Description: If two structures have the same components (properties), one is a left vector space iff the other one is. (Contributed by Mario Carneiro, 27-Jun-2015)

		Ref	Expression
	Hypotheses	lvecpropd.1	$⊢ φ \to B = {Base}_{K}$
		lvecpropd.2	$⊢ φ \to B = {Base}_{L}$
		lvecpropd.3	$⊢ (φ \land (x \in B \land y \in B)) \to x +_{K} y = x +_{L} y$
		lvecpropd.4	$⊢ φ \to F = Scalar (K)$
		lvecpropd.5	$⊢ φ \to F = Scalar (L)$
		lvecpropd.6	$⊢ P = {Base}_{F}$
		lvecpropd.7	$⊢ (φ \land (x \in P \land y \in B)) \to x \cdot_{K} y = x \cdot_{L} y$
	Assertion	lvecpropd	$⊢ φ \to (K \in LVec \leftrightarrow L \in LVec)$

Proof

Step	Hyp	Ref	Expression
1		lvecpropd.1	$⊢ φ \to B = {Base}_{K}$
2		lvecpropd.2	$⊢ φ \to B = {Base}_{L}$
3		lvecpropd.3	$⊢ (φ \land (x \in B \land y \in B)) \to x +_{K} y = x +_{L} y$
4		lvecpropd.4	$⊢ φ \to F = Scalar (K)$
5		lvecpropd.5	$⊢ φ \to F = Scalar (L)$
6		lvecpropd.6	$⊢ P = {Base}_{F}$
7		lvecpropd.7	$⊢ (φ \land (x \in P \land y \in B)) \to x \cdot_{K} y = x \cdot_{L} y$
8	1 2 3 4 5 6 7	lmodpropd	$⊢ φ \to (K \in LMod \leftrightarrow L \in LMod)$
9	4 5	eqtr3d	$⊢ φ \to Scalar (K) = Scalar (L)$
10	9	eleq1d	$⊢ φ \to (Scalar (K) \in DivRing \leftrightarrow Scalar (L) \in DivRing)$
11	8 10	anbi12d	$⊢ φ \to ((K \in LMod \land Scalar (K) \in DivRing) \leftrightarrow (L \in LMod \land Scalar (L) \in DivRing))$
12		eqid	$⊢ Scalar (K) = Scalar (K)$
13	12	islvec	$⊢ K \in LVec \leftrightarrow (K \in LMod \land Scalar (K) \in DivRing)$
14		eqid	$⊢ Scalar (L) = Scalar (L)$
15	14	islvec	$⊢ L \in LVec \leftrightarrow (L \in LMod \land Scalar (L) \in DivRing)$
16	11 13 15	3bitr4g	$⊢ φ \to (K \in LVec \leftrightarrow L \in LVec)$