Metamath Proof Explorer


Theorem lvecprop2d

Description: If two structures have the same components (properties), one is a left vector space iff the other one is. This version of lvecpropd also breaks up the components of the scalar ring. (Contributed by Mario Carneiro, 27-Jun-2015)

Ref Expression
Hypotheses lvecprop2d.b1 φ B = Base K
lvecprop2d.b2 φ B = Base L
lvecprop2d.f F = Scalar K
lvecprop2d.g G = Scalar L
lvecprop2d.p1 φ P = Base F
lvecprop2d.p2 φ P = Base G
lvecprop2d.1 φ x B y B x + K y = x + L y
lvecprop2d.2 φ x P y P x + F y = x + G y
lvecprop2d.3 φ x P y P x F y = x G y
lvecprop2d.4 φ x P y B x K y = x L y
Assertion lvecprop2d φ K LVec L LVec

Proof

Step Hyp Ref Expression
1 lvecprop2d.b1 φ B = Base K
2 lvecprop2d.b2 φ B = Base L
3 lvecprop2d.f F = Scalar K
4 lvecprop2d.g G = Scalar L
5 lvecprop2d.p1 φ P = Base F
6 lvecprop2d.p2 φ P = Base G
7 lvecprop2d.1 φ x B y B x + K y = x + L y
8 lvecprop2d.2 φ x P y P x + F y = x + G y
9 lvecprop2d.3 φ x P y P x F y = x G y
10 lvecprop2d.4 φ x P y B x K y = x L y
11 1 2 3 4 5 6 7 8 9 10 lmodprop2d φ K LMod L LMod
12 5 6 8 9 drngpropd φ F DivRing G DivRing
13 11 12 anbi12d φ K LMod F DivRing L LMod G DivRing
14 3 islvec K LVec K LMod F DivRing
15 4 islvec L LVec L LMod G DivRing
16 13 14 15 3bitr4g φ K LVec L LVec