Step | Hyp | Ref
| Expression |
1 | | lmhmvsca.v |
. 2
⊢ 𝑉 = (Base‘𝑀) |
2 | | eqid 2610 |
. 2
⊢ (
·𝑠 ‘𝑀) = ( ·𝑠
‘𝑀) |
3 | | lmhmvsca.s |
. 2
⊢ · = (
·𝑠 ‘𝑁) |
4 | | eqid 2610 |
. 2
⊢
(Scalar‘𝑀) =
(Scalar‘𝑀) |
5 | | lmhmvsca.j |
. 2
⊢ 𝐽 = (Scalar‘𝑁) |
6 | | eqid 2610 |
. 2
⊢
(Base‘(Scalar‘𝑀)) = (Base‘(Scalar‘𝑀)) |
7 | | lmhmlmod1 18854 |
. . 3
⊢ (𝐹 ∈ (𝑀 LMHom 𝑁) → 𝑀 ∈ LMod) |
8 | 7 | 3ad2ant3 1077 |
. 2
⊢ ((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) → 𝑀 ∈ LMod) |
9 | | lmhmlmod2 18853 |
. . 3
⊢ (𝐹 ∈ (𝑀 LMHom 𝑁) → 𝑁 ∈ LMod) |
10 | 9 | 3ad2ant3 1077 |
. 2
⊢ ((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) → 𝑁 ∈ LMod) |
11 | 4, 5 | lmhmsca 18851 |
. . 3
⊢ (𝐹 ∈ (𝑀 LMHom 𝑁) → 𝐽 = (Scalar‘𝑀)) |
12 | 11 | 3ad2ant3 1077 |
. 2
⊢ ((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) → 𝐽 = (Scalar‘𝑀)) |
13 | | fvex 6113 |
. . . . . . 7
⊢
(Base‘𝑀)
∈ V |
14 | 1, 13 | eqeltri 2684 |
. . . . . 6
⊢ 𝑉 ∈ V |
15 | 14 | a1i 11 |
. . . . 5
⊢ ((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) → 𝑉 ∈ V) |
16 | | simpl2 1058 |
. . . . 5
⊢ (((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ 𝑣 ∈ 𝑉) → 𝐴 ∈ 𝐾) |
17 | | eqid 2610 |
. . . . . . . 8
⊢
(Base‘𝑁) =
(Base‘𝑁) |
18 | 1, 17 | lmhmf 18855 |
. . . . . . 7
⊢ (𝐹 ∈ (𝑀 LMHom 𝑁) → 𝐹:𝑉⟶(Base‘𝑁)) |
19 | 18 | 3ad2ant3 1077 |
. . . . . 6
⊢ ((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) → 𝐹:𝑉⟶(Base‘𝑁)) |
20 | 19 | ffvelrnda 6267 |
. . . . 5
⊢ (((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ 𝑣 ∈ 𝑉) → (𝐹‘𝑣) ∈ (Base‘𝑁)) |
21 | | fconstmpt 5085 |
. . . . . 6
⊢ (𝑉 × {𝐴}) = (𝑣 ∈ 𝑉 ↦ 𝐴) |
22 | 21 | a1i 11 |
. . . . 5
⊢ ((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) → (𝑉 × {𝐴}) = (𝑣 ∈ 𝑉 ↦ 𝐴)) |
23 | 19 | feqmptd 6159 |
. . . . 5
⊢ ((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) → 𝐹 = (𝑣 ∈ 𝑉 ↦ (𝐹‘𝑣))) |
24 | 15, 16, 20, 22, 23 | offval2 6812 |
. . . 4
⊢ ((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) → ((𝑉 × {𝐴}) ∘𝑓 · 𝐹) = (𝑣 ∈ 𝑉 ↦ (𝐴 · (𝐹‘𝑣)))) |
25 | | eqidd 2611 |
. . . . 5
⊢ ((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) → (𝑢 ∈ (Base‘𝑁) ↦ (𝐴 · 𝑢)) = (𝑢 ∈ (Base‘𝑁) ↦ (𝐴 · 𝑢))) |
26 | | oveq2 6557 |
. . . . 5
⊢ (𝑢 = (𝐹‘𝑣) → (𝐴 · 𝑢) = (𝐴 · (𝐹‘𝑣))) |
27 | 20, 23, 25, 26 | fmptco 6303 |
. . . 4
⊢ ((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) → ((𝑢 ∈ (Base‘𝑁) ↦ (𝐴 · 𝑢)) ∘ 𝐹) = (𝑣 ∈ 𝑉 ↦ (𝐴 · (𝐹‘𝑣)))) |
28 | 24, 27 | eqtr4d 2647 |
. . 3
⊢ ((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) → ((𝑉 × {𝐴}) ∘𝑓 · 𝐹) = ((𝑢 ∈ (Base‘𝑁) ↦ (𝐴 · 𝑢)) ∘ 𝐹)) |
29 | | simp2 1055 |
. . . . 5
⊢ ((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) → 𝐴 ∈ 𝐾) |
30 | | lmhmvsca.k |
. . . . . 6
⊢ 𝐾 = (Base‘𝐽) |
31 | 17, 5, 3, 30 | lmodvsghm 18747 |
. . . . 5
⊢ ((𝑁 ∈ LMod ∧ 𝐴 ∈ 𝐾) → (𝑢 ∈ (Base‘𝑁) ↦ (𝐴 · 𝑢)) ∈ (𝑁 GrpHom 𝑁)) |
32 | 10, 29, 31 | syl2anc 691 |
. . . 4
⊢ ((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) → (𝑢 ∈ (Base‘𝑁) ↦ (𝐴 · 𝑢)) ∈ (𝑁 GrpHom 𝑁)) |
33 | | lmghm 18852 |
. . . . 5
⊢ (𝐹 ∈ (𝑀 LMHom 𝑁) → 𝐹 ∈ (𝑀 GrpHom 𝑁)) |
34 | 33 | 3ad2ant3 1077 |
. . . 4
⊢ ((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) → 𝐹 ∈ (𝑀 GrpHom 𝑁)) |
35 | | ghmco 17503 |
. . . 4
⊢ (((𝑢 ∈ (Base‘𝑁) ↦ (𝐴 · 𝑢)) ∈ (𝑁 GrpHom 𝑁) ∧ 𝐹 ∈ (𝑀 GrpHom 𝑁)) → ((𝑢 ∈ (Base‘𝑁) ↦ (𝐴 · 𝑢)) ∘ 𝐹) ∈ (𝑀 GrpHom 𝑁)) |
36 | 32, 34, 35 | syl2anc 691 |
. . 3
⊢ ((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) → ((𝑢 ∈ (Base‘𝑁) ↦ (𝐴 · 𝑢)) ∘ 𝐹) ∈ (𝑀 GrpHom 𝑁)) |
37 | 28, 36 | eqeltrd 2688 |
. 2
⊢ ((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) → ((𝑉 × {𝐴}) ∘𝑓 · 𝐹) ∈ (𝑀 GrpHom 𝑁)) |
38 | | simpl1 1057 |
. . . . . 6
⊢ (((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) → 𝐽 ∈ CRing) |
39 | | simpl2 1058 |
. . . . . 6
⊢ (((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) → 𝐴 ∈ 𝐾) |
40 | | simprl 790 |
. . . . . . 7
⊢ (((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) → 𝑥 ∈ (Base‘(Scalar‘𝑀))) |
41 | 12 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) → (Base‘𝐽) = (Base‘(Scalar‘𝑀))) |
42 | 30, 41 | syl5eq 2656 |
. . . . . . . 8
⊢ ((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) → 𝐾 = (Base‘(Scalar‘𝑀))) |
43 | 42 | adantr 480 |
. . . . . . 7
⊢ (((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) → 𝐾 = (Base‘(Scalar‘𝑀))) |
44 | 40, 43 | eleqtrrd 2691 |
. . . . . 6
⊢ (((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) → 𝑥 ∈ 𝐾) |
45 | | eqid 2610 |
. . . . . . 7
⊢
(.r‘𝐽) = (.r‘𝐽) |
46 | 30, 45 | crngcom 18385 |
. . . . . 6
⊢ ((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝑥 ∈ 𝐾) → (𝐴(.r‘𝐽)𝑥) = (𝑥(.r‘𝐽)𝐴)) |
47 | 38, 39, 44, 46 | syl3anc 1318 |
. . . . 5
⊢ (((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) → (𝐴(.r‘𝐽)𝑥) = (𝑥(.r‘𝐽)𝐴)) |
48 | 47 | oveq1d 6564 |
. . . 4
⊢ (((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) → ((𝐴(.r‘𝐽)𝑥) · (𝐹‘𝑦)) = ((𝑥(.r‘𝐽)𝐴) · (𝐹‘𝑦))) |
49 | 10 | adantr 480 |
. . . . 5
⊢ (((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) → 𝑁 ∈ LMod) |
50 | 19 | adantr 480 |
. . . . . 6
⊢ (((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) → 𝐹:𝑉⟶(Base‘𝑁)) |
51 | | simprr 792 |
. . . . . 6
⊢ (((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) → 𝑦 ∈ 𝑉) |
52 | 50, 51 | ffvelrnd 6268 |
. . . . 5
⊢ (((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) → (𝐹‘𝑦) ∈ (Base‘𝑁)) |
53 | 17, 5, 3, 30, 45 | lmodvsass 18711 |
. . . . 5
⊢ ((𝑁 ∈ LMod ∧ (𝐴 ∈ 𝐾 ∧ 𝑥 ∈ 𝐾 ∧ (𝐹‘𝑦) ∈ (Base‘𝑁))) → ((𝐴(.r‘𝐽)𝑥) · (𝐹‘𝑦)) = (𝐴 · (𝑥 · (𝐹‘𝑦)))) |
54 | 49, 39, 44, 52, 53 | syl13anc 1320 |
. . . 4
⊢ (((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) → ((𝐴(.r‘𝐽)𝑥) · (𝐹‘𝑦)) = (𝐴 · (𝑥 · (𝐹‘𝑦)))) |
55 | 17, 5, 3, 30, 45 | lmodvsass 18711 |
. . . . 5
⊢ ((𝑁 ∈ LMod ∧ (𝑥 ∈ 𝐾 ∧ 𝐴 ∈ 𝐾 ∧ (𝐹‘𝑦) ∈ (Base‘𝑁))) → ((𝑥(.r‘𝐽)𝐴) · (𝐹‘𝑦)) = (𝑥 · (𝐴 · (𝐹‘𝑦)))) |
56 | 49, 44, 39, 52, 55 | syl13anc 1320 |
. . . 4
⊢ (((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) → ((𝑥(.r‘𝐽)𝐴) · (𝐹‘𝑦)) = (𝑥 · (𝐴 · (𝐹‘𝑦)))) |
57 | 48, 54, 56 | 3eqtr3d 2652 |
. . 3
⊢ (((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) → (𝐴 · (𝑥 · (𝐹‘𝑦))) = (𝑥 · (𝐴 · (𝐹‘𝑦)))) |
58 | 1, 4, 2, 6 | lmodvscl 18703 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ 𝑥 ∈
(Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉) → (𝑥( ·𝑠
‘𝑀)𝑦) ∈ 𝑉) |
59 | 58 | 3expb 1258 |
. . . . 5
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈
(Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) → (𝑥( ·𝑠
‘𝑀)𝑦) ∈ 𝑉) |
60 | 8, 59 | sylan 487 |
. . . 4
⊢ (((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) → (𝑥( ·𝑠
‘𝑀)𝑦) ∈ 𝑉) |
61 | 14 | a1i 11 |
. . . . 5
⊢ (((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) → 𝑉 ∈ V) |
62 | | ffn 5958 |
. . . . . . 7
⊢ (𝐹:𝑉⟶(Base‘𝑁) → 𝐹 Fn 𝑉) |
63 | 19, 62 | syl 17 |
. . . . . 6
⊢ ((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) → 𝐹 Fn 𝑉) |
64 | 63 | adantr 480 |
. . . . 5
⊢ (((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) → 𝐹 Fn 𝑉) |
65 | 4, 6, 1, 2, 3 | lmhmlin 18856 |
. . . . . . . 8
⊢ ((𝐹 ∈ (𝑀 LMHom 𝑁) ∧ 𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉) → (𝐹‘(𝑥( ·𝑠
‘𝑀)𝑦)) = (𝑥 · (𝐹‘𝑦))) |
66 | 65 | 3expb 1258 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝑀 LMHom 𝑁) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) → (𝐹‘(𝑥( ·𝑠
‘𝑀)𝑦)) = (𝑥 · (𝐹‘𝑦))) |
67 | 66 | 3ad2antl3 1218 |
. . . . . 6
⊢ (((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) → (𝐹‘(𝑥( ·𝑠
‘𝑀)𝑦)) = (𝑥 · (𝐹‘𝑦))) |
68 | 67 | adantr 480 |
. . . . 5
⊢ ((((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) ∧ (𝑥( ·𝑠
‘𝑀)𝑦) ∈ 𝑉) → (𝐹‘(𝑥( ·𝑠
‘𝑀)𝑦)) = (𝑥 · (𝐹‘𝑦))) |
69 | 61, 39, 64, 68 | ofc1 6818 |
. . . 4
⊢ ((((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) ∧ (𝑥( ·𝑠
‘𝑀)𝑦) ∈ 𝑉) → (((𝑉 × {𝐴}) ∘𝑓 · 𝐹)‘(𝑥( ·𝑠
‘𝑀)𝑦)) = (𝐴 · (𝑥 · (𝐹‘𝑦)))) |
70 | 60, 69 | mpdan 699 |
. . 3
⊢ (((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) → (((𝑉 × {𝐴}) ∘𝑓 · 𝐹)‘(𝑥( ·𝑠
‘𝑀)𝑦)) = (𝐴 · (𝑥 · (𝐹‘𝑦)))) |
71 | | eqidd 2611 |
. . . . . 6
⊢ ((((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) ∧ 𝑦 ∈ 𝑉) → (𝐹‘𝑦) = (𝐹‘𝑦)) |
72 | 61, 39, 64, 71 | ofc1 6818 |
. . . . 5
⊢ ((((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) ∧ 𝑦 ∈ 𝑉) → (((𝑉 × {𝐴}) ∘𝑓 · 𝐹)‘𝑦) = (𝐴 · (𝐹‘𝑦))) |
73 | 51, 72 | mpdan 699 |
. . . 4
⊢ (((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) → (((𝑉 × {𝐴}) ∘𝑓 · 𝐹)‘𝑦) = (𝐴 · (𝐹‘𝑦))) |
74 | 73 | oveq2d 6565 |
. . 3
⊢ (((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) → (𝑥 · (((𝑉 × {𝐴}) ∘𝑓 · 𝐹)‘𝑦)) = (𝑥 · (𝐴 · (𝐹‘𝑦)))) |
75 | 57, 70, 74 | 3eqtr4d 2654 |
. 2
⊢ (((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) → (((𝑉 × {𝐴}) ∘𝑓 · 𝐹)‘(𝑥( ·𝑠
‘𝑀)𝑦)) = (𝑥 · (((𝑉 × {𝐴}) ∘𝑓 · 𝐹)‘𝑦))) |
76 | 1, 2, 3, 4, 5, 6, 8, 10, 12, 37, 75 | islmhmd 18860 |
1
⊢ ((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) → ((𝑉 × {𝐴}) ∘𝑓 · 𝐹) ∈ (𝑀 LMHom 𝑁)) |