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
|- ( ph -> B = ( Base ` K ) )
lvecprop2d.b2
|- ( ph -> B = ( Base ` L ) )
lvecprop2d.f
|- F = ( Scalar ` K )
lvecprop2d.g
|- G = ( Scalar ` L )
lvecprop2d.p1
|- ( ph -> P = ( Base ` F ) )
lvecprop2d.p2
|- ( ph -> P = ( Base ` G ) )
lvecprop2d.1
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
lvecprop2d.2
|- ( ( ph /\ ( x e. P /\ y e. P ) ) -> ( x ( +g ` F ) y ) = ( x ( +g ` G ) y ) )
lvecprop2d.3
|- ( ( ph /\ ( x e. P /\ y e. P ) ) -> ( x ( .r ` F ) y ) = ( x ( .r ` G ) y ) )
lvecprop2d.4
|- ( ( ph /\ ( x e. P /\ y e. B ) ) -> ( x ( .s ` K ) y ) = ( x ( .s ` L ) y ) )
Assertion lvecprop2d
|- ( ph -> ( K e. LVec <-> L e. LVec ) )

Proof

Step Hyp Ref Expression
1 lvecprop2d.b1
 |-  ( ph -> B = ( Base ` K ) )
2 lvecprop2d.b2
 |-  ( ph -> B = ( Base ` L ) )
3 lvecprop2d.f
 |-  F = ( Scalar ` K )
4 lvecprop2d.g
 |-  G = ( Scalar ` L )
5 lvecprop2d.p1
 |-  ( ph -> P = ( Base ` F ) )
6 lvecprop2d.p2
 |-  ( ph -> P = ( Base ` G ) )
7 lvecprop2d.1
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
8 lvecprop2d.2
 |-  ( ( ph /\ ( x e. P /\ y e. P ) ) -> ( x ( +g ` F ) y ) = ( x ( +g ` G ) y ) )
9 lvecprop2d.3
 |-  ( ( ph /\ ( x e. P /\ y e. P ) ) -> ( x ( .r ` F ) y ) = ( x ( .r ` G ) y ) )
10 lvecprop2d.4
 |-  ( ( ph /\ ( x e. P /\ y e. B ) ) -> ( x ( .s ` K ) y ) = ( x ( .s ` L ) y ) )
11 1 2 3 4 5 6 7 8 9 10 lmodprop2d
 |-  ( ph -> ( K e. LMod <-> L e. LMod ) )
12 5 6 8 9 drngpropd
 |-  ( ph -> ( F e. DivRing <-> G e. DivRing ) )
13 11 12 anbi12d
 |-  ( ph -> ( ( K e. LMod /\ F e. DivRing ) <-> ( L e. LMod /\ G e. DivRing ) ) )
14 3 islvec
 |-  ( K e. LVec <-> ( K e. LMod /\ F e. DivRing ) )
15 4 islvec
 |-  ( L e. LVec <-> ( L e. LMod /\ G e. DivRing ) )
16 13 14 15 3bitr4g
 |-  ( ph -> ( K e. LVec <-> L e. LVec ) )