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