Metamath Proof Explorer

Theorem lmhmvsca

Description: The pointwise scalar product of a linear function and a constant is linear, over a commutative ring. (Contributed by Mario Carneiro, 22-Sep-2015)

Ref Expression
Hypotheses lmhmvsca.v ⊢ 𝑉 = ( Base ‘ 𝑀 )
lmhmvsca.s ⊢ · = ( ·𝑠 ‘ 𝑁 )
lmhmvsca.j ⊢ 𝐽 = ( Scalar ‘ 𝑁 )
lmhmvsca.k ⊢ 𝐾 = ( Base ‘ 𝐽 )
Assertion lmhmvsca ( ( 𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ) → ( ( 𝑉 × { 𝐴 } ) ∘f · 𝐹 ) ∈ ( 𝑀 LMHom 𝑁 ) )

Proof

Step Hyp Ref Expression
1 lmhmvsca.v ⊢ 𝑉 = ( Base ‘ 𝑀 )
2 lmhmvsca.s ⊢ · = ( ·𝑠 ‘ 𝑁 )
3 lmhmvsca.j ⊢ 𝐽 = ( Scalar ‘ 𝑁 )
4 lmhmvsca.k ⊢ 𝐾 = ( Base ‘ 𝐽 )
5 eqid ⊢ ( ·𝑠 ‘ 𝑀 ) = ( ·𝑠 ‘ 𝑀 )
6 eqid ⊢ ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝑀 )
7 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑀 ) ) = ( Base ‘ ( Scalar ‘ 𝑀 ) )
8 lmhmlmod1 ⊢ ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) → 𝑀 ∈ LMod )
9 8 3ad2ant3 ⊢ ( ( 𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ) → 𝑀 ∈ LMod )
10 lmhmlmod2 ⊢ ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) → 𝑁 ∈ LMod )
11 10 3ad2ant3 ⊢ ( ( 𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ) → 𝑁 ∈ LMod )
12 6 3 lmhmsca ⊢ ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) → 𝐽 = ( Scalar ‘ 𝑀 ) )
13 12 3ad2ant3 ⊢ ( ( 𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ) → 𝐽 = ( Scalar ‘ 𝑀 ) )
14 1 fvexi ⊢ 𝑉 ∈ V
15 14 a1i ⊢ ( ( 𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ) → 𝑉 ∈ V )
16 simpl2 ⊢ ( ( ( 𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ 𝑣 ∈ 𝑉 ) → 𝐴 ∈ 𝐾 )
17 eqid ⊢ ( Base ‘ 𝑁 ) = ( Base ‘ 𝑁 )
18 1 17 lmhmf ⊢ ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) → 𝐹 : 𝑉 ⟶ ( Base ‘ 𝑁 ) )
19 18 3ad2ant3 ⊢ ( ( 𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ) → 𝐹 : 𝑉 ⟶ ( Base ‘ 𝑁 ) )
20 19 ffvelcdmda ⊢ ( ( ( 𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ 𝑣 ∈ 𝑉 ) → ( 𝐹 ‘ 𝑣 ) ∈ ( Base ‘ 𝑁 ) )
21 fconstmpt ⊢ ( 𝑉 × { 𝐴 } ) = ( 𝑣 ∈ 𝑉 ↦ 𝐴 )
22 21 a1i ⊢ ( ( 𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ) → ( 𝑉 × { 𝐴 } ) = ( 𝑣 ∈ 𝑉 ↦ 𝐴 ) )
23 19 feqmptd ⊢ ( ( 𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ) → 𝐹 = ( 𝑣 ∈ 𝑉 ↦ ( 𝐹 ‘ 𝑣 ) ) )
24 15 16 20 22 23 offval2 ⊢ ( ( 𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ) → ( ( 𝑉 × { 𝐴 } ) ∘f · 𝐹 ) = ( 𝑣 ∈ 𝑉 ↦ ( 𝐴 · ( 𝐹 ‘ 𝑣 ) ) ) )
25 eqidd ⊢ ( ( 𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ) → ( 𝑢 ∈ ( Base ‘ 𝑁 ) ↦ ( 𝐴 · 𝑢 ) ) = ( 𝑢 ∈ ( Base ‘ 𝑁 ) ↦ ( 𝐴 · 𝑢 ) ) )
26 oveq2 ⊢ ( 𝑢 = ( 𝐹 ‘ 𝑣 ) → ( 𝐴 · 𝑢 ) = ( 𝐴 · ( 𝐹 ‘ 𝑣 ) ) )
27 20 23 25 26 fmptco ⊢ ( ( 𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ) → ( ( 𝑢 ∈ ( Base ‘ 𝑁 ) ↦ ( 𝐴 · 𝑢 ) ) ∘ 𝐹 ) = ( 𝑣 ∈ 𝑉 ↦ ( 𝐴 · ( 𝐹 ‘ 𝑣 ) ) ) )
28 24 27 eqtr4d ⊢ ( ( 𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ) → ( ( 𝑉 × { 𝐴 } ) ∘f · 𝐹 ) = ( ( 𝑢 ∈ ( Base ‘ 𝑁 ) ↦ ( 𝐴 · 𝑢 ) ) ∘ 𝐹 ) )
29 simp2 ⊢ ( ( 𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ) → 𝐴 ∈ 𝐾 )
30 17 3 2 4 lmodvsghm ⊢ ( ( 𝑁 ∈ LMod ∧ 𝐴 ∈ 𝐾 ) → ( 𝑢 ∈ ( Base ‘ 𝑁 ) ↦ ( 𝐴 · 𝑢 ) ) ∈ ( 𝑁 GrpHom 𝑁 ) )
31 11 29 30 syl2anc ⊢ ( ( 𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ) → ( 𝑢 ∈ ( Base ‘ 𝑁 ) ↦ ( 𝐴 · 𝑢 ) ) ∈ ( 𝑁 GrpHom 𝑁 ) )
32 lmghm ⊢ ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) → 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) )
33 32 3ad2ant3 ⊢ ( ( 𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ) → 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) )
34 ghmco ⊢ ( ( ( 𝑢 ∈ ( Base ‘ 𝑁 ) ↦ ( 𝐴 · 𝑢 ) ) ∈ ( 𝑁 GrpHom 𝑁 ) ∧ 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) ) → ( ( 𝑢 ∈ ( Base ‘ 𝑁 ) ↦ ( 𝐴 · 𝑢 ) ) ∘ 𝐹 ) ∈ ( 𝑀 GrpHom 𝑁 ) )
35 31 33 34 syl2anc ⊢ ( ( 𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ) → ( ( 𝑢 ∈ ( Base ‘ 𝑁 ) ↦ ( 𝐴 · 𝑢 ) ) ∘ 𝐹 ) ∈ ( 𝑀 GrpHom 𝑁 ) )
36 28 35 eqeltrd ⊢ ( ( 𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ) → ( ( 𝑉 × { 𝐴 } ) ∘f · 𝐹 ) ∈ ( 𝑀 GrpHom 𝑁 ) )
37 simpl1 ⊢ ( ( ( 𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ 𝑉 ) ) → 𝐽 ∈ CRing )
38 simpl2 ⊢ ( ( ( 𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ 𝑉 ) ) → 𝐴 ∈ 𝐾 )
39 simprl ⊢ ( ( ( 𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ 𝑉 ) ) → 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
40 13 fveq2d ⊢ ( ( 𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ) → ( Base ‘ 𝐽 ) = ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
41 4 40 eqtrid ⊢ ( ( 𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ) → 𝐾 = ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
42 41 adantr ⊢ ( ( ( 𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ 𝑉 ) ) → 𝐾 = ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
43 39 42 eleqtrrd ⊢ ( ( ( 𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ 𝑉 ) ) → 𝑥 ∈ 𝐾 )
44 eqid ⊢ ( .r ‘ 𝐽 ) = ( .r ‘ 𝐽 )
45 4 44 crngcom ⊢ ( ( 𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝑥 ∈ 𝐾 ) → ( 𝐴 ( .r ‘ 𝐽 ) 𝑥 ) = ( 𝑥 ( .r ‘ 𝐽 ) 𝐴 ) )
46 37 38 43 45 syl3anc ⊢ ( ( ( 𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝐴 ( .r ‘ 𝐽 ) 𝑥 ) = ( 𝑥 ( .r ‘ 𝐽 ) 𝐴 ) )
47 46 oveq1d ⊢ ( ( ( 𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ 𝑉 ) ) → ( ( 𝐴 ( .r ‘ 𝐽 ) 𝑥 ) · ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝑥 ( .r ‘ 𝐽 ) 𝐴 ) · ( 𝐹 ‘ 𝑦 ) ) )
48 11 adantr ⊢ ( ( ( 𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ 𝑉 ) ) → 𝑁 ∈ LMod )
49 19 adantr ⊢ ( ( ( 𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ 𝑉 ) ) → 𝐹 : 𝑉 ⟶ ( Base ‘ 𝑁 ) )
50 simprr ⊢ ( ( ( 𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ 𝑉 ) ) → 𝑦 ∈ 𝑉 )
51 49 50 ffvelcdmd ⊢ ( ( ( 𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ( Base ‘ 𝑁 ) )
52 17 3 2 4 44 lmodvsass ⊢ ( ( 𝑁 ∈ LMod ∧ ( 𝐴 ∈ 𝐾 ∧ 𝑥 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑦 ) ∈ ( Base ‘ 𝑁 ) ) ) → ( ( 𝐴 ( .r ‘ 𝐽 ) 𝑥 ) · ( 𝐹 ‘ 𝑦 ) ) = ( 𝐴 · ( 𝑥 · ( 𝐹 ‘ 𝑦 ) ) ) )
53 48 38 43 51 52 syl13anc ⊢ ( ( ( 𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ 𝑉 ) ) → ( ( 𝐴 ( .r ‘ 𝐽 ) 𝑥 ) · ( 𝐹 ‘ 𝑦 ) ) = ( 𝐴 · ( 𝑥 · ( 𝐹 ‘ 𝑦 ) ) ) )
54 17 3 2 4 44 lmodvsass ⊢ ( ( 𝑁 ∈ LMod ∧ ( 𝑥 ∈ 𝐾 ∧ 𝐴 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑦 ) ∈ ( Base ‘ 𝑁 ) ) ) → ( ( 𝑥 ( .r ‘ 𝐽 ) 𝐴 ) · ( 𝐹 ‘ 𝑦 ) ) = ( 𝑥 · ( 𝐴 · ( 𝐹 ‘ 𝑦 ) ) ) )
55 48 43 38 51 54 syl13anc ⊢ ( ( ( 𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ 𝑉 ) ) → ( ( 𝑥 ( .r ‘ 𝐽 ) 𝐴 ) · ( 𝐹 ‘ 𝑦 ) ) = ( 𝑥 · ( 𝐴 · ( 𝐹 ‘ 𝑦 ) ) ) )
56 47 53 55 3eqtr3d ⊢ ( ( ( 𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝐴 · ( 𝑥 · ( 𝐹 ‘ 𝑦 ) ) ) = ( 𝑥 · ( 𝐴 · ( 𝐹 ‘ 𝑦 ) ) ) )
57 1 6 5 7 lmodvscl ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ 𝑉 ) → ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ∈ 𝑉 )
58 57 3expb ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ∈ 𝑉 )
59 9 58 sylan ⊢ ( ( ( 𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ∈ 𝑉 )
60 14 a1i ⊢ ( ( ( 𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ 𝑉 ) ) → 𝑉 ∈ V )
61 19 ffnd ⊢ ( ( 𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ) → 𝐹 Fn 𝑉 )
62 61 adantr ⊢ ( ( ( 𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ 𝑉 ) ) → 𝐹 Fn 𝑉 )
63 6 7 1 5 2 lmhmlin ⊢ ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ 𝑉 ) → ( 𝐹 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) = ( 𝑥 · ( 𝐹 ‘ 𝑦 ) ) )
64 63 3expb ⊢ ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝐹 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) = ( 𝑥 · ( 𝐹 ‘ 𝑦 ) ) )
65 64 3ad2antl3 ⊢ ( ( ( 𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝐹 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) = ( 𝑥 · ( 𝐹 ‘ 𝑦 ) ) )
66 65 adantr ⊢ ( ( ( ( 𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ 𝑉 ) ) ∧ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ∈ 𝑉 ) → ( 𝐹 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) = ( 𝑥 · ( 𝐹 ‘ 𝑦 ) ) )
67 60 38 62 66 ofc1 ⊢ ( ( ( ( 𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ 𝑉 ) ) ∧ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ∈ 𝑉 ) → ( ( ( 𝑉 × { 𝐴 } ) ∘f · 𝐹 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) = ( 𝐴 · ( 𝑥 · ( 𝐹 ‘ 𝑦 ) ) ) )
68 59 67 mpdan ⊢ ( ( ( 𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ 𝑉 ) ) → ( ( ( 𝑉 × { 𝐴 } ) ∘f · 𝐹 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) = ( 𝐴 · ( 𝑥 · ( 𝐹 ‘ 𝑦 ) ) ) )
69 eqidd ⊢ ( ( ( ( 𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ 𝑉 ) ) ∧ 𝑦 ∈ 𝑉 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
70 60 38 62 69 ofc1 ⊢ ( ( ( ( 𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ 𝑉 ) ) ∧ 𝑦 ∈ 𝑉 ) → ( ( ( 𝑉 × { 𝐴 } ) ∘f · 𝐹 ) ‘ 𝑦 ) = ( 𝐴 · ( 𝐹 ‘ 𝑦 ) ) )
71 50 70 mpdan ⊢ ( ( ( 𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ 𝑉 ) ) → ( ( ( 𝑉 × { 𝐴 } ) ∘f · 𝐹 ) ‘ 𝑦 ) = ( 𝐴 · ( 𝐹 ‘ 𝑦 ) ) )
72 71 oveq2d ⊢ ( ( ( 𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝑥 · ( ( ( 𝑉 × { 𝐴 } ) ∘f · 𝐹 ) ‘ 𝑦 ) ) = ( 𝑥 · ( 𝐴 · ( 𝐹 ‘ 𝑦 ) ) ) )
73 56 68 72 3eqtr4d ⊢ ( ( ( 𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ 𝑉 ) ) → ( ( ( 𝑉 × { 𝐴 } ) ∘f · 𝐹 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) = ( 𝑥 · ( ( ( 𝑉 × { 𝐴 } ) ∘f · 𝐹 ) ‘ 𝑦 ) ) )
74 1 5 2 6 3 7 9 11 13 36 73 islmhmd ⊢ ( ( 𝐽 ∈ CRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ) → ( ( 𝑉 × { 𝐴 } ) ∘f · 𝐹 ) ∈ ( 𝑀 LMHom 𝑁 ) )