| Step | Hyp | Ref
| Expression |
| 1 | | lmhmvsca.v |
. 2
⊢ 𝑉 = (Base‘𝑀) |
| 2 | | eqid 2737 |
. 2
⊢ (
·𝑠 ‘𝑀) = ( ·𝑠
‘𝑀) |
| 3 | | lmhmvsca.s |
. 2
⊢ · = (
·𝑠 ‘𝑁) |
| 4 | | eqid 2737 |
. 2
⊢
(Scalar‘𝑀) =
(Scalar‘𝑀) |
| 5 | | lmhmvsca.j |
. 2
⊢ 𝐽 = (Scalar‘𝑁) |
| 6 | | eqid 2737 |
. 2
⊢
(Base‘(Scalar‘𝑀)) = (Base‘(Scalar‘𝑀)) |
| 7 | | lmhmlmod1 21032 |
. . 3
⊢ (𝐹 ∈ (𝑀 LMHom 𝑁) → 𝑀 ∈ LMod) |
| 8 | 7 | 3ad2ant3 1136 |
. 2
⊢ ((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) → 𝑀 ∈ LMod) |
| 9 | | lmhmlmod2 21031 |
. . 3
⊢ (𝐹 ∈ (𝑀 LMHom 𝑁) → 𝑁 ∈ LMod) |
| 10 | 9 | 3ad2ant3 1136 |
. 2
⊢ ((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) → 𝑁 ∈ LMod) |
| 11 | 4, 5 | lmhmsca 21029 |
. . 3
⊢ (𝐹 ∈ (𝑀 LMHom 𝑁) → 𝐽 = (Scalar‘𝑀)) |
| 12 | 11 | 3ad2ant3 1136 |
. 2
⊢ ((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) → 𝐽 = (Scalar‘𝑀)) |
| 13 | 1 | fvexi 6920 |
. . . . . 6
⊢ 𝑉 ∈ V |
| 14 | 13 | a1i 11 |
. . . . 5
⊢ ((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) → 𝑉 ∈ V) |
| 15 | | simpl2 1193 |
. . . . 5
⊢ (((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ 𝑣 ∈ 𝑉) → 𝐴 ∈ 𝐾) |
| 16 | | eqid 2737 |
. . . . . . . 8
⊢
(Base‘𝑁) =
(Base‘𝑁) |
| 17 | 1, 16 | lmhmf 21033 |
. . . . . . 7
⊢ (𝐹 ∈ (𝑀 LMHom 𝑁) → 𝐹:𝑉⟶(Base‘𝑁)) |
| 18 | 17 | 3ad2ant3 1136 |
. . . . . 6
⊢ ((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) → 𝐹:𝑉⟶(Base‘𝑁)) |
| 19 | 18 | ffvelcdmda 7104 |
. . . . 5
⊢ (((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ 𝑣 ∈ 𝑉) → (𝐹‘𝑣) ∈ (Base‘𝑁)) |
| 20 | | fconstmpt 5747 |
. . . . . 6
⊢ (𝑉 × {𝐴}) = (𝑣 ∈ 𝑉 ↦ 𝐴) |
| 21 | 20 | a1i 11 |
. . . . 5
⊢ ((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) → (𝑉 × {𝐴}) = (𝑣 ∈ 𝑉 ↦ 𝐴)) |
| 22 | 18 | feqmptd 6977 |
. . . . 5
⊢ ((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) → 𝐹 = (𝑣 ∈ 𝑉 ↦ (𝐹‘𝑣))) |
| 23 | 14, 15, 19, 21, 22 | offval2 7717 |
. . . 4
⊢ ((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) → ((𝑉 × {𝐴}) ∘f · 𝐹) = (𝑣 ∈ 𝑉 ↦ (𝐴 · (𝐹‘𝑣)))) |
| 24 | | eqidd 2738 |
. . . . 5
⊢ ((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) → (𝑢 ∈ (Base‘𝑁) ↦ (𝐴 · 𝑢)) = (𝑢 ∈ (Base‘𝑁) ↦ (𝐴 · 𝑢))) |
| 25 | | oveq2 7439 |
. . . . 5
⊢ (𝑢 = (𝐹‘𝑣) → (𝐴 · 𝑢) = (𝐴 · (𝐹‘𝑣))) |
| 26 | 19, 22, 24, 25 | fmptco 7149 |
. . . 4
⊢ ((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) → ((𝑢 ∈ (Base‘𝑁) ↦ (𝐴 · 𝑢)) ∘ 𝐹) = (𝑣 ∈ 𝑉 ↦ (𝐴 · (𝐹‘𝑣)))) |
| 27 | 23, 26 | eqtr4d 2780 |
. . 3
⊢ ((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) → ((𝑉 × {𝐴}) ∘f · 𝐹) = ((𝑢 ∈ (Base‘𝑁) ↦ (𝐴 · 𝑢)) ∘ 𝐹)) |
| 28 | | simp2 1138 |
. . . . 5
⊢ ((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) → 𝐴 ∈ 𝐾) |
| 29 | | lmhmvsca.k |
. . . . . 6
⊢ 𝐾 = (Base‘𝐽) |
| 30 | 16, 5, 3, 29 | lmodvsghm 20921 |
. . . . 5
⊢ ((𝑁 ∈ LMod ∧ 𝐴 ∈ 𝐾) → (𝑢 ∈ (Base‘𝑁) ↦ (𝐴 · 𝑢)) ∈ (𝑁 GrpHom 𝑁)) |
| 31 | 10, 28, 30 | syl2anc 584 |
. . . 4
⊢ ((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) → (𝑢 ∈ (Base‘𝑁) ↦ (𝐴 · 𝑢)) ∈ (𝑁 GrpHom 𝑁)) |
| 32 | | lmghm 21030 |
. . . . 5
⊢ (𝐹 ∈ (𝑀 LMHom 𝑁) → 𝐹 ∈ (𝑀 GrpHom 𝑁)) |
| 33 | 32 | 3ad2ant3 1136 |
. . . 4
⊢ ((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) → 𝐹 ∈ (𝑀 GrpHom 𝑁)) |
| 34 | | ghmco 19254 |
. . . 4
⊢ (((𝑢 ∈ (Base‘𝑁) ↦ (𝐴 · 𝑢)) ∈ (𝑁 GrpHom 𝑁) ∧ 𝐹 ∈ (𝑀 GrpHom 𝑁)) → ((𝑢 ∈ (Base‘𝑁) ↦ (𝐴 · 𝑢)) ∘ 𝐹) ∈ (𝑀 GrpHom 𝑁)) |
| 35 | 31, 33, 34 | syl2anc 584 |
. . 3
⊢ ((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) → ((𝑢 ∈ (Base‘𝑁) ↦ (𝐴 · 𝑢)) ∘ 𝐹) ∈ (𝑀 GrpHom 𝑁)) |
| 36 | 27, 35 | eqeltrd 2841 |
. 2
⊢ ((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) → ((𝑉 × {𝐴}) ∘f · 𝐹) ∈ (𝑀 GrpHom 𝑁)) |
| 37 | | simpl1 1192 |
. . . . . 6
⊢ (((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) → 𝐽 ∈ CRing) |
| 38 | | simpl2 1193 |
. . . . . 6
⊢ (((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) → 𝐴 ∈ 𝐾) |
| 39 | | simprl 771 |
. . . . . . 7
⊢ (((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) → 𝑥 ∈ (Base‘(Scalar‘𝑀))) |
| 40 | 12 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) → (Base‘𝐽) = (Base‘(Scalar‘𝑀))) |
| 41 | 29, 40 | eqtrid 2789 |
. . . . . . . 8
⊢ ((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) → 𝐾 = (Base‘(Scalar‘𝑀))) |
| 42 | 41 | adantr 480 |
. . . . . . 7
⊢ (((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) → 𝐾 = (Base‘(Scalar‘𝑀))) |
| 43 | 39, 42 | eleqtrrd 2844 |
. . . . . 6
⊢ (((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) → 𝑥 ∈ 𝐾) |
| 44 | | eqid 2737 |
. . . . . . 7
⊢
(.r‘𝐽) = (.r‘𝐽) |
| 45 | 29, 44 | crngcom 20248 |
. . . . . 6
⊢ ((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝑥 ∈ 𝐾) → (𝐴(.r‘𝐽)𝑥) = (𝑥(.r‘𝐽)𝐴)) |
| 46 | 37, 38, 43, 45 | syl3anc 1373 |
. . . . 5
⊢ (((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) → (𝐴(.r‘𝐽)𝑥) = (𝑥(.r‘𝐽)𝐴)) |
| 47 | 46 | oveq1d 7446 |
. . . 4
⊢ (((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) → ((𝐴(.r‘𝐽)𝑥) · (𝐹‘𝑦)) = ((𝑥(.r‘𝐽)𝐴) · (𝐹‘𝑦))) |
| 48 | 10 | adantr 480 |
. . . . 5
⊢ (((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) → 𝑁 ∈ LMod) |
| 49 | 18 | adantr 480 |
. . . . . 6
⊢ (((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) → 𝐹:𝑉⟶(Base‘𝑁)) |
| 50 | | simprr 773 |
. . . . . 6
⊢ (((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) → 𝑦 ∈ 𝑉) |
| 51 | 49, 50 | ffvelcdmd 7105 |
. . . . 5
⊢ (((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) → (𝐹‘𝑦) ∈ (Base‘𝑁)) |
| 52 | 16, 5, 3, 29, 44 | lmodvsass 20885 |
. . . . 5
⊢ ((𝑁 ∈ LMod ∧ (𝐴 ∈ 𝐾 ∧ 𝑥 ∈ 𝐾 ∧ (𝐹‘𝑦) ∈ (Base‘𝑁))) → ((𝐴(.r‘𝐽)𝑥) · (𝐹‘𝑦)) = (𝐴 · (𝑥 · (𝐹‘𝑦)))) |
| 53 | 48, 38, 43, 51, 52 | syl13anc 1374 |
. . . 4
⊢ (((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) → ((𝐴(.r‘𝐽)𝑥) · (𝐹‘𝑦)) = (𝐴 · (𝑥 · (𝐹‘𝑦)))) |
| 54 | 16, 5, 3, 29, 44 | lmodvsass 20885 |
. . . . 5
⊢ ((𝑁 ∈ LMod ∧ (𝑥 ∈ 𝐾 ∧ 𝐴 ∈ 𝐾 ∧ (𝐹‘𝑦) ∈ (Base‘𝑁))) → ((𝑥(.r‘𝐽)𝐴) · (𝐹‘𝑦)) = (𝑥 · (𝐴 · (𝐹‘𝑦)))) |
| 55 | 48, 43, 38, 51, 54 | syl13anc 1374 |
. . . 4
⊢ (((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) → ((𝑥(.r‘𝐽)𝐴) · (𝐹‘𝑦)) = (𝑥 · (𝐴 · (𝐹‘𝑦)))) |
| 56 | 47, 53, 55 | 3eqtr3d 2785 |
. . 3
⊢ (((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) → (𝐴 · (𝑥 · (𝐹‘𝑦))) = (𝑥 · (𝐴 · (𝐹‘𝑦)))) |
| 57 | 1, 4, 2, 6 | lmodvscl 20876 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ 𝑥 ∈
(Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉) → (𝑥( ·𝑠
‘𝑀)𝑦) ∈ 𝑉) |
| 58 | 57 | 3expb 1121 |
. . . . 5
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈
(Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) → (𝑥( ·𝑠
‘𝑀)𝑦) ∈ 𝑉) |
| 59 | 8, 58 | sylan 580 |
. . . 4
⊢ (((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) → (𝑥( ·𝑠
‘𝑀)𝑦) ∈ 𝑉) |
| 60 | 13 | a1i 11 |
. . . . 5
⊢ (((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) → 𝑉 ∈ V) |
| 61 | 18 | ffnd 6737 |
. . . . . 6
⊢ ((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) → 𝐹 Fn 𝑉) |
| 62 | 61 | adantr 480 |
. . . . 5
⊢ (((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) → 𝐹 Fn 𝑉) |
| 63 | 4, 6, 1, 2, 3 | lmhmlin 21034 |
. . . . . . . 8
⊢ ((𝐹 ∈ (𝑀 LMHom 𝑁) ∧ 𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉) → (𝐹‘(𝑥( ·𝑠
‘𝑀)𝑦)) = (𝑥 · (𝐹‘𝑦))) |
| 64 | 63 | 3expb 1121 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝑀 LMHom 𝑁) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) → (𝐹‘(𝑥( ·𝑠
‘𝑀)𝑦)) = (𝑥 · (𝐹‘𝑦))) |
| 65 | 64 | 3ad2antl3 1188 |
. . . . . 6
⊢ (((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) → (𝐹‘(𝑥( ·𝑠
‘𝑀)𝑦)) = (𝑥 · (𝐹‘𝑦))) |
| 66 | 65 | adantr 480 |
. . . . 5
⊢ ((((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) ∧ (𝑥( ·𝑠
‘𝑀)𝑦) ∈ 𝑉) → (𝐹‘(𝑥( ·𝑠
‘𝑀)𝑦)) = (𝑥 · (𝐹‘𝑦))) |
| 67 | 60, 38, 62, 66 | ofc1 7725 |
. . . 4
⊢ ((((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) ∧ (𝑥( ·𝑠
‘𝑀)𝑦) ∈ 𝑉) → (((𝑉 × {𝐴}) ∘f · 𝐹)‘(𝑥( ·𝑠
‘𝑀)𝑦)) = (𝐴 · (𝑥 · (𝐹‘𝑦)))) |
| 68 | 59, 67 | mpdan 687 |
. . 3
⊢ (((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) → (((𝑉 × {𝐴}) ∘f · 𝐹)‘(𝑥( ·𝑠
‘𝑀)𝑦)) = (𝐴 · (𝑥 · (𝐹‘𝑦)))) |
| 69 | | eqidd 2738 |
. . . . . 6
⊢ ((((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) ∧ 𝑦 ∈ 𝑉) → (𝐹‘𝑦) = (𝐹‘𝑦)) |
| 70 | 60, 38, 62, 69 | ofc1 7725 |
. . . . 5
⊢ ((((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) ∧ 𝑦 ∈ 𝑉) → (((𝑉 × {𝐴}) ∘f · 𝐹)‘𝑦) = (𝐴 · (𝐹‘𝑦))) |
| 71 | 50, 70 | mpdan 687 |
. . . 4
⊢ (((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) → (((𝑉 × {𝐴}) ∘f · 𝐹)‘𝑦) = (𝐴 · (𝐹‘𝑦))) |
| 72 | 71 | oveq2d 7447 |
. . 3
⊢ (((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) → (𝑥 · (((𝑉 × {𝐴}) ∘f · 𝐹)‘𝑦)) = (𝑥 · (𝐴 · (𝐹‘𝑦)))) |
| 73 | 56, 68, 72 | 3eqtr4d 2787 |
. 2
⊢ (((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ 𝑉)) → (((𝑉 × {𝐴}) ∘f · 𝐹)‘(𝑥( ·𝑠
‘𝑀)𝑦)) = (𝑥 · (((𝑉 × {𝐴}) ∘f · 𝐹)‘𝑦))) |
| 74 | 1, 2, 3, 4, 5, 6, 8, 10, 12, 36, 73 | islmhmd 21038 |
1
⊢ ((𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ (𝑀 LMHom 𝑁)) → ((𝑉 × {𝐴}) ∘f · 𝐹) ∈ (𝑀 LMHom 𝑁)) |