Metamath Proof Explorer

Theorem lmhmpropd

Description: Module homomorphism depends only on the module attributes of structures. (Contributed by Mario Carneiro, 8-Oct-2015)

Ref Expression
Hypotheses lmhmpropd.a 
|- ( ph -> B = ( Base ` J ) )
lmhmpropd.b 
|- ( ph -> C = ( Base ` K ) )
lmhmpropd.c 
|- ( ph -> B = ( Base ` L ) )
lmhmpropd.d 
|- ( ph -> C = ( Base ` M ) )
lmhmpropd.1 
|- ( ph -> F = ( Scalar ` J ) )
lmhmpropd.2 
|- ( ph -> G = ( Scalar ` K ) )
lmhmpropd.3 
|- ( ph -> F = ( Scalar ` L ) )
lmhmpropd.4 
|- ( ph -> G = ( Scalar ` M ) )
lmhmpropd.p 
|- P = ( Base ` F )
lmhmpropd.q 
|- Q = ( Base ` G )
lmhmpropd.e 
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` J ) y ) = ( x ( +g ` L ) y ) )
lmhmpropd.f 
|- ( ( ph /\ ( x e. C /\ y e. C ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` M ) y ) )
lmhmpropd.g 
|- ( ( ph /\ ( x e. P /\ y e. B ) ) -> ( x ( .s ` J ) y ) = ( x ( .s ` L ) y ) )
lmhmpropd.h 
|- ( ( ph /\ ( x e. Q /\ y e. C ) ) -> ( x ( .s ` K ) y ) = ( x ( .s ` M ) y ) )
Assertion lmhmpropd 
|- ( ph -> ( J LMHom K ) = ( L LMHom M ) )

Proof

Step Hyp Ref Expression
1 lmhmpropd.a 
 |-  ( ph -> B = ( Base ` J ) )
2 lmhmpropd.b 
 |-  ( ph -> C = ( Base ` K ) )
3 lmhmpropd.c 
 |-  ( ph -> B = ( Base ` L ) )
4 lmhmpropd.d 
 |-  ( ph -> C = ( Base ` M ) )
5 lmhmpropd.1 
 |-  ( ph -> F = ( Scalar ` J ) )
6 lmhmpropd.2 
 |-  ( ph -> G = ( Scalar ` K ) )
7 lmhmpropd.3 
 |-  ( ph -> F = ( Scalar ` L ) )
8 lmhmpropd.4 
 |-  ( ph -> G = ( Scalar ` M ) )
9 lmhmpropd.p 
 |-  P = ( Base ` F )
10 lmhmpropd.q 
 |-  Q = ( Base ` G )
11 lmhmpropd.e 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` J ) y ) = ( x ( +g ` L ) y ) )
12 lmhmpropd.f 
 |-  ( ( ph /\ ( x e. C /\ y e. C ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` M ) y ) )
13 lmhmpropd.g 
 |-  ( ( ph /\ ( x e. P /\ y e. B ) ) -> ( x ( .s ` J ) y ) = ( x ( .s ` L ) y ) )
14 lmhmpropd.h 
 |-  ( ( ph /\ ( x e. Q /\ y e. C ) ) -> ( x ( .s ` K ) y ) = ( x ( .s ` M ) y ) )
15 1 3 11 5 7 9 13 lmodpropd 
 |-  ( ph -> ( J e. LMod <-> L e. LMod ) )
16 2 4 12 6 8 10 14 lmodpropd 
 |-  ( ph -> ( K e. LMod <-> M e. LMod ) )
17 15 16 anbi12d 
 |-  ( ph -> ( ( J e. LMod /\ K e. LMod ) <-> ( L e. LMod /\ M e. LMod ) ) )
18 13 oveqrspc2v 
 |-  ( ( ph /\ ( z e. P /\ w e. B ) ) -> ( z ( .s ` J ) w ) = ( z ( .s ` L ) w ) )
19 18 adantlr 
 |-  ( ( ( ph /\ ( f e. ( J GrpHom K ) /\ G = F ) ) /\ ( z e. P /\ w e. B ) ) -> ( z ( .s ` J ) w ) = ( z ( .s ` L ) w ) )
20 19 fveq2d 
 |-  ( ( ( ph /\ ( f e. ( J GrpHom K ) /\ G = F ) ) /\ ( z e. P /\ w e. B ) ) -> ( f ` ( z ( .s ` J ) w ) ) = ( f ` ( z ( .s ` L ) w ) ) )
21 simpll 
 |-  ( ( ( ph /\ ( f e. ( J GrpHom K ) /\ G = F ) ) /\ ( z e. P /\ w e. B ) ) -> ph )
