# 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 𝑇 ) )