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 ) )