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