Metamath Proof Explorer

Theorem lmodpropd

Description: If two structures have the same components (properties), one is a left module iff the other one is. (Contributed by Mario Carneiro, 8-Feb-2015) (Revised by Mario Carneiro, 27-Jun-2015)

Ref Expression
Hypotheses lmodpropd.1 
|- ( ph -> B = ( Base ` K ) )
lmodpropd.2 
|- ( ph -> B = ( Base ` L ) )
lmodpropd.3 
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
lmodpropd.4 
|- ( ph -> F = ( Scalar ` K ) )
lmodpropd.5 
|- ( ph -> F = ( Scalar ` L ) )
lmodpropd.6 
|- P = ( Base ` F )
lmodpropd.7 
|- ( ( ph /\ ( x e. P /\ y e. B ) ) -> ( x ( .s ` K ) y ) = ( x ( .s ` L ) y ) )
Assertion lmodpropd 
|- ( ph -> ( K e. LMod <-> L e. LMod ) )

Proof

Step Hyp Ref Expression
1 lmodpropd.1 
 |-  ( ph -> B = ( Base ` K ) )
2 lmodpropd.2 
 |-  ( ph -> B = ( Base ` L ) )
3 lmodpropd.3 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
4 lmodpropd.4 
 |-  ( ph -> F = ( Scalar ` K ) )
5 lmodpropd.5 
 |-  ( ph -> F = ( Scalar ` L ) )
6 lmodpropd.6 
 |-  P = ( Base ` F )
7 lmodpropd.7 
 |-  ( ( ph /\ ( x e. P /\ y e. B ) ) -> ( x ( .s ` K ) y ) = ( x ( .s ` L ) y ) )
8 eqid 
 |-  ( Scalar ` K ) = ( Scalar ` K )
9 eqid 
 |-  ( Scalar ` L ) = ( Scalar ` L )
10 4 fveq2d 
 |-  ( ph -> ( Base ` F ) = ( Base ` ( Scalar ` K ) ) )
11 6 10 syl5eq 
 |-  ( ph -> P = ( Base ` ( Scalar ` K ) ) )
12 5 fveq2d 
 |-  ( ph -> ( Base ` F ) = ( Base ` ( Scalar ` L ) ) )
13 6 12 syl5eq 
 |-  ( ph -> P = ( Base ` ( Scalar ` L ) ) )
14 4 5 eqtr3d 
 |-  ( ph -> ( Scalar ` K ) = ( Scalar ` L ) )
15 14 adantr 
 |-  ( ( ph /\ ( x e. P /\ y e. P ) ) -> ( Scalar ` K ) = ( Scalar ` L ) )
16 15 fveq2d 
 |-  ( ( ph /\ ( x e. P /\ y e. P ) ) -> ( +g ` ( Scalar ` K ) ) = ( +g ` ( Scalar ` L ) ) )
17 16 oveqd 
 |-  ( ( ph /\ ( x e. P /\ y e. P ) ) -> ( x ( +g ` ( Scalar ` K ) ) y ) = ( x ( +g ` ( Scalar ` L ) ) y ) )
18 15 fveq2d 
 |-  ( ( ph /\ ( x e. P /\ y e. P ) ) -> ( .r ` ( Scalar ` K ) ) = ( .r ` ( Scalar ` L ) ) )
19 18 oveqd 
 |-  ( ( ph /\ ( x e. P /\ y e. P ) ) -> ( x ( .r ` ( Scalar ` K ) ) y ) = ( x ( .r ` ( Scalar ` L ) ) y ) )
20 1 2 8 9 11 13 3 17 19 7 lmodprop2d 
 |-  ( ph -> ( K e. LMod <-> L e. LMod ) )