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 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐽 ) )
lmhmpropd.b ⊢ ( 𝜑 → 𝐶 = ( Base ‘ 𝐾 ) )
lmhmpropd.c ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
lmhmpropd.d ⊢ ( 𝜑 → 𝐶 = ( Base ‘ 𝑀 ) )
lmhmpropd.1 ⊢ ( 𝜑 → 𝐹 = ( Scalar ‘ 𝐽 ) )
lmhmpropd.2 ⊢ ( 𝜑 → 𝐺 = ( Scalar ‘ 𝐾 ) )
lmhmpropd.3 ⊢ ( 𝜑 → 𝐹 = ( Scalar ‘ 𝐿 ) )
lmhmpropd.4 ⊢ ( 𝜑 → 𝐺 = ( Scalar ‘ 𝑀 ) )
lmhmpropd.p ⊢ 𝑃 = ( Base ‘ 𝐹 )
lmhmpropd.q ⊢ 𝑄 = ( Base ‘ 𝐺 )
lmhmpropd.e ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐽 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
lmhmpropd.f ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) )
lmhmpropd.g ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐽 ) 𝑦 ) = ( 𝑥 ( ·𝑠 ‘ 𝐿 ) 𝑦 ) )
lmhmpropd.h ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑄 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) )
Assertion lmhmpropd ( 𝜑 → ( 𝐽 LMHom 𝐾 ) = ( 𝐿 LMHom 𝑀 ) )

Proof

