This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ φ → B = Base K
lvecpropd.2 ⊢ φ → B = Base L
lvecpropd.3 ⊢ φ ∧ x ∈ B ∧ y ∈ B → x + K y = x + L y
lvecpropd.4 ⊢ φ → F = Scalar ⁡ K
lvecpropd.5 ⊢ φ → F = Scalar ⁡ L
lvecpropd.6 ⊢ P = Base F
lvecpropd.7 ⊢ φ ∧ x ∈ P ∧ y ∈ B → x ⋅ K y = x ⋅ L y
Assertion lvecpropd ⊢ φ → K ∈ LVec ↔ L ∈ LVec

Proof

Step Hyp Ref Expression
1 lvecpropd.1 ⊢ φ → B = Base K
2 lvecpropd.2 ⊢ φ → B = Base L
3 lvecpropd.3 ⊢ φ ∧ x ∈ B ∧ y ∈ B → x + K y = x + L y
4 lvecpropd.4 ⊢ φ → F = Scalar ⁡ K
5 lvecpropd.5 ⊢ φ → F = Scalar ⁡ L
6 lvecpropd.6 ⊢ P = Base F
7 lvecpropd.7 ⊢ φ ∧ x ∈ P ∧ y ∈ B → x ⋅ K y = x ⋅ L y
8 1 2 3 4 5 6 7 lmodpropd ⊢ φ → K ∈ LMod ↔ L ∈ LMod
9 4 5 eqtr3d ⊢ φ → Scalar ⁡ K = Scalar ⁡ L
10 9 eleq1d ⊢ φ → Scalar ⁡ K ∈ DivRing ↔ Scalar ⁡ L ∈ DivRing
11 8 10 anbi12d ⊢ φ → K ∈ LMod ∧ Scalar ⁡ K ∈ DivRing ↔ L ∈ LMod ∧ Scalar ⁡ L ∈ DivRing
12 eqid ⊢ Scalar ⁡ K = Scalar ⁡ K
13 12 islvec ⊢ K ∈ LVec ↔ K ∈ LMod ∧ Scalar ⁡ K ∈ DivRing
14 eqid ⊢ Scalar ⁡ L = Scalar ⁡ L
15 14 islvec ⊢ L ∈ LVec ↔ L ∈ LMod ∧ Scalar ⁡ L ∈ DivRing
16 11 13 15 3bitr4g ⊢ φ → K ∈ LVec ↔ L ∈ LVec