# 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 ${⊢}{F}={R}\mathrm{freeLMod}{I}$
frlmup.b ${⊢}{B}={\mathrm{Base}}_{{F}}$
frlmup.c ${⊢}{C}={\mathrm{Base}}_{{T}}$
frlmup.v
frlmup.e
frlmup.t ${⊢}{\phi }\to {T}\in \mathrm{LMod}$
frlmup.i ${⊢}{\phi }\to {I}\in {X}$
frlmup.r ${⊢}{\phi }\to {R}=\mathrm{Scalar}\left({T}\right)$
frlmup.a ${⊢}{\phi }\to {A}:{I}⟶{C}$
Assertion frlmup1 ${⊢}{\phi }\to {E}\in \left({F}\mathrm{LMHom}{T}\right)$

### Proof

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