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 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
lvecpropd.2 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
lvecpropd.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
lvecpropd.4 ⊢ ( 𝜑 → 𝐹 = ( Scalar ‘ 𝐾 ) )
lvecpropd.5 ⊢ ( 𝜑 → 𝐹 = ( Scalar ‘ 𝐿 ) )
lvecpropd.6 ⊢ 𝑃 = ( Base ‘ 𝐹 )
lvecpropd.7 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( ·𝑠 ‘ 𝐿 ) 𝑦 ) )
Assertion lvecpropd ( 𝜑 → ( 𝐾 ∈ LVec ↔ 𝐿 ∈ LVec ) )

Proof

Step Hyp Ref Expression
1 lvecpropd.1 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
2 lvecpropd.2 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
3 lvecpropd.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
4 lvecpropd.4 ⊢ ( 𝜑 → 𝐹 = ( Scalar ‘ 𝐾 ) )
5 lvecpropd.5 ⊢ ( 𝜑 → 𝐹 = ( Scalar ‘ 𝐿 ) )
6 lvecpropd.6 ⊢ 𝑃 = ( Base ‘ 𝐹 )
7 lvecpropd.7 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( ·𝑠 ‘ 𝐿 ) 𝑦 ) )
8 1 2 3 4 5 6 7 lmodpropd ⊢ ( 𝜑 → ( 𝐾 ∈ LMod ↔ 𝐿 ∈ LMod ) )
9 4 5 eqtr3d ⊢ ( 𝜑 → ( Scalar ‘ 𝐾 ) = ( Scalar ‘ 𝐿 ) )
10 9 eleq1d ⊢ ( 𝜑 → ( ( Scalar ‘ 𝐾 ) ∈ DivRing ↔ ( Scalar ‘ 𝐿 ) ∈ DivRing ) )
11 8 10 anbi12d ⊢ ( 𝜑 → ( ( 𝐾 ∈ LMod ∧ ( Scalar ‘ 𝐾 ) ∈ DivRing ) ↔ ( 𝐿 ∈ LMod ∧ ( Scalar ‘ 𝐿 ) ∈ DivRing ) ) )
12 eqid ⊢ ( Scalar ‘ 𝐾 ) = ( Scalar ‘ 𝐾 )
13 12 islvec ⊢ ( 𝐾 ∈ LVec ↔ ( 𝐾 ∈ LMod ∧ ( Scalar ‘ 𝐾 ) ∈ DivRing ) )
14 eqid ⊢ ( Scalar ‘ 𝐿 ) = ( Scalar ‘ 𝐿 )
15 14 islvec ⊢ ( 𝐿 ∈ LVec ↔ ( 𝐿 ∈ LMod ∧ ( Scalar ‘ 𝐿 ) ∈ DivRing ) )
16 11 13 15 3bitr4g ⊢ ( 𝜑 → ( 𝐾 ∈ LVec ↔ 𝐿 ∈ LVec ) )