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