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

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 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
lvecprop2d.b2 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
lvecprop2d.f ⊢ 𝐹 = ( Scalar ‘ 𝐾 )
lvecprop2d.g ⊢ 𝐺 = ( Scalar ‘ 𝐿 )
lvecprop2d.p1 ⊢ ( 𝜑 → 𝑃 = ( Base ‘ 𝐹 ) )
lvecprop2d.p2 ⊢ ( 𝜑 → 𝑃 = ( Base ‘ 𝐺 ) )
lvecprop2d.1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
lvecprop2d.2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ) → ( 𝑥 ( +g ‘ 𝐹 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) )
lvecprop2d.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ) → ( 𝑥 ( .r ‘ 𝐹 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝐺 ) 𝑦 ) )
lvecprop2d.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( ·𝑠 ‘ 𝐿 ) 𝑦 ) )
Assertion lvecprop2d ( 𝜑 → ( 𝐾 ∈ LVec ↔ 𝐿 ∈ LVec ) )

Proof

Step Hyp Ref Expression
1 lvecprop2d.b1 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
2 lvecprop2d.b2 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
3 lvecprop2d.f ⊢ 𝐹 = ( Scalar ‘ 𝐾 )
4 lvecprop2d.g ⊢ 𝐺 = ( Scalar ‘ 𝐿 )
5 lvecprop2d.p1 ⊢ ( 𝜑 → 𝑃 = ( Base ‘ 𝐹 ) )
6 lvecprop2d.p2 ⊢ ( 𝜑 → 𝑃 = ( Base ‘ 𝐺 ) )
7 lvecprop2d.1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
8 lvecprop2d.2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ) → ( 𝑥 ( +g ‘ 𝐹 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) )
9 lvecprop2d.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ) → ( 𝑥 ( .r ‘ 𝐹 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝐺 ) 𝑦 ) )
10 lvecprop2d.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( ·𝑠 ‘ 𝐿 ) 𝑦 ) )
11 1 2 3 4 5 6 7 8 9 10 lmodprop2d ⊢ ( 𝜑 → ( 𝐾 ∈ LMod ↔ 𝐿 ∈ LMod ) )
12 5 6 8 9 drngpropd ⊢ ( 𝜑 → ( 𝐹 ∈ DivRing ↔ 𝐺 ∈ DivRing ) )
13 11 12 anbi12d ⊢ ( 𝜑 → ( ( 𝐾 ∈ LMod ∧ 𝐹 ∈ DivRing ) ↔ ( 𝐿 ∈ LMod ∧ 𝐺 ∈ DivRing ) ) )
14 3 islvec ⊢ ( 𝐾 ∈ LVec ↔ ( 𝐾 ∈ LMod ∧ 𝐹 ∈ DivRing ) )
15 4 islvec ⊢ ( 𝐿 ∈ LVec ↔ ( 𝐿 ∈ LMod ∧ 𝐺 ∈ DivRing ) )
16 13 14 15 3bitr4g ⊢ ( 𝜑 → ( 𝐾 ∈ LVec ↔ 𝐿 ∈ LVec ) )