Step Hyp Ref Expression
1 lmhmpropd.a ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐽 ) )
2 lmhmpropd.b ⊢ ( 𝜑 → 𝐶 = ( Base ‘ 𝐾 ) )
3 lmhmpropd.c ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
4 lmhmpropd.d ⊢ ( 𝜑 → 𝐶 = ( Base ‘ 𝑀 ) )
5 lmhmpropd.1 ⊢ ( 𝜑 → 𝐹 = ( Scalar ‘ 𝐽 ) )
6 lmhmpropd.2 ⊢ ( 𝜑 → 𝐺 = ( Scalar ‘ 𝐾 ) )
7 lmhmpropd.3 ⊢ ( 𝜑 → 𝐹 = ( Scalar ‘ 𝐿 ) )
8 lmhmpropd.4 ⊢ ( 𝜑 → 𝐺 = ( Scalar ‘ 𝑀 ) )
9 lmhmpropd.p ⊢ 𝑃 = ( Base ‘ 𝐹 )
10 lmhmpropd.q ⊢ 𝑄 = ( Base ‘ 𝐺 )
11 lmhmpropd.e ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐽 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
12 lmhmpropd.f ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) )
13 lmhmpropd.g ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐽 ) 𝑦 ) = ( 𝑥 ( ·𝑠 ‘ 𝐿 ) 𝑦 ) )
14 lmhmpropd.h ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑄 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) )
15 1 3 11 5 7 9 13 lmodpropd ⊢ ( 𝜑 → ( 𝐽 ∈ LMod ↔ 𝐿 ∈ LMod ) )
16 2 4 12 6 8 10 14 lmodpropd ⊢ ( 𝜑 → ( 𝐾 ∈ LMod ↔ 𝑀 ∈ LMod ) )
17 15 16 anbi12d ⊢ ( 𝜑 → ( ( 𝐽 ∈ LMod ∧ 𝐾 ∈ LMod ) ↔ ( 𝐿 ∈ LMod ∧ 𝑀 ∈ LMod ) ) )
18 13 oveqrspc2v ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑃 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑧 ( ·𝑠 ‘ 𝐽 ) 𝑤 ) = ( 𝑧 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) )
19 18 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐽 GrpHom 𝐾 ) ∧ 𝐺 = 𝐹 ) ) ∧ ( 𝑧 ∈ 𝑃 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑧 ( ·𝑠 ‘ 𝐽 ) 𝑤 ) = ( 𝑧 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) )
20 19 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐽 GrpHom 𝐾 ) ∧ 𝐺 = 𝐹 ) ) ∧ ( 𝑧 ∈ 𝑃 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑓 ‘ ( 𝑧 ( ·𝑠 ‘ 𝐽 ) 𝑤 ) ) = ( 𝑓 ‘ ( 𝑧 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) )
21 simpll ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐽 GrpHom 𝐾 ) ∧ 𝐺 = 𝐹 ) ) ∧ ( 𝑧 ∈ 𝑃 ∧ 𝑤 ∈ 𝐵 ) ) → 𝜑 )
22 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐽 GrpHom 𝐾 ) ∧ 𝐺 = 𝐹 ) ) ∧ ( 𝑧 ∈ 𝑃 ∧ 𝑤 ∈ 𝐵 ) ) → 𝑧 ∈ 𝑃 )
23 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐽 GrpHom 𝐾 ) ∧ 𝐺 = 𝐹 ) ) ∧ ( 𝑧 ∈ 𝑃 ∧ 𝑤 ∈ 𝐵 ) ) → 𝐺 = 𝐹 )
24 23 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐽 GrpHom 𝐾 ) ∧ 𝐺 = 𝐹 ) ) ∧ ( 𝑧 ∈ 𝑃 ∧ 𝑤 ∈ 𝐵 ) ) → ( Base ‘ 𝐺 ) = ( Base ‘ 𝐹 ) )
25 24 10 9 3eqtr4g ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐽 GrpHom 𝐾 ) ∧ 𝐺 = 𝐹 ) ) ∧ ( 𝑧 ∈ 𝑃 ∧ 𝑤 ∈ 𝐵 ) ) → 𝑄 = 𝑃 )
26 22 25 eleqtrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐽 GrpHom 𝐾 ) ∧ 𝐺 = 𝐹 ) ) ∧ ( 𝑧 ∈ 𝑃 ∧ 𝑤 ∈ 𝐵 ) ) → 𝑧 ∈ 𝑄 )
27 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐽 GrpHom 𝐾 ) ∧ 𝐺 = 𝐹 ) ) ∧ ( 𝑧 ∈ 𝑃 ∧ 𝑤 ∈ 𝐵 ) ) → 𝑓 ∈ ( 𝐽 GrpHom 𝐾 ) )
28 eqid ⊢ ( Base ‘ 𝐽 ) = ( Base ‘ 𝐽 )
29 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
30 28 29 ghmf ⊢ ( 𝑓 ∈ ( 𝐽 GrpHom 𝐾 ) → 𝑓 : ( Base ‘ 𝐽 ) ⟶ ( Base ‘ 𝐾 ) )
31 27 30 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐽 GrpHom 𝐾 ) ∧ 𝐺 = 𝐹 ) ) ∧ ( 𝑧 ∈ 𝑃 ∧ 𝑤 ∈ 𝐵 ) ) → 𝑓 : ( Base ‘ 𝐽 ) ⟶ ( Base ‘ 𝐾 ) )
32 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐽 GrpHom 𝐾 ) ∧ 𝐺 = 𝐹 ) ) ∧ ( 𝑧 ∈ 𝑃 ∧ 𝑤 ∈ 𝐵 ) ) → 𝑤 ∈ 𝐵 )
33 21 1 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐽 GrpHom 𝐾 ) ∧ 𝐺 = 𝐹 ) ) ∧ ( 𝑧 ∈ 𝑃 ∧ 𝑤 ∈ 𝐵 ) ) → 𝐵 = ( Base ‘ 𝐽 ) )
34 32 33 eleqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐽 GrpHom 𝐾 ) ∧ 𝐺 = 𝐹 ) ) ∧ ( 𝑧 ∈ 𝑃 ∧ 𝑤 ∈ 𝐵 ) ) → 𝑤 ∈ ( Base ‘ 𝐽 ) )
35 31 34 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐽 GrpHom 𝐾 ) ∧ 𝐺 = 𝐹 ) ) ∧ ( 𝑧 ∈ 𝑃 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑓 ‘ 𝑤 ) ∈ ( Base ‘ 𝐾 ) )
36 21 2 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐽 GrpHom 𝐾 ) ∧ 𝐺 = 𝐹 ) ) ∧ ( 𝑧 ∈ 𝑃 ∧ 𝑤 ∈ 𝐵 ) ) → 𝐶 = ( Base ‘ 𝐾 ) )
37 35 36 eleqtrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐽 GrpHom 𝐾 ) ∧ 𝐺 = 𝐹 ) ) ∧ ( 𝑧 ∈ 𝑃 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑓 ‘ 𝑤 ) ∈ 𝐶 )
38 14 oveqrspc2v ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑄 ∧ ( 𝑓 ‘ 𝑤 ) ∈ 𝐶 ) ) → ( 𝑧 ( ·𝑠 ‘ 𝐾 ) ( 𝑓 ‘ 𝑤 ) ) = ( 𝑧 ( ·𝑠 ‘ 𝑀 ) ( 𝑓 ‘ 𝑤 ) ) )
39 21 26 37 38 syl12anc ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐽 GrpHom 𝐾 ) ∧ 𝐺 = 𝐹 ) ) ∧ ( 𝑧 ∈ 𝑃 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑧 ( ·𝑠 ‘ 𝐾 ) ( 𝑓 ‘ 𝑤 ) ) = ( 𝑧 ( ·𝑠 ‘ 𝑀 ) ( 𝑓 ‘ 𝑤 ) ) )
40 20 39 eqeq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐽 GrpHom 𝐾 ) ∧ 𝐺 = 𝐹 ) ) ∧ ( 𝑧 ∈ 𝑃 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 𝑓 ‘ ( 𝑧 ( ·𝑠 ‘ 𝐽 ) 𝑤 ) ) = ( 𝑧 ( ·𝑠 ‘ 𝐾 ) ( 𝑓 ‘ 𝑤 ) ) ↔ ( 𝑓 ‘ ( 𝑧 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) = ( 𝑧 ( ·𝑠 ‘ 𝑀 ) ( 𝑓 ‘ 𝑤 ) ) ) )
41 40 2ralbidva ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐽 GrpHom 𝐾 ) ∧ 𝐺 = 𝐹 ) ) → ( ∀ 𝑧 ∈ 𝑃 ∀ 𝑤 ∈ 𝐵 ( 𝑓 ‘ ( 𝑧 ( ·𝑠 ‘ 𝐽 ) 𝑤 ) ) = ( 𝑧 ( ·𝑠 ‘ 𝐾 ) ( 𝑓 ‘ 𝑤 ) ) ↔ ∀ 𝑧 ∈ 𝑃 ∀ 𝑤 ∈ 𝐵 ( 𝑓 ‘ ( 𝑧 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) = ( 𝑧 ( ·𝑠 ‘ 𝑀 ) ( 𝑓 ‘ 𝑤 ) ) ) )
42 41 pm5.32da ⊢ ( 𝜑 → ( ( ( 𝑓 ∈ ( 𝐽 GrpHom 𝐾 ) ∧ 𝐺 = 𝐹 ) ∧ ∀ 𝑧 ∈ 𝑃 ∀ 𝑤 ∈ 𝐵 ( 𝑓 ‘ ( 𝑧 ( ·𝑠 ‘ 𝐽 ) 𝑤 ) ) = ( 𝑧 ( ·𝑠 ‘ 𝐾 ) ( 𝑓 ‘ 𝑤 ) ) ) ↔ ( ( 𝑓 ∈ ( 𝐽 GrpHom 𝐾 ) ∧ 𝐺 = 𝐹 ) ∧ ∀ 𝑧 ∈ 𝑃 ∀ 𝑤 ∈ 𝐵 ( 𝑓 ‘ ( 𝑧 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) = ( 𝑧 ( ·𝑠 ‘ 𝑀 ) ( 𝑓 ‘ 𝑤 ) ) ) ) )
43 df-3an ⊢ ( ( 𝑓 ∈ ( 𝐽 GrpHom 𝐾 ) ∧ 𝐺 = 𝐹 ∧ ∀ 𝑧 ∈ 𝑃 ∀ 𝑤 ∈ 𝐵 ( 𝑓 ‘ ( 𝑧 ( ·𝑠 ‘ 𝐽 ) 𝑤 ) ) = ( 𝑧 ( ·𝑠 ‘ 𝐾 ) ( 𝑓 ‘ 𝑤 ) ) ) ↔ ( ( 𝑓 ∈ ( 𝐽 GrpHom 𝐾 ) ∧ 𝐺 = 𝐹 ) ∧ ∀ 𝑧 ∈ 𝑃 ∀ 𝑤 ∈ 𝐵 ( 𝑓 ‘ ( 𝑧 ( ·𝑠 ‘ 𝐽 ) 𝑤 ) ) = ( 𝑧 ( ·𝑠 ‘ 𝐾 ) ( 𝑓 ‘ 𝑤 ) ) ) )
44 df-3an ⊢ ( ( 𝑓 ∈ ( 𝐽 GrpHom 𝐾 ) ∧ 𝐺 = 𝐹 ∧ ∀ 𝑧 ∈ 𝑃 ∀ 𝑤 ∈ 𝐵 ( 𝑓 ‘ ( 𝑧 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) = ( 𝑧 ( ·𝑠 ‘ 𝑀 ) ( 𝑓 ‘ 𝑤 ) ) ) ↔ ( ( 𝑓 ∈ ( 𝐽 GrpHom 𝐾 ) ∧ 𝐺 = 𝐹 ) ∧ ∀ 𝑧 ∈ 𝑃 ∀ 𝑤 ∈ 𝐵 ( 𝑓 ‘ ( 𝑧 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) = ( 𝑧 ( ·𝑠 ‘ 𝑀 ) ( 𝑓 ‘ 𝑤 ) ) ) )
45 42 43 44 3bitr4g ⊢ ( 𝜑 → ( ( 𝑓 ∈ ( 𝐽 GrpHom 𝐾 ) ∧ 𝐺 = 𝐹 ∧ ∀ 𝑧 ∈ 𝑃 ∀ 𝑤 ∈ 𝐵 ( 𝑓 ‘ ( 𝑧 ( ·𝑠 ‘ 𝐽 ) 𝑤 ) ) = ( 𝑧 ( ·𝑠 ‘ 𝐾 ) ( 𝑓 ‘ 𝑤 ) ) ) ↔ ( 𝑓 ∈ ( 𝐽 GrpHom 𝐾 ) ∧ 𝐺 = 𝐹 ∧ ∀ 𝑧 ∈ 𝑃 ∀ 𝑤 ∈ 𝐵 ( 𝑓 ‘ ( 𝑧 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) = ( 𝑧 ( ·𝑠 ‘ 𝑀 ) ( 𝑓 ‘ 𝑤 ) ) ) ) )
46 6 5 eqeq12d ⊢ ( 𝜑 → ( 𝐺 = 𝐹 ↔ ( Scalar ‘ 𝐾 ) = ( Scalar ‘ 𝐽 ) ) )
47 5 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝐹 ) = ( Base ‘ ( Scalar ‘ 𝐽 ) ) )
48 9 47 eqtrid ⊢ ( 𝜑 → 𝑃 = ( Base ‘ ( Scalar ‘ 𝐽 ) ) )
49 1 raleqdv ⊢ ( 𝜑 → ( ∀ 𝑤 ∈ 𝐵 ( 𝑓 ‘ ( 𝑧 ( ·𝑠 ‘ 𝐽 ) 𝑤 ) ) = ( 𝑧 ( ·𝑠 ‘ 𝐾 ) ( 𝑓 ‘ 𝑤 ) ) ↔ ∀ 𝑤 ∈ ( Base ‘ 𝐽 ) ( 𝑓 ‘ ( 𝑧 ( ·𝑠 ‘ 𝐽 ) 𝑤 ) ) = ( 𝑧 ( ·𝑠 ‘ 𝐾 ) ( 𝑓 ‘ 𝑤 ) ) ) )
50 48 49 raleqbidv ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ 𝑃 ∀ 𝑤 ∈ 𝐵 ( 𝑓 ‘ ( 𝑧 ( ·𝑠 ‘ 𝐽 ) 𝑤 ) ) = ( 𝑧 ( ·𝑠 ‘ 𝐾 ) ( 𝑓 ‘ 𝑤 ) ) ↔ ∀ 𝑧 ∈ ( Base ‘ ( Scalar ‘ 𝐽 ) ) ∀ 𝑤 ∈ ( Base ‘ 𝐽 ) ( 𝑓 ‘ ( 𝑧 ( ·𝑠 ‘ 𝐽 ) 𝑤 ) ) = ( 𝑧 ( ·𝑠 ‘ 𝐾 ) ( 𝑓 ‘ 𝑤 ) ) ) )
51 46 50 3anbi23d ⊢ ( 𝜑 → ( ( 𝑓 ∈ ( 𝐽 GrpHom 𝐾 ) ∧ 𝐺 = 𝐹 ∧ ∀ 𝑧 ∈ 𝑃 ∀ 𝑤 ∈ 𝐵 ( 𝑓 ‘ ( 𝑧 ( ·𝑠 ‘ 𝐽 ) 𝑤 ) ) = ( 𝑧 ( ·𝑠 ‘ 𝐾 ) ( 𝑓 ‘ 𝑤 ) ) ) ↔ ( 𝑓 ∈ ( 𝐽 GrpHom 𝐾 ) ∧ ( Scalar ‘ 𝐾 ) = ( Scalar ‘ 𝐽 ) ∧ ∀ 𝑧 ∈ ( Base ‘ ( Scalar ‘ 𝐽 ) ) ∀ 𝑤 ∈ ( Base ‘ 𝐽 ) ( 𝑓 ‘ ( 𝑧 ( ·𝑠 ‘ 𝐽 ) 𝑤 ) ) = ( 𝑧 ( ·𝑠 ‘ 𝐾 ) ( 𝑓 ‘ 𝑤 ) ) ) ) )
52 1 2 3 4 11 12 ghmpropd ⊢ ( 𝜑 → ( 𝐽 GrpHom 𝐾 ) = ( 𝐿 GrpHom 𝑀 ) )
53 52 eleq2d ⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝐽 GrpHom 𝐾 ) ↔ 𝑓 ∈ ( 𝐿 GrpHom 𝑀 ) ) )
54 8 7 eqeq12d ⊢ ( 𝜑 → ( 𝐺 = 𝐹 ↔ ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝐿 ) ) )
55 7 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝐹 ) = ( Base ‘ ( Scalar ‘ 𝐿 ) ) )
56 9 55 eqtrid ⊢ ( 𝜑 → 𝑃 = ( Base ‘ ( Scalar ‘ 𝐿 ) ) )
57 3 raleqdv ⊢ ( 𝜑 → ( ∀ 𝑤 ∈ 𝐵 ( 𝑓 ‘ ( 𝑧 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) = ( 𝑧 ( ·𝑠 ‘ 𝑀 ) ( 𝑓 ‘ 𝑤 ) ) ↔ ∀ 𝑤 ∈ ( Base ‘ 𝐿 ) ( 𝑓 ‘ ( 𝑧 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) = ( 𝑧 ( ·𝑠 ‘ 𝑀 ) ( 𝑓 ‘ 𝑤 ) ) ) )
58 56 57 raleqbidv ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ 𝑃 ∀ 𝑤 ∈ 𝐵 ( 𝑓 ‘ ( 𝑧 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) = ( 𝑧 ( ·𝑠 ‘ 𝑀 ) ( 𝑓 ‘ 𝑤 ) ) ↔ ∀ 𝑧 ∈ ( Base ‘ ( Scalar ‘ 𝐿 ) ) ∀ 𝑤 ∈ ( Base ‘ 𝐿 ) ( 𝑓 ‘ ( 𝑧 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) = ( 𝑧 ( ·𝑠 ‘ 𝑀 ) ( 𝑓 ‘ 𝑤 ) ) ) )
59 53 54 58 3anbi123d ⊢ ( 𝜑 → ( ( 𝑓 ∈ ( 𝐽 GrpHom 𝐾 ) ∧ 𝐺 = 𝐹 ∧ ∀ 𝑧 ∈ 𝑃 ∀ 𝑤 ∈ 𝐵 ( 𝑓 ‘ ( 𝑧 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) = ( 𝑧 ( ·𝑠 ‘ 𝑀 ) ( 𝑓 ‘ 𝑤 ) ) ) ↔ ( 𝑓 ∈ ( 𝐿 GrpHom 𝑀 ) ∧ ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝐿 ) ∧ ∀ 𝑧 ∈ ( Base ‘ ( Scalar ‘ 𝐿 ) ) ∀ 𝑤 ∈ ( Base ‘ 𝐿 ) ( 𝑓 ‘ ( 𝑧 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) = ( 𝑧 ( ·𝑠 ‘ 𝑀 ) ( 𝑓 ‘ 𝑤 ) ) ) ) )
60 45 51 59 3bitr3d ⊢ ( 𝜑 → ( ( 𝑓 ∈ ( 𝐽 GrpHom 𝐾 ) ∧ ( Scalar ‘ 𝐾 ) = ( Scalar ‘ 𝐽 ) ∧ ∀ 𝑧 ∈ ( Base ‘ ( Scalar ‘ 𝐽 ) ) ∀ 𝑤 ∈ ( Base ‘ 𝐽 ) ( 𝑓 ‘ ( 𝑧 ( ·𝑠 ‘ 𝐽 ) 𝑤 ) ) = ( 𝑧 ( ·𝑠 ‘ 𝐾 ) ( 𝑓 ‘ 𝑤 ) ) ) ↔ ( 𝑓 ∈ ( 𝐿 GrpHom 𝑀 ) ∧ ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝐿 ) ∧ ∀ 𝑧 ∈ ( Base ‘ ( Scalar ‘ 𝐿 ) ) ∀ 𝑤 ∈ ( Base ‘ 𝐿 ) ( 𝑓 ‘ ( 𝑧 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) = ( 𝑧 ( ·𝑠 ‘ 𝑀 ) ( 𝑓 ‘ 𝑤 ) ) ) ) )
61 17 60 anbi12d ⊢ ( 𝜑 → ( ( ( 𝐽 ∈ LMod ∧ 𝐾 ∈ LMod ) ∧ ( 𝑓 ∈ ( 𝐽 GrpHom 𝐾 ) ∧ ( Scalar ‘ 𝐾 ) = ( Scalar ‘ 𝐽 ) ∧ ∀ 𝑧 ∈ ( Base ‘ ( Scalar ‘ 𝐽 ) ) ∀ 𝑤 ∈ ( Base ‘ 𝐽 ) ( 𝑓 ‘ ( 𝑧 ( ·𝑠 ‘ 𝐽 ) 𝑤 ) ) = ( 𝑧 ( ·𝑠 ‘ 𝐾 ) ( 𝑓 ‘ 𝑤 ) ) ) ) ↔ ( ( 𝐿 ∈ LMod ∧ 𝑀 ∈ LMod ) ∧ ( 𝑓 ∈ ( 𝐿 GrpHom 𝑀 ) ∧ ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝐿 ) ∧ ∀ 𝑧 ∈ ( Base ‘ ( Scalar ‘ 𝐿 ) ) ∀ 𝑤 ∈ ( Base ‘ 𝐿 ) ( 𝑓 ‘ ( 𝑧 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) = ( 𝑧 ( ·𝑠 ‘ 𝑀 ) ( 𝑓 ‘ 𝑤 ) ) ) ) ) )
62 eqid ⊢ ( Scalar ‘ 𝐽 ) = ( Scalar ‘ 𝐽 )
63 eqid ⊢ ( Scalar ‘ 𝐾 ) = ( Scalar ‘ 𝐾 )
64 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝐽 ) ) = ( Base ‘ ( Scalar ‘ 𝐽 ) )
65 eqid ⊢ ( ·𝑠 ‘ 𝐽 ) = ( ·𝑠 ‘ 𝐽 )
66 eqid ⊢ ( ·𝑠 ‘ 𝐾 ) = ( ·𝑠 ‘ 𝐾 )
67 62 63 64 28 65 66 islmhm ⊢ ( 𝑓 ∈ ( 𝐽 LMHom 𝐾 ) ↔ ( ( 𝐽 ∈ LMod ∧ 𝐾 ∈ LMod ) ∧ ( 𝑓 ∈ ( 𝐽 GrpHom 𝐾 ) ∧ ( Scalar ‘ 𝐾 ) = ( Scalar ‘ 𝐽 ) ∧ ∀ 𝑧 ∈ ( Base ‘ ( Scalar ‘ 𝐽 ) ) ∀ 𝑤 ∈ ( Base ‘ 𝐽 ) ( 𝑓 ‘ ( 𝑧 ( ·𝑠 ‘ 𝐽 ) 𝑤 ) ) = ( 𝑧 ( ·𝑠 ‘ 𝐾 ) ( 𝑓 ‘ 𝑤 ) ) ) ) )
68 eqid ⊢ ( Scalar ‘ 𝐿 ) = ( Scalar ‘ 𝐿 )
69 eqid ⊢ ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝑀 )
70 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝐿 ) ) = ( Base ‘ ( Scalar ‘ 𝐿 ) )
71 eqid ⊢ ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
72 eqid ⊢ ( ·𝑠 ‘ 𝐿 ) = ( ·𝑠 ‘ 𝐿 )
73 eqid ⊢ ( ·𝑠 ‘ 𝑀 ) = ( ·𝑠 ‘ 𝑀 )
74 68 69 70 71 72 73 islmhm ⊢ ( 𝑓 ∈ ( 𝐿 LMHom 𝑀 ) ↔ ( ( 𝐿 ∈ LMod ∧ 𝑀 ∈ LMod ) ∧ ( 𝑓 ∈ ( 𝐿 GrpHom 𝑀 ) ∧ ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝐿 ) ∧ ∀ 𝑧 ∈ ( Base ‘ ( Scalar ‘ 𝐿 ) ) ∀ 𝑤 ∈ ( Base ‘ 𝐿 ) ( 𝑓 ‘ ( 𝑧 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) = ( 𝑧 ( ·𝑠 ‘ 𝑀 ) ( 𝑓 ‘ 𝑤 ) ) ) ) )
75 61 67 74 3bitr4g ⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝐽 LMHom 𝐾 ) ↔ 𝑓 ∈ ( 𝐿 LMHom 𝑀 ) ) )
76 75 eqrdv ⊢ ( 𝜑 → ( 𝐽 LMHom 𝐾 ) = ( 𝐿 LMHom 𝑀 ) )