Metamath Proof Explorer

Theorem frlmup1

Description: Any assignment of unit vectors to target vectors can be extended (uniquely) to a homomorphism from a free module to an arbitrary other module on the same base ring. (Contributed by Stefan O'Rear, 7-Feb-2015) (Proof shortened by AV, 21-Jul-2019)

Ref Expression
Hypotheses frlmup.f ⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 )
frlmup.b ⊢ 𝐵 = ( Base ‘ 𝐹 )
frlmup.c ⊢ 𝐶 = ( Base ‘ 𝑇 )
frlmup.v ⊢ · = ( ·𝑠 ‘ 𝑇 )
frlmup.e ⊢ 𝐸 = ( 𝑥 ∈ 𝐵 ↦ ( 𝑇 Σg ( 𝑥 ∘f · 𝐴 ) ) )
frlmup.t ⊢ ( 𝜑 → 𝑇 ∈ LMod )
frlmup.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑋 )
frlmup.r ⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑇 ) )
frlmup.a ⊢ ( 𝜑 → 𝐴 : 𝐼 ⟶ 𝐶 )
Assertion frlmup1 ( 𝜑 → 𝐸 ∈ ( 𝐹 LMHom 𝑇 ) )

Proof

Step Hyp Ref Expression
1 frlmup.f ⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 )
2 frlmup.b ⊢ 𝐵 = ( Base ‘ 𝐹 )
3 frlmup.c ⊢ 𝐶 = ( Base ‘ 𝑇 )
4 frlmup.v ⊢ · = ( ·𝑠 ‘ 𝑇 )
5 frlmup.e ⊢ 𝐸 = ( 𝑥 ∈ 𝐵 ↦ ( 𝑇 Σg ( 𝑥 ∘f · 𝐴 ) ) )
6 frlmup.t ⊢ ( 𝜑 → 𝑇 ∈ LMod )
7 frlmup.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑋 )
8 frlmup.r ⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑇 ) )
9 frlmup.a ⊢ ( 𝜑 → 𝐴 : 𝐼 ⟶ 𝐶 )
10 eqid ⊢ ( ·𝑠 ‘ 𝐹 ) = ( ·𝑠 ‘ 𝐹 )
11 eqid ⊢ ( Scalar ‘ 𝐹 ) = ( Scalar ‘ 𝐹 )
12 eqid ⊢ ( Scalar ‘ 𝑇 ) = ( Scalar ‘ 𝑇 )
13 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝐹 ) ) = ( Base ‘ ( Scalar ‘ 𝐹 ) )
14 12 lmodring ⊢ ( 𝑇 ∈ LMod → ( Scalar ‘ 𝑇 ) ∈ Ring )
15 6 14 syl ⊢ ( 𝜑 → ( Scalar ‘ 𝑇 ) ∈ Ring )
16 8 15 eqeltrd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
17 1 frlmlmod ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑋 ) → 𝐹 ∈ LMod )
18 16 7 17 syl2anc ⊢ ( 𝜑 → 𝐹 ∈ LMod )
19 1 frlmsca ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑋 ) → 𝑅 = ( Scalar ‘ 𝐹 ) )
20 16 7 19 syl2anc ⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝐹 ) )
21 8 20 eqtr3d ⊢ ( 𝜑 → ( Scalar ‘ 𝑇 ) = ( Scalar ‘ 𝐹 ) )
22 eqid ⊢ ( +g ‘ 𝐹 ) = ( +g ‘ 𝐹 )
23 eqid ⊢ ( +g ‘ 𝑇 ) = ( +g ‘ 𝑇 )
24 lmodgrp ⊢ ( 𝐹 ∈ LMod → 𝐹 ∈ Grp )
25 18 24 syl ⊢ ( 𝜑 → 𝐹 ∈ Grp )
26 lmodgrp ⊢ ( 𝑇 ∈ LMod → 𝑇 ∈ Grp )
27 6 26 syl ⊢ ( 𝜑 → 𝑇 ∈ Grp )
28 eleq1w ⊢ ( 𝑧 = 𝑥 → ( 𝑧 ∈ 𝐵 ↔ 𝑥 ∈ 𝐵 ) )
29 28 anbi2d ⊢ ( 𝑧 = 𝑥 → ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ↔ ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ) )
30 oveq1 ⊢ ( 𝑧 = 𝑥 → ( 𝑧 ∘f · 𝐴 ) = ( 𝑥 ∘f · 𝐴 ) )
31 30 oveq2d ⊢ ( 𝑧 = 𝑥 → ( 𝑇 Σg ( 𝑧 ∘f · 𝐴 ) ) = ( 𝑇 Σg ( 𝑥 ∘f · 𝐴 ) ) )
32 31 eleq1d ⊢ ( 𝑧 = 𝑥 → ( ( 𝑇 Σg ( 𝑧 ∘f · 𝐴 ) ) ∈ 𝐶 ↔ ( 𝑇 Σg ( 𝑥 ∘f · 𝐴 ) ) ∈ 𝐶 ) )
33 29 32 imbi12d ⊢ ( 𝑧 = 𝑥 → ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑇 Σg ( 𝑧 ∘f · 𝐴 ) ) ∈ 𝐶 ) ↔ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑇 Σg ( 𝑥 ∘f · 𝐴 ) ) ∈ 𝐶 ) ) )
34 eqid ⊢ ( 0g ‘ 𝑇 ) = ( 0g ‘ 𝑇 )
35 lmodcmn ⊢ ( 𝑇 ∈ LMod → 𝑇 ∈ CMnd )
36 6 35 syl ⊢ ( 𝜑 → 𝑇 ∈ CMnd )
37 36 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → 𝑇 ∈ CMnd )
38 7 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → 𝐼 ∈ 𝑋 )
39 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ 𝐶 ) ) → 𝑇 ∈ LMod )
40 simprl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ 𝐶 ) ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
41 8 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑇 ) ) )
42 41 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ 𝐶 ) ) → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑇 ) ) )
43 40 42 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ 𝐶 ) ) → 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) )
44 simprr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ 𝐶 ) ) → 𝑦 ∈ 𝐶 )
45 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑇 ) ) = ( Base ‘ ( Scalar ‘ 𝑇 ) )
46 3 12 4 45 lmodvscl ⊢ ( ( 𝑇 ∈ LMod ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∧ 𝑦 ∈ 𝐶 ) → ( 𝑥 · 𝑦 ) ∈ 𝐶 )
47 39 43 44 46 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝑥 · 𝑦 ) ∈ 𝐶 )
48 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
49 1 48 2 frlmbasf ⊢ ( ( 𝐼 ∈ 𝑋 ∧ 𝑧 ∈ 𝐵 ) → 𝑧 : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
50 7 49 sylan ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → 𝑧 : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
51 9 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → 𝐴 : 𝐼 ⟶ 𝐶 )
52 inidm ⊢ ( 𝐼 ∩ 𝐼 ) = 𝐼
53 47 50 51 38 38 52 off ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑧 ∘f · 𝐴 ) : 𝐼 ⟶ 𝐶 )
54 ovexd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑧 ∘f · 𝐴 ) ∈ V )
55 53 ffund ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → Fun ( 𝑧 ∘f · 𝐴 ) )
56 fvexd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( 0g ‘ 𝑇 ) ∈ V )
57 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
58 1 57 2 frlmbasfsupp ⊢ ( ( 𝐼 ∈ 𝑋 ∧ 𝑧 ∈ 𝐵 ) → 𝑧 finSupp ( 0g ‘ 𝑅 ) )
59 7 58 sylan ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → 𝑧 finSupp ( 0g ‘ 𝑅 ) )
60 8 fveq2d ⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) = ( 0g ‘ ( Scalar ‘ 𝑇 ) ) )
61 60 eqcomd ⊢ ( 𝜑 → ( 0g ‘ ( Scalar ‘ 𝑇 ) ) = ( 0g ‘ 𝑅 ) )
62 61 breq2d ⊢ ( 𝜑 → ( 𝑧 finSupp ( 0g ‘ ( Scalar ‘ 𝑇 ) ) ↔ 𝑧 finSupp ( 0g ‘ 𝑅 ) ) )
63 62 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑧 finSupp ( 0g ‘ ( Scalar ‘ 𝑇 ) ) ↔ 𝑧 finSupp ( 0g ‘ 𝑅 ) ) )
64 59 63 mpbird ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → 𝑧 finSupp ( 0g ‘ ( Scalar ‘ 𝑇 ) ) )
65 64 fsuppimpd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑧 supp ( 0g ‘ ( Scalar ‘ 𝑇 ) ) ) ∈ Fin )
66 ssidd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑧 supp ( 0g ‘ ( Scalar ‘ 𝑇 ) ) ) ⊆ ( 𝑧 supp ( 0g ‘ ( Scalar ‘ 𝑇 ) ) ) )
67 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑤 ∈ 𝐶 ) → 𝑇 ∈ LMod )
68 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑇 ) ) = ( 0g ‘ ( Scalar ‘ 𝑇 ) )
69 3 12 4 68 34 lmod0vs ⊢ ( ( 𝑇 ∈ LMod ∧ 𝑤 ∈ 𝐶 ) → ( ( 0g ‘ ( Scalar ‘ 𝑇 ) ) · 𝑤 ) = ( 0g ‘ 𝑇 ) )
70 67 69 sylancom ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑤 ∈ 𝐶 ) → ( ( 0g ‘ ( Scalar ‘ 𝑇 ) ) · 𝑤 ) = ( 0g ‘ 𝑇 ) )
71 fvexd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( 0g ‘ ( Scalar ‘ 𝑇 ) ) ∈ V )
72 66 70 50 51 38 71 suppssof1 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( ( 𝑧 ∘f · 𝐴 ) supp ( 0g ‘ 𝑇 ) ) ⊆ ( 𝑧 supp ( 0g ‘ ( Scalar ‘ 𝑇 ) ) ) )
73 suppssfifsupp ⊢ ( ( ( ( 𝑧 ∘f · 𝐴 ) ∈ V ∧ Fun ( 𝑧 ∘f · 𝐴 ) ∧ ( 0g ‘ 𝑇 ) ∈ V ) ∧ ( ( 𝑧 supp ( 0g ‘ ( Scalar ‘ 𝑇 ) ) ) ∈ Fin ∧ ( ( 𝑧 ∘f · 𝐴 ) supp ( 0g ‘ 𝑇 ) ) ⊆ ( 𝑧 supp ( 0g ‘ ( Scalar ‘ 𝑇 ) ) ) ) ) → ( 𝑧 ∘f · 𝐴 ) finSupp ( 0g ‘ 𝑇 ) )
74 54 55 56 65 72 73 syl32anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑧 ∘f · 𝐴 ) finSupp ( 0g ‘ 𝑇 ) )
75 3 34 37 38 53 74 gsumcl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑇 Σg ( 𝑧 ∘f · 𝐴 ) ) ∈ 𝐶 )
76 33 75 chvarvv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑇 Σg ( 𝑥 ∘f · 𝐴 ) ) ∈ 𝐶 )
77 76 5 fmptd ⊢ ( 𝜑 → 𝐸 : 𝐵 ⟶ 𝐶 )
78 36 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑇 ∈ CMnd )
79 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → 𝐼 ∈ 𝑋 )
80 eleq1w ⊢ ( 𝑧 = 𝑦 → ( 𝑧 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵 ) )
81 80 anbi2d ⊢ ( 𝑧 = 𝑦 → ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ↔ ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ) )
82 oveq1 ⊢ ( 𝑧 = 𝑦 → ( 𝑧 ∘f · 𝐴 ) = ( 𝑦 ∘f · 𝐴 ) )
83 82 feq1d ⊢ ( 𝑧 = 𝑦 → ( ( 𝑧 ∘f · 𝐴 ) : 𝐼 ⟶ 𝐶 ↔ ( 𝑦 ∘f · 𝐴 ) : 𝐼 ⟶ 𝐶 ) )
84 81 83 imbi12d ⊢ ( 𝑧 = 𝑦 → ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑧 ∘f · 𝐴 ) : 𝐼 ⟶ 𝐶 ) ↔ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 ∘f · 𝐴 ) : 𝐼 ⟶ 𝐶 ) ) )
85 84 53 chvarvv ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 ∘f · 𝐴 ) : 𝐼 ⟶ 𝐶 )
86 85 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑦 ∘f · 𝐴 ) : 𝐼 ⟶ 𝐶 )
87 53 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑧 ∘f · 𝐴 ) : 𝐼 ⟶ 𝐶 )
88 82 breq1d ⊢ ( 𝑧 = 𝑦 → ( ( 𝑧 ∘f · 𝐴 ) finSupp ( 0g ‘ 𝑇 ) ↔ ( 𝑦 ∘f · 𝐴 ) finSupp ( 0g ‘ 𝑇 ) ) )
89 81 88 imbi12d ⊢ ( 𝑧 = 𝑦 → ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑧 ∘f · 𝐴 ) finSupp ( 0g ‘ 𝑇 ) ) ↔ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 ∘f · 𝐴 ) finSupp ( 0g ‘ 𝑇 ) ) ) )
90 89 74 chvarvv ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 ∘f · 𝐴 ) finSupp ( 0g ‘ 𝑇 ) )
91 90 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑦 ∘f · 𝐴 ) finSupp ( 0g ‘ 𝑇 ) )
92 74 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑧 ∘f · 𝐴 ) finSupp ( 0g ‘ 𝑇 ) )
93 3 34 23 78 79 86 87 91 92 gsumadd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑇 Σg ( ( 𝑦 ∘f · 𝐴 ) ∘f ( +g ‘ 𝑇 ) ( 𝑧 ∘f · 𝐴 ) ) ) = ( ( 𝑇 Σg ( 𝑦 ∘f · 𝐴 ) ) ( +g ‘ 𝑇 ) ( 𝑇 Σg ( 𝑧 ∘f · 𝐴 ) ) ) )
94 2 22 lmodvacl ⊢ ( ( 𝐹 ∈ LMod ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑦 ( +g ‘ 𝐹 ) 𝑧 ) ∈ 𝐵 )
95 94 3expb ⊢ ( ( 𝐹 ∈ LMod ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑦 ( +g ‘ 𝐹 ) 𝑧 ) ∈ 𝐵 )
96 18 95 sylan ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑦 ( +g ‘ 𝐹 ) 𝑧 ) ∈ 𝐵 )
97 oveq1 ⊢ ( 𝑥 = ( 𝑦 ( +g ‘ 𝐹 ) 𝑧 ) → ( 𝑥 ∘f · 𝐴 ) = ( ( 𝑦 ( +g ‘ 𝐹 ) 𝑧 ) ∘f · 𝐴 ) )
98 97 oveq2d ⊢ ( 𝑥 = ( 𝑦 ( +g ‘ 𝐹 ) 𝑧 ) → ( 𝑇 Σg ( 𝑥 ∘f · 𝐴 ) ) = ( 𝑇 Σg ( ( 𝑦 ( +g ‘ 𝐹 ) 𝑧 ) ∘f · 𝐴 ) ) )
99 ovex ⊢ ( 𝑇 Σg ( ( 𝑦 ( +g ‘ 𝐹 ) 𝑧 ) ∘f · 𝐴 ) ) ∈ V
100 98 5 99 fvmpt ⊢ ( ( 𝑦 ( +g ‘ 𝐹 ) 𝑧 ) ∈ 𝐵 → ( 𝐸 ‘ ( 𝑦 ( +g ‘ 𝐹 ) 𝑧 ) ) = ( 𝑇 Σg ( ( 𝑦 ( +g ‘ 𝐹 ) 𝑧 ) ∘f · 𝐴 ) ) )
101 96 100 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝐸 ‘ ( 𝑦 ( +g ‘ 𝐹 ) 𝑧 ) ) = ( 𝑇 Σg ( ( 𝑦 ( +g ‘ 𝐹 ) 𝑧 ) ∘f · 𝐴 ) ) )
102 16 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑅 ∈ Ring )
103 simprl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑦 ∈ 𝐵 )
104 simprr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑧 ∈ 𝐵 )
105 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
106 1 2 102 79 103 104 105 22 frlmplusgval ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑦 ( +g ‘ 𝐹 ) 𝑧 ) = ( 𝑦 ∘f ( +g ‘ 𝑅 ) 𝑧 ) )
107 106 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑦 ( +g ‘ 𝐹 ) 𝑧 ) ∘f · 𝐴 ) = ( ( 𝑦 ∘f ( +g ‘ 𝑅 ) 𝑧 ) ∘f · 𝐴 ) )
108 1 48 2 frlmbasf ⊢ ( ( 𝐼 ∈ 𝑋 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
109 7 108 sylan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
110 109 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑦 : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
111 110 ffnd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑦 Fn 𝐼 )
112 50 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑧 : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
113 112 ffnd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑧 Fn 𝐼 )
114 111 113 79 79 52 offn ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑦 ∘f ( +g ‘ 𝑅 ) 𝑧 ) Fn 𝐼 )
115 9 ffnd ⊢ ( 𝜑 → 𝐴 Fn 𝐼 )
116 115 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → 𝐴 Fn 𝐼 )
117 114 116 79 79 52 offn ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑦 ∘f ( +g ‘ 𝑅 ) 𝑧 ) ∘f · 𝐴 ) Fn 𝐼 )
118 85 ffnd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 ∘f · 𝐴 ) Fn 𝐼 )
119 118 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑦 ∘f · 𝐴 ) Fn 𝐼 )
120 53 ffnd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑧 ∘f · 𝐴 ) Fn 𝐼 )
121 120 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑧 ∘f · 𝐴 ) Fn 𝐼 )
122 119 121 79 79 52 offn ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑦 ∘f · 𝐴 ) ∘f ( +g ‘ 𝑇 ) ( 𝑧 ∘f · 𝐴 ) ) Fn 𝐼 )
123 8 fveq2d ⊢ ( 𝜑 → ( +g ‘ 𝑅 ) = ( +g ‘ ( Scalar ‘ 𝑇 ) ) )
124 123 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( +g ‘ 𝑅 ) = ( +g ‘ ( Scalar ‘ 𝑇 ) ) )
125 124 oveqd ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑦 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( 𝑧 ‘ 𝑥 ) ) = ( ( 𝑦 ‘ 𝑥 ) ( +g ‘ ( Scalar ‘ 𝑇 ) ) ( 𝑧 ‘ 𝑥 ) ) )
126 125 oveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ( 𝑦 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( 𝑧 ‘ 𝑥 ) ) · ( 𝐴 ‘ 𝑥 ) ) = ( ( ( 𝑦 ‘ 𝑥 ) ( +g ‘ ( Scalar ‘ 𝑇 ) ) ( 𝑧 ‘ 𝑥 ) ) · ( 𝐴 ‘ 𝑥 ) ) )
127 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝑇 ∈ LMod )
128 110 ffvelrnda ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑦 ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) )
129 41 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑇 ) ) )
130 128 129 eleqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑦 ‘ 𝑥 ) ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) )
131 112 ffvelrnda ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑧 ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) )
132 131 129 eleqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑧 ‘ 𝑥 ) ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) )
133 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → 𝐴 : 𝐼 ⟶ 𝐶 )
134 133 ffvelrnda ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐴 ‘ 𝑥 ) ∈ 𝐶 )
135 eqid ⊢ ( +g ‘ ( Scalar ‘ 𝑇 ) ) = ( +g ‘ ( Scalar ‘ 𝑇 ) )
136 3 23 12 4 45 135 lmodvsdir ⊢ ( ( 𝑇 ∈ LMod ∧ ( ( 𝑦 ‘ 𝑥 ) ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∧ ( 𝑧 ‘ 𝑥 ) ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∧ ( 𝐴 ‘ 𝑥 ) ∈ 𝐶 ) ) → ( ( ( 𝑦 ‘ 𝑥 ) ( +g ‘ ( Scalar ‘ 𝑇 ) ) ( 𝑧 ‘ 𝑥 ) ) · ( 𝐴 ‘ 𝑥 ) ) = ( ( ( 𝑦 ‘ 𝑥 ) · ( 𝐴 ‘ 𝑥 ) ) ( +g ‘ 𝑇 ) ( ( 𝑧 ‘ 𝑥 ) · ( 𝐴 ‘ 𝑥 ) ) ) )
137 127 130 132 134 136 syl13anc ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ( 𝑦 ‘ 𝑥 ) ( +g ‘ ( Scalar ‘ 𝑇 ) ) ( 𝑧 ‘ 𝑥 ) ) · ( 𝐴 ‘ 𝑥 ) ) = ( ( ( 𝑦 ‘ 𝑥 ) · ( 𝐴 ‘ 𝑥 ) ) ( +g ‘ 𝑇 ) ( ( 𝑧 ‘ 𝑥 ) · ( 𝐴 ‘ 𝑥 ) ) ) )
138 126 137 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ( 𝑦 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( 𝑧 ‘ 𝑥 ) ) · ( 𝐴 ‘ 𝑥 ) ) = ( ( ( 𝑦 ‘ 𝑥 ) · ( 𝐴 ‘ 𝑥 ) ) ( +g ‘ 𝑇 ) ( ( 𝑧 ‘ 𝑥 ) · ( 𝐴 ‘ 𝑥 ) ) ) )
139 111 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝑦 Fn 𝐼 )
140 113 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝑧 Fn 𝐼 )
141 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝐼 ∈ 𝑋 )
142 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝑥 ∈ 𝐼 )
143 fnfvof ⊢ ( ( ( 𝑦 Fn 𝐼 ∧ 𝑧 Fn 𝐼 ) ∧ ( 𝐼 ∈ 𝑋 ∧ 𝑥 ∈ 𝐼 ) ) → ( ( 𝑦 ∘f ( +g ‘ 𝑅 ) 𝑧 ) ‘ 𝑥 ) = ( ( 𝑦 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( 𝑧 ‘ 𝑥 ) ) )
144 139 140 141 142 143 syl22anc ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑦 ∘f ( +g ‘ 𝑅 ) 𝑧 ) ‘ 𝑥 ) = ( ( 𝑦 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( 𝑧 ‘ 𝑥 ) ) )
145 144 oveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ( 𝑦 ∘f ( +g ‘ 𝑅 ) 𝑧 ) ‘ 𝑥 ) · ( 𝐴 ‘ 𝑥 ) ) = ( ( ( 𝑦 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( 𝑧 ‘ 𝑥 ) ) · ( 𝐴 ‘ 𝑥 ) ) )
146 115 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝐴 Fn 𝐼 )
147 fnfvof ⊢ ( ( ( 𝑦 Fn 𝐼 ∧ 𝐴 Fn 𝐼 ) ∧ ( 𝐼 ∈ 𝑋 ∧ 𝑥 ∈ 𝐼 ) ) → ( ( 𝑦 ∘f · 𝐴 ) ‘ 𝑥 ) = ( ( 𝑦 ‘ 𝑥 ) · ( 𝐴 ‘ 𝑥 ) ) )
148 139 146 141 142 147 syl22anc ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑦 ∘f · 𝐴 ) ‘ 𝑥 ) = ( ( 𝑦 ‘ 𝑥 ) · ( 𝐴 ‘ 𝑥 ) ) )
149 fnfvof ⊢ ( ( ( 𝑧 Fn 𝐼 ∧ 𝐴 Fn 𝐼 ) ∧ ( 𝐼 ∈ 𝑋 ∧ 𝑥 ∈ 𝐼 ) ) → ( ( 𝑧 ∘f · 𝐴 ) ‘ 𝑥 ) = ( ( 𝑧 ‘ 𝑥 ) · ( 𝐴 ‘ 𝑥 ) ) )
150 140 146 141 142 149 syl22anc ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑧 ∘f · 𝐴 ) ‘ 𝑥 ) = ( ( 𝑧 ‘ 𝑥 ) · ( 𝐴 ‘ 𝑥 ) ) )
151 148 150 oveq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ( 𝑦 ∘f · 𝐴 ) ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( ( 𝑧 ∘f · 𝐴 ) ‘ 𝑥 ) ) = ( ( ( 𝑦 ‘ 𝑥 ) · ( 𝐴 ‘ 𝑥 ) ) ( +g ‘ 𝑇 ) ( ( 𝑧 ‘ 𝑥 ) · ( 𝐴 ‘ 𝑥 ) ) ) )
152 138 145 151 3eqtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ( 𝑦 ∘f ( +g ‘ 𝑅 ) 𝑧 ) ‘ 𝑥 ) · ( 𝐴 ‘ 𝑥 ) ) = ( ( ( 𝑦 ∘f · 𝐴 ) ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( ( 𝑧 ∘f · 𝐴 ) ‘ 𝑥 ) ) )
153 114 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑦 ∘f ( +g ‘ 𝑅 ) 𝑧 ) Fn 𝐼 )
154 fnfvof ⊢ ( ( ( ( 𝑦 ∘f ( +g ‘ 𝑅 ) 𝑧 ) Fn 𝐼 ∧ 𝐴 Fn 𝐼 ) ∧ ( 𝐼 ∈ 𝑋 ∧ 𝑥 ∈ 𝐼 ) ) → ( ( ( 𝑦 ∘f ( +g ‘ 𝑅 ) 𝑧 ) ∘f · 𝐴 ) ‘ 𝑥 ) = ( ( ( 𝑦 ∘f ( +g ‘ 𝑅 ) 𝑧 ) ‘ 𝑥 ) · ( 𝐴 ‘ 𝑥 ) ) )
155 153 146 141 142 154 syl22anc ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ( 𝑦 ∘f ( +g ‘ 𝑅 ) 𝑧 ) ∘f · 𝐴 ) ‘ 𝑥 ) = ( ( ( 𝑦 ∘f ( +g ‘ 𝑅 ) 𝑧 ) ‘ 𝑥 ) · ( 𝐴 ‘ 𝑥 ) ) )
156 119 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑦 ∘f · 𝐴 ) Fn 𝐼 )
157 121 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑧 ∘f · 𝐴 ) Fn 𝐼 )
158 fnfvof ⊢ ( ( ( ( 𝑦 ∘f · 𝐴 ) Fn 𝐼 ∧ ( 𝑧 ∘f · 𝐴 ) Fn 𝐼 ) ∧ ( 𝐼 ∈ 𝑋 ∧ 𝑥 ∈ 𝐼 ) ) → ( ( ( 𝑦 ∘f · 𝐴 ) ∘f ( +g ‘ 𝑇 ) ( 𝑧 ∘f · 𝐴 ) ) ‘ 𝑥 ) = ( ( ( 𝑦 ∘f · 𝐴 ) ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( ( 𝑧 ∘f · 𝐴 ) ‘ 𝑥 ) ) )
159 156 157 141 142 158 syl22anc ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ( 𝑦 ∘f · 𝐴 ) ∘f ( +g ‘ 𝑇 ) ( 𝑧 ∘f · 𝐴 ) ) ‘ 𝑥 ) = ( ( ( 𝑦 ∘f · 𝐴 ) ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( ( 𝑧 ∘f · 𝐴 ) ‘ 𝑥 ) ) )
160 152 155 159 3eqtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ( 𝑦 ∘f ( +g ‘ 𝑅 ) 𝑧 ) ∘f · 𝐴 ) ‘ 𝑥 ) = ( ( ( 𝑦 ∘f · 𝐴 ) ∘f ( +g ‘ 𝑇 ) ( 𝑧 ∘f · 𝐴 ) ) ‘ 𝑥 ) )
161 117 122 160 eqfnfvd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑦 ∘f ( +g ‘ 𝑅 ) 𝑧 ) ∘f · 𝐴 ) = ( ( 𝑦 ∘f · 𝐴 ) ∘f ( +g ‘ 𝑇 ) ( 𝑧 ∘f · 𝐴 ) ) )
162 107 161 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑦 ( +g ‘ 𝐹 ) 𝑧 ) ∘f · 𝐴 ) = ( ( 𝑦 ∘f · 𝐴 ) ∘f ( +g ‘ 𝑇 ) ( 𝑧 ∘f · 𝐴 ) ) )
163 162 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑇 Σg ( ( 𝑦 ( +g ‘ 𝐹 ) 𝑧 ) ∘f · 𝐴 ) ) = ( 𝑇 Σg ( ( 𝑦 ∘f · 𝐴 ) ∘f ( +g ‘ 𝑇 ) ( 𝑧 ∘f · 𝐴 ) ) ) )
164 101 163 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝐸 ‘ ( 𝑦 ( +g ‘ 𝐹 ) 𝑧 ) ) = ( 𝑇 Σg ( ( 𝑦 ∘f · 𝐴 ) ∘f ( +g ‘ 𝑇 ) ( 𝑧 ∘f · 𝐴 ) ) ) )
165 oveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∘f · 𝐴 ) = ( 𝑦 ∘f · 𝐴 ) )
166 165 oveq2d ⊢ ( 𝑥 = 𝑦 → ( 𝑇 Σg ( 𝑥 ∘f · 𝐴 ) ) = ( 𝑇 Σg ( 𝑦 ∘f · 𝐴 ) ) )
167 ovex ⊢ ( 𝑇 Σg ( 𝑦 ∘f · 𝐴 ) ) ∈ V
168 166 5 167 fvmpt ⊢ ( 𝑦 ∈ 𝐵 → ( 𝐸 ‘ 𝑦 ) = ( 𝑇 Σg ( 𝑦 ∘f · 𝐴 ) ) )
169 168 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝐸 ‘ 𝑦 ) = ( 𝑇 Σg ( 𝑦 ∘f · 𝐴 ) ) )
170 oveq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∘f · 𝐴 ) = ( 𝑧 ∘f · 𝐴 ) )
171 170 oveq2d ⊢ ( 𝑥 = 𝑧 → ( 𝑇 Σg ( 𝑥 ∘f · 𝐴 ) ) = ( 𝑇 Σg ( 𝑧 ∘f · 𝐴 ) ) )
172 ovex ⊢ ( 𝑇 Σg ( 𝑧 ∘f · 𝐴 ) ) ∈ V
173 171 5 172 fvmpt ⊢ ( 𝑧 ∈ 𝐵 → ( 𝐸 ‘ 𝑧 ) = ( 𝑇 Σg ( 𝑧 ∘f · 𝐴 ) ) )
174 173 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝐸 ‘ 𝑧 ) = ( 𝑇 Σg ( 𝑧 ∘f · 𝐴 ) ) )
175 169 174 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝐸 ‘ 𝑦 ) ( +g ‘ 𝑇 ) ( 𝐸 ‘ 𝑧 ) ) = ( ( 𝑇 Σg ( 𝑦 ∘f · 𝐴 ) ) ( +g ‘ 𝑇 ) ( 𝑇 Σg ( 𝑧 ∘f · 𝐴 ) ) ) )
176 93 164 175 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝐸 ‘ ( 𝑦 ( +g ‘ 𝐹 ) 𝑧 ) ) = ( ( 𝐸 ‘ 𝑦 ) ( +g ‘ 𝑇 ) ( 𝐸 ‘ 𝑧 ) ) )
177 2 3 22 23 25 27 77 176 isghmd ⊢ ( 𝜑 → 𝐸 ∈ ( 𝐹 GrpHom 𝑇 ) )
178 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) ) → 𝑇 ∈ LMod )
179 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) ) → 𝐼 ∈ 𝑋 )
180 21 fveq2d ⊢ ( 𝜑 → ( Base ‘ ( Scalar ‘ 𝑇 ) ) = ( Base ‘ ( Scalar ‘ 𝐹 ) ) )
181 180 eleq2d ⊢ ( 𝜑 → ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ↔ 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ) )
182 181 biimpar ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ) → 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) )
183 182 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) ) → 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) )
184 53 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑧 ∘f · 𝐴 ) : 𝐼 ⟶ 𝐶 )
185 184 ffvelrnda ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑧 ∘f · 𝐴 ) ‘ 𝑥 ) ∈ 𝐶 )
186 53 feqmptd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑧 ∘f · 𝐴 ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑧 ∘f · 𝐴 ) ‘ 𝑥 ) ) )
187 186 74 eqbrtrrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑧 ∘f · 𝐴 ) ‘ 𝑥 ) ) finSupp ( 0g ‘ 𝑇 ) )
188 187 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑧 ∘f · 𝐴 ) ‘ 𝑥 ) ) finSupp ( 0g ‘ 𝑇 ) )
189 3 12 45 34 23 4 178 179 183 185 188 gsumvsmul ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑇 Σg ( 𝑥 ∈ 𝐼 ↦ ( 𝑦 · ( ( 𝑧 ∘f · 𝐴 ) ‘ 𝑥 ) ) ) ) = ( 𝑦 · ( 𝑇 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑧 ∘f · 𝐴 ) ‘ 𝑥 ) ) ) ) )
190 18 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) ) → 𝐹 ∈ LMod )
191 simprl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) ) → 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) )
192 simprr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) ) → 𝑧 ∈ 𝐵 )
193 2 11 10 13 lmodvscl ⊢ ( ( 𝐹 ∈ LMod ∧ 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝑦 ( ·𝑠 ‘ 𝐹 ) 𝑧 ) ∈ 𝐵 )
194 190 191 192 193 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑦 ( ·𝑠 ‘ 𝐹 ) 𝑧 ) ∈ 𝐵 )
195 1 48 2 frlmbasf ⊢ ( ( 𝐼 ∈ 𝑋 ∧ ( 𝑦 ( ·𝑠 ‘ 𝐹 ) 𝑧 ) ∈ 𝐵 ) → ( 𝑦 ( ·𝑠 ‘ 𝐹 ) 𝑧 ) : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
196 179 194 195 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑦 ( ·𝑠 ‘ 𝐹 ) 𝑧 ) : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
197 196 ffnd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑦 ( ·𝑠 ‘ 𝐹 ) 𝑧 ) Fn 𝐼 )
198 115 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) ) → 𝐴 Fn 𝐼 )
199 197 198 179 179 52 offn ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑦 ( ·𝑠 ‘ 𝐹 ) 𝑧 ) ∘f · 𝐴 ) Fn 𝐼 )
200 dffn2 ⊢ ( ( ( 𝑦 ( ·𝑠 ‘ 𝐹 ) 𝑧 ) ∘f · 𝐴 ) Fn 𝐼 ↔ ( ( 𝑦 ( ·𝑠 ‘ 𝐹 ) 𝑧 ) ∘f · 𝐴 ) : 𝐼 ⟶ V )
201 199 200 sylib ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑦 ( ·𝑠 ‘ 𝐹 ) 𝑧 ) ∘f · 𝐴 ) : 𝐼 ⟶ V )
202 201 feqmptd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑦 ( ·𝑠 ‘ 𝐹 ) 𝑧 ) ∘f · 𝐴 ) = ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑦 ( ·𝑠 ‘ 𝐹 ) 𝑧 ) ∘f · 𝐴 ) ‘ 𝑥 ) ) )
203 8 fveq2d ⊢ ( 𝜑 → ( .r ‘ 𝑅 ) = ( .r ‘ ( Scalar ‘ 𝑇 ) ) )
204 203 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( .r ‘ 𝑅 ) = ( .r ‘ ( Scalar ‘ 𝑇 ) ) )
205 204 oveqd ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑦 ( .r ‘ 𝑅 ) ( 𝑧 ‘ 𝑥 ) ) = ( 𝑦 ( .r ‘ ( Scalar ‘ 𝑇 ) ) ( 𝑧 ‘ 𝑥 ) ) )
206 205 oveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑦 ( .r ‘ 𝑅 ) ( 𝑧 ‘ 𝑥 ) ) · ( 𝐴 ‘ 𝑥 ) ) = ( ( 𝑦 ( .r ‘ ( Scalar ‘ 𝑇 ) ) ( 𝑧 ‘ 𝑥 ) ) · ( 𝐴 ‘ 𝑥 ) ) )
207 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝑇 ∈ LMod )
208 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) )
209 180 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( Base ‘ ( Scalar ‘ 𝑇 ) ) = ( Base ‘ ( Scalar ‘ 𝐹 ) ) )
210 208 209 eleqtrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) )
211 50 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑧 ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) )
212 41 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐼 ) → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑇 ) ) )
213 211 212 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑧 ‘ 𝑥 ) ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) )
214 213 adantlrl ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑧 ‘ 𝑥 ) ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) )
215 9 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝐴 ‘ 𝑥 ) ∈ 𝐶 )
216 215 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐴 ‘ 𝑥 ) ∈ 𝐶 )
217 eqid ⊢ ( .r ‘ ( Scalar ‘ 𝑇 ) ) = ( .r ‘ ( Scalar ‘ 𝑇 ) )
218 3 12 4 45 217 lmodvsass ⊢ ( ( 𝑇 ∈ LMod ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∧ ( 𝑧 ‘ 𝑥 ) ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∧ ( 𝐴 ‘ 𝑥 ) ∈ 𝐶 ) ) → ( ( 𝑦 ( .r ‘ ( Scalar ‘ 𝑇 ) ) ( 𝑧 ‘ 𝑥 ) ) · ( 𝐴 ‘ 𝑥 ) ) = ( 𝑦 · ( ( 𝑧 ‘ 𝑥 ) · ( 𝐴 ‘ 𝑥 ) ) ) )
219 207 210 214 216 218 syl13anc ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑦 ( .r ‘ ( Scalar ‘ 𝑇 ) ) ( 𝑧 ‘ 𝑥 ) ) · ( 𝐴 ‘ 𝑥 ) ) = ( 𝑦 · ( ( 𝑧 ‘ 𝑥 ) · ( 𝐴 ‘ 𝑥 ) ) ) )
220 206 219 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑦 ( .r ‘ 𝑅 ) ( 𝑧 ‘ 𝑥 ) ) · ( 𝐴 ‘ 𝑥 ) ) = ( 𝑦 · ( ( 𝑧 ‘ 𝑥 ) · ( 𝐴 ‘ 𝑥 ) ) ) )
221 197 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑦 ( ·𝑠 ‘ 𝐹 ) 𝑧 ) Fn 𝐼 )
222 115 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝐴 Fn 𝐼 )
223 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝐼 ∈ 𝑋 )
224 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝑥 ∈ 𝐼 )
225 fnfvof ⊢ ( ( ( ( 𝑦 ( ·𝑠 ‘ 𝐹 ) 𝑧 ) Fn 𝐼 ∧ 𝐴 Fn 𝐼 ) ∧ ( 𝐼 ∈ 𝑋 ∧ 𝑥 ∈ 𝐼 ) ) → ( ( ( 𝑦 ( ·𝑠 ‘ 𝐹 ) 𝑧 ) ∘f · 𝐴 ) ‘ 𝑥 ) = ( ( ( 𝑦 ( ·𝑠 ‘ 𝐹 ) 𝑧 ) ‘ 𝑥 ) · ( 𝐴 ‘ 𝑥 ) ) )
226 221 222 223 224 225 syl22anc ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ( 𝑦 ( ·𝑠 ‘ 𝐹 ) 𝑧 ) ∘f · 𝐴 ) ‘ 𝑥 ) = ( ( ( 𝑦 ( ·𝑠 ‘ 𝐹 ) 𝑧 ) ‘ 𝑥 ) · ( 𝐴 ‘ 𝑥 ) ) )
227 20 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝐹 ) ) )
228 227 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝐹 ) ) )
229 208 228 eleqtrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝑦 ∈ ( Base ‘ 𝑅 ) )
230 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝑧 ∈ 𝐵 )
231 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
232 1 2 48 223 229 230 224 10 231 frlmvscaval ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑦 ( ·𝑠 ‘ 𝐹 ) 𝑧 ) ‘ 𝑥 ) = ( 𝑦 ( .r ‘ 𝑅 ) ( 𝑧 ‘ 𝑥 ) ) )
233 232 oveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ( 𝑦 ( ·𝑠 ‘ 𝐹 ) 𝑧 ) ‘ 𝑥 ) · ( 𝐴 ‘ 𝑥 ) ) = ( ( 𝑦 ( .r ‘ 𝑅 ) ( 𝑧 ‘ 𝑥 ) ) · ( 𝐴 ‘ 𝑥 ) ) )
234 226 233 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ( 𝑦 ( ·𝑠 ‘ 𝐹 ) 𝑧 ) ∘f · 𝐴 ) ‘ 𝑥 ) = ( ( 𝑦 ( .r ‘ 𝑅 ) ( 𝑧 ‘ 𝑥 ) ) · ( 𝐴 ‘ 𝑥 ) ) )
235 50 ffnd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → 𝑧 Fn 𝐼 )
236 235 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) ) → 𝑧 Fn 𝐼 )
237 236 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝑧 Fn 𝐼 )
238 237 222 223 224 149 syl22anc ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑧 ∘f · 𝐴 ) ‘ 𝑥 ) = ( ( 𝑧 ‘ 𝑥 ) · ( 𝐴 ‘ 𝑥 ) ) )
239 238 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑦 · ( ( 𝑧 ∘f · 𝐴 ) ‘ 𝑥 ) ) = ( 𝑦 · ( ( 𝑧 ‘ 𝑥 ) · ( 𝐴 ‘ 𝑥 ) ) ) )
240 220 234 239 3eqtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ( 𝑦 ( ·𝑠 ‘ 𝐹 ) 𝑧 ) ∘f · 𝐴 ) ‘ 𝑥 ) = ( 𝑦 · ( ( 𝑧 ∘f · 𝐴 ) ‘ 𝑥 ) ) )
241 240 mpteq2dva ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑦 ( ·𝑠 ‘ 𝐹 ) 𝑧 ) ∘f · 𝐴 ) ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑦 · ( ( 𝑧 ∘f · 𝐴 ) ‘ 𝑥 ) ) ) )
242 202 241 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑦 ( ·𝑠 ‘ 𝐹 ) 𝑧 ) ∘f · 𝐴 ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑦 · ( ( 𝑧 ∘f · 𝐴 ) ‘ 𝑥 ) ) ) )
243 242 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑇 Σg ( ( 𝑦 ( ·𝑠 ‘ 𝐹 ) 𝑧 ) ∘f · 𝐴 ) ) = ( 𝑇 Σg ( 𝑥 ∈ 𝐼 ↦ ( 𝑦 · ( ( 𝑧 ∘f · 𝐴 ) ‘ 𝑥 ) ) ) ) )
244 184 feqmptd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑧 ∘f · 𝐴 ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑧 ∘f · 𝐴 ) ‘ 𝑥 ) ) )
245 244 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑇 Σg ( 𝑧 ∘f · 𝐴 ) ) = ( 𝑇 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑧 ∘f · 𝐴 ) ‘ 𝑥 ) ) ) )
246 245 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑦 · ( 𝑇 Σg ( 𝑧 ∘f · 𝐴 ) ) ) = ( 𝑦 · ( 𝑇 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑧 ∘f · 𝐴 ) ‘ 𝑥 ) ) ) ) )
247 189 243 246 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑇 Σg ( ( 𝑦 ( ·𝑠 ‘ 𝐹 ) 𝑧 ) ∘f · 𝐴 ) ) = ( 𝑦 · ( 𝑇 Σg ( 𝑧 ∘f · 𝐴 ) ) ) )
248 oveq1 ⊢ ( 𝑥 = ( 𝑦 ( ·𝑠 ‘ 𝐹 ) 𝑧 ) → ( 𝑥 ∘f · 𝐴 ) = ( ( 𝑦 ( ·𝑠 ‘ 𝐹 ) 𝑧 ) ∘f · 𝐴 ) )
249 248 oveq2d ⊢ ( 𝑥 = ( 𝑦 ( ·𝑠 ‘ 𝐹 ) 𝑧 ) → ( 𝑇 Σg ( 𝑥 ∘f · 𝐴 ) ) = ( 𝑇 Σg ( ( 𝑦 ( ·𝑠 ‘ 𝐹 ) 𝑧 ) ∘f · 𝐴 ) ) )
250 ovex ⊢ ( 𝑇 Σg ( ( 𝑦 ( ·𝑠 ‘ 𝐹 ) 𝑧 ) ∘f · 𝐴 ) ) ∈ V
251 249 5 250 fvmpt ⊢ ( ( 𝑦 ( ·𝑠 ‘ 𝐹 ) 𝑧 ) ∈ 𝐵 → ( 𝐸 ‘ ( 𝑦 ( ·𝑠 ‘ 𝐹 ) 𝑧 ) ) = ( 𝑇 Σg ( ( 𝑦 ( ·𝑠 ‘ 𝐹 ) 𝑧 ) ∘f · 𝐴 ) ) )
252 194 251 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝐸 ‘ ( 𝑦 ( ·𝑠 ‘ 𝐹 ) 𝑧 ) ) = ( 𝑇 Σg ( ( 𝑦 ( ·𝑠 ‘ 𝐹 ) 𝑧 ) ∘f · 𝐴 ) ) )
253 173 oveq2d ⊢ ( 𝑧 ∈ 𝐵 → ( 𝑦 · ( 𝐸 ‘ 𝑧 ) ) = ( 𝑦 · ( 𝑇 Σg ( 𝑧 ∘f · 𝐴 ) ) ) )
254 253 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑦 · ( 𝐸 ‘ 𝑧 ) ) = ( 𝑦 · ( 𝑇 Σg ( 𝑧 ∘f · 𝐴 ) ) ) )
255 247 252 254 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝐸 ‘ ( 𝑦 ( ·𝑠 ‘ 𝐹 ) 𝑧 ) ) = ( 𝑦 · ( 𝐸 ‘ 𝑧 ) ) )
256 2 10 4 11 12 13 18 6 21 177 255 islmhmd ⊢ ( 𝜑 → 𝐸 ∈ ( 𝐹 LMHom 𝑇 ) )