22 simprl 
 |-  ( ( ( ph /\ ( f e. ( J GrpHom K ) /\ G = F ) ) /\ ( z e. P /\ w e. B ) ) -> z e. P )
23 simplrr 
 |-  ( ( ( ph /\ ( f e. ( J GrpHom K ) /\ G = F ) ) /\ ( z e. P /\ w e. B ) ) -> G = F )
24 23 fveq2d 
 |-  ( ( ( ph /\ ( f e. ( J GrpHom K ) /\ G = F ) ) /\ ( z e. P /\ w e. B ) ) -> ( Base ` G ) = ( Base ` F ) )
25 24 10 9 3eqtr4g 
 |-  ( ( ( ph /\ ( f e. ( J GrpHom K ) /\ G = F ) ) /\ ( z e. P /\ w e. B ) ) -> Q = P )
26 22 25 eleqtrrd 
 |-  ( ( ( ph /\ ( f e. ( J GrpHom K ) /\ G = F ) ) /\ ( z e. P /\ w e. B ) ) -> z e. Q )
27 simplrl 
 |-  ( ( ( ph /\ ( f e. ( J GrpHom K ) /\ G = F ) ) /\ ( z e. P /\ w e. B ) ) -> f e. ( J GrpHom K ) )
28 eqid 
 |-  ( Base ` J ) = ( Base ` J )
29 eqid 
 |-  ( Base ` K ) = ( Base ` K )
30 28 29 ghmf 
 |-  ( f e. ( J GrpHom K ) -> f : ( Base ` J ) --> ( Base ` K ) )
31 27 30 syl 
 |-  ( ( ( ph /\ ( f e. ( J GrpHom K ) /\ G = F ) ) /\ ( z e. P /\ w e. B ) ) -> f : ( Base ` J ) --> ( Base ` K ) )
32 simprr 
 |-  ( ( ( ph /\ ( f e. ( J GrpHom K ) /\ G = F ) ) /\ ( z e. P /\ w e. B ) ) -> w e. B )
33 21 1 syl 
 |-  ( ( ( ph /\ ( f e. ( J GrpHom K ) /\ G = F ) ) /\ ( z e. P /\ w e. B ) ) -> B = ( Base ` J ) )
34 32 33 eleqtrd 
 |-  ( ( ( ph /\ ( f e. ( J GrpHom K ) /\ G = F ) ) /\ ( z e. P /\ w e. B ) ) -> w e. ( Base ` J ) )
35 31 34 ffvelrnd 
 |-  ( ( ( ph /\ ( f e. ( J GrpHom K ) /\ G = F ) ) /\ ( z e. P /\ w e. B ) ) -> ( f ` w ) e. ( Base ` K ) )
36 21 2 syl 
 |-  ( ( ( ph /\ ( f e. ( J GrpHom K ) /\ G = F ) ) /\ ( z e. P /\ w e. B ) ) -> C = ( Base ` K ) )
37 35 36 eleqtrrd 
 |-  ( ( ( ph /\ ( f e. ( J GrpHom K ) /\ G = F ) ) /\ ( z e. P /\ w e. B ) ) -> ( f ` w ) e. C )
