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