38 14 oveqrspc2v 
 |-  ( ( ph /\ ( z e. Q /\ ( f ` w ) e. C ) ) -> ( z ( .s ` K ) ( f ` w ) ) = ( z ( .s ` M ) ( f ` w ) ) )
39 21 26 37 38 syl12anc 
 |-  ( ( ( ph /\ ( f e. ( J GrpHom K ) /\ G = F ) ) /\ ( z e. P /\ w e. B ) ) -> ( z ( .s ` K ) ( f ` w ) ) = ( z ( .s ` M ) ( f ` w ) ) )
40 20 39 eqeq12d 
 |-  ( ( ( ph /\ ( f e. ( J GrpHom K ) /\ G = F ) ) /\ ( z e. P /\ w e. B ) ) -> ( ( f ` ( z ( .s ` J ) w ) ) = ( z ( .s ` K ) ( f ` w ) ) <-> ( f ` ( z ( .s ` L ) w ) ) = ( z ( .s ` M ) ( f ` w ) ) ) )
41 40 2ralbidva 
 |-  ( ( ph /\ ( f e. ( J GrpHom K ) /\ G = F ) ) -> ( A. z e. P A. w e. B ( f ` ( z ( .s ` J ) w ) ) = ( z ( .s ` K ) ( f ` w ) ) <-> A. z e. P A. w e. B ( f ` ( z ( .s ` L ) w ) ) = ( z ( .s ` M ) ( f ` w ) ) ) )
42 41 pm5.32da 
 |-  ( ph -> ( ( ( f e. ( J GrpHom K ) /\ G = F ) /\ A. z e. P A. w e. B ( f ` ( z ( .s ` J ) w ) ) = ( z ( .s ` K ) ( f ` w ) ) ) <-> ( ( f e. ( J GrpHom K ) /\ G = F ) /\ A. z e. P A. w e. B ( f ` ( z ( .s ` L ) w ) ) = ( z ( .s ` M ) ( f ` w ) ) ) ) )
43 df-3an 
 |-  ( ( f e. ( J GrpHom K ) /\ G = F /\ A. z e. P A. w e. B ( f ` ( z ( .s ` J ) w ) ) = ( z ( .s ` K ) ( f ` w ) ) ) <-> ( ( f e. ( J GrpHom K ) /\ G = F ) /\ A. z e. P A. w e. B ( f ` ( z ( .s ` J ) w ) ) = ( z ( .s ` K ) ( f ` w ) ) ) )
44 df-3an 
 |-  ( ( f e. ( J GrpHom K ) /\ G = F /\ A. z e. P A. w e. B ( f ` ( z ( .s ` L ) w ) ) = ( z ( .s ` M ) ( f ` w ) ) ) <-> ( ( f e. ( J GrpHom K ) /\ G = F ) /\ A. z e. P A. w e. B ( f ` ( z ( .s ` L ) w ) ) = ( z ( .s ` M ) ( f ` w ) ) ) )
45 42 43 44 3bitr4g 
 |-  ( ph -> ( ( f e. ( J GrpHom K ) /\ G = F /\ A. z e. P A. w e. B ( f ` ( z ( .s ` J ) w ) ) = ( z ( .s ` K ) ( f ` w ) ) ) <-> ( f e. ( J GrpHom K ) /\ G = F /\ A. z e. P A. w e. B ( f ` ( z ( .s ` L ) w ) ) = ( z ( .s ` M ) ( f ` w ) ) ) ) )
46 6 5 eqeq12d 
 |-  ( ph -> ( G = F <-> ( Scalar ` K ) = ( Scalar ` J ) ) )
47 5 fveq2d 
 |-  ( ph -> ( Base ` F ) = ( Base ` ( Scalar ` J ) ) )
48 9 47 syl5eq 
 |-  ( ph -> P = ( Base ` ( Scalar ` J ) ) )
49 1 raleqdv 
 |-  ( ph -> ( A. w e. B ( f ` ( z ( .s ` J ) w ) ) = ( z ( .s ` K ) ( f ` w ) ) <-> A. w e. ( Base ` J ) ( f ` ( z ( .s ` J ) w ) ) = ( z ( .s ` K ) ( f ` w ) ) ) )
50 48 49 raleqbidv 
 |-  ( ph -> ( A. z e. P A. w e. B ( f ` ( z ( .s ` J ) w ) ) = ( z ( .s ` K ) ( f ` w ) ) <-> A. z e. ( Base ` ( Scalar ` J ) ) A. w e. ( Base ` J ) ( f ` ( z ( .s ` J ) w ) ) = ( z ( .s ` K ) ( f ` w ) ) ) )
51 46 50 3anbi23d 
 |-  ( ph -> ( ( f e. ( J GrpHom K ) /\ G = F /\ A. z e. P A. w e. B ( f ` ( z ( .s ` J ) w ) ) = ( z ( .s ` K ) ( f ` w ) ) ) <-> ( f e. ( J GrpHom K ) /\ ( Scalar ` K ) = ( Scalar ` J ) /\ A. z e. ( Base ` ( Scalar ` J ) ) A. w e. ( Base ` J ) ( f ` ( z ( .s ` J ) w ) ) = ( z ( .s ` K ) ( f ` w ) ) ) ) )
52 1 2 3 4 11 12 ghmpropd 
 |-  ( ph -> ( J GrpHom K ) = ( L GrpHom M ) )
53 52 eleq2d 
 |-  ( ph -> ( f e. ( J GrpHom K ) <-> f e. ( L GrpHom M ) ) )
54 8 7 eqeq12d 
 |-  ( ph -> ( G = F <-> ( Scalar ` M ) = ( Scalar ` L ) ) )
55 7 fveq2d 
 |-  ( ph -> ( Base ` F ) = ( Base ` ( Scalar ` L ) ) )
56 9 55 syl5eq 
 |-  ( ph -> P = ( Base ` ( Scalar ` L ) ) )
57 3 raleqdv 
 |-  ( ph -> ( A. w e. B ( f ` ( z ( .s ` L ) w ) ) = ( z ( .s ` M ) ( f ` w ) ) <-> A. w e. ( Base ` L ) ( f ` ( z ( .s ` L ) w ) ) = ( z ( .s ` M ) ( f ` w ) ) ) )
58 56 57 raleqbidv 
 |-  ( ph -> ( A. z e. P A. w e. B ( f ` ( z ( .s ` L ) w ) ) = ( z ( .s ` M ) ( f ` w ) ) <-> A. z e. ( Base ` ( Scalar ` L ) ) A. w e. ( Base ` L ) ( f ` ( z ( .s ` L ) w ) ) = ( z ( .s ` M ) ( f ` w ) ) ) )
59 53 54 58 3anbi123d 
 |-  ( ph -> ( ( f e. ( J GrpHom K ) /\ G = F /\ A. z e. P A. w e. B ( f ` ( z ( .s ` L ) w ) ) = ( z ( .s ` M ) ( f ` w ) ) ) <-> ( f e. ( L GrpHom M ) /\ ( Scalar ` M ) = ( Scalar ` L ) /\ A. z e. ( Base ` ( Scalar ` L ) ) A. w e. ( Base ` L ) ( f ` ( z ( .s ` L ) w ) ) = ( z ( .s ` M ) ( f ` w ) ) ) ) )
60 45 51 59 3bitr3d 
 |-  ( ph -> ( ( f e. ( J GrpHom K ) /\ ( Scalar ` K ) = ( Scalar ` J ) /\ A. z e. ( Base ` ( Scalar ` J ) ) A. w e. ( Base ` J ) ( f ` ( z ( .s ` J ) w ) ) = ( z ( .s ` K ) ( f ` w ) ) ) <-> ( f e. ( L GrpHom M ) /\ ( Scalar ` M ) = ( Scalar ` L ) /\ A. z e. ( Base ` ( Scalar ` L ) ) A. w e. ( Base ` L ) ( f ` ( z ( .s ` L ) w ) ) = ( z ( .s ` M ) ( f ` w ) ) ) ) )
61 17 60 anbi12d 
 |-  ( ph -> ( ( ( J e. LMod /\ K e. LMod ) /\ ( f e. ( J GrpHom K ) /\ ( Scalar ` K ) = ( Scalar ` J ) /\ A. z e. ( Base ` ( Scalar ` J ) ) A. w e. ( Base ` J ) ( f ` ( z ( .s ` J ) w ) ) = ( z ( .s ` K ) ( f ` w ) ) ) ) <-> ( ( L e. LMod /\ M e. LMod ) /\ ( f e. ( L GrpHom M ) /\ ( Scalar ` M ) = ( Scalar ` L ) /\ A. z e. ( Base ` ( Scalar ` L ) ) A. w e. ( Base ` L ) ( f ` ( z ( .s ` L ) w ) ) = ( z ( .s ` M ) ( f ` w ) ) ) ) ) )
62 eqid 
 |-  ( Scalar ` J ) = ( Scalar ` J )
63 eqid 
 |-  ( Scalar ` K ) = ( Scalar ` K )
64 eqid 
 |-  ( Base ` ( Scalar ` J ) ) = ( Base ` ( Scalar ` J ) )
65 eqid 
 |-  ( .s ` J ) = ( .s ` J )
66 eqid 
 |-  ( .s ` K ) = ( .s ` K )
67 62 63 64 28 65 66 islmhm 
 |-  ( f e. ( J LMHom K ) <-> ( ( J e. LMod /\ K e. LMod ) /\ ( f e. ( J GrpHom K ) /\ ( Scalar ` K ) = ( Scalar ` J ) /\ A. z e. ( Base ` ( Scalar ` J ) ) A. w e. ( Base ` J ) ( f ` ( z ( .s ` J ) w ) ) = ( z ( .s ` K ) ( f ` w ) ) ) ) )
68 eqid 
 |-  ( Scalar ` L ) = ( Scalar ` L )
69 eqid 
 |-  ( Scalar ` M ) = ( Scalar ` M )
70 eqid 
 |-  ( Base ` ( Scalar ` L ) ) = ( Base ` ( Scalar ` L ) )
71 eqid 
 |-  ( Base ` L ) = ( Base ` L )
72 eqid 
 |-  ( .s ` L ) = ( .s ` L )
73 eqid 
 |-  ( .s ` M ) = ( .s ` M )
74 68 69 70 71 72 73 islmhm 
 |-  ( f e. ( L LMHom M ) <-> ( ( L e. LMod /\ M e. LMod ) /\ ( f e. ( L GrpHom M ) /\ ( Scalar ` M ) = ( Scalar ` L ) /\ A. z e. ( Base ` ( Scalar ` L ) ) A. w e. ( Base ` L ) ( f ` ( z ( .s ` L ) w ) ) = ( z ( .s ` M ) ( f ` w ) ) ) ) )
75 61 67 74 3bitr4g 
 |-  ( ph -> ( f e. ( J LMHom K ) <-> f e. ( L LMHom M ) ) )
76 75 eqrdv 
 |-  ( ph -> ( J LMHom K ) = ( L LMHom M ) )