# Metamath Proof Explorer

## Theorem dvhlveclem

Description: Lemma for dvhlvec . TODO: proof substituting inner part first shorter/longer than substituting outer part first? TODO: break up into smaller lemmas? TODO: does ph -> method shorten proof? (Contributed by NM, 22-Oct-2013) (Proof shortened by Mario Carneiro, 24-Jun-2014)

Ref Expression
Hypotheses dvhgrp.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
dvhgrp.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
dvhgrp.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
dvhgrp.e ${⊢}{E}=\mathrm{TEndo}\left({K}\right)\left({W}\right)$
dvhgrp.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
dvhgrp.d ${⊢}{D}=\mathrm{Scalar}\left({U}\right)$
dvhgrp.p
dvhgrp.a
dvhgrp.o
dvhgrp.i ${⊢}{I}={inv}_{g}\left({D}\right)$
dvhlvec.m
dvhlvec.s
Assertion dvhlveclem ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {U}\in \mathrm{LVec}$

### Proof

Step Hyp Ref Expression
1 dvhgrp.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 dvhgrp.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
3 dvhgrp.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
4 dvhgrp.e ${⊢}{E}=\mathrm{TEndo}\left({K}\right)\left({W}\right)$
5 dvhgrp.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
6 dvhgrp.d ${⊢}{D}=\mathrm{Scalar}\left({U}\right)$
7 dvhgrp.p
8 dvhgrp.a
9 dvhgrp.o
10 dvhgrp.i ${⊢}{I}={inv}_{g}\left({D}\right)$
11 dvhlvec.m
12 dvhlvec.s
13 eqid ${⊢}{\mathrm{Base}}_{{U}}={\mathrm{Base}}_{{U}}$
14 2 3 4 5 13 dvhvbase ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {\mathrm{Base}}_{{U}}={T}×{E}$
15 14 eqcomd ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {T}×{E}={\mathrm{Base}}_{{U}}$
16 8 a1i
17 6 a1i ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {D}=\mathrm{Scalar}\left({U}\right)$
18 12 a1i
19 eqid ${⊢}{\mathrm{Base}}_{{D}}={\mathrm{Base}}_{{D}}$
20 2 4 5 6 19 dvhbase ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {\mathrm{Base}}_{{D}}={E}$
21 20 eqcomd ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {E}={\mathrm{Base}}_{{D}}$
22 7 a1i
23 11 a1i
24 eqid ${⊢}\mathrm{EDRing}\left({K}\right)\left({W}\right)=\mathrm{EDRing}\left({K}\right)\left({W}\right)$
25 2 24 5 6 dvhsca ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {D}=\mathrm{EDRing}\left({K}\right)\left({W}\right)$
26 25 fveq2d ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {1}_{{D}}={1}_{\mathrm{EDRing}\left({K}\right)\left({W}\right)}$
27 eqid ${⊢}{1}_{\mathrm{EDRing}\left({K}\right)\left({W}\right)}={1}_{\mathrm{EDRing}\left({K}\right)\left({W}\right)}$
28 2 3 24 27 erng1r ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {1}_{\mathrm{EDRing}\left({K}\right)\left({W}\right)}={\mathrm{I}↾}_{{T}}$
29 26 28 eqtr2d ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {\mathrm{I}↾}_{{T}}={1}_{{D}}$
30 2 24 erngdv ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \mathrm{EDRing}\left({K}\right)\left({W}\right)\in \mathrm{DivRing}$
31 25 30 eqeltrd ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {D}\in \mathrm{DivRing}$
32 drngring ${⊢}{D}\in \mathrm{DivRing}\to {D}\in \mathrm{Ring}$
33 31 32 syl ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {D}\in \mathrm{Ring}$
34 1 2 3 4 5 6 7 8 9 10 dvhgrp ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {U}\in \mathrm{Grp}$
35 2 3 4 5 12 dvhvscacl
36 35 3impb
37 simpl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({s}\in {E}\wedge {t}\in \left({T}×{E}\right)\wedge {f}\in \left({T}×{E}\right)\right)\right)\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
38 simpr1 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({s}\in {E}\wedge {t}\in \left({T}×{E}\right)\wedge {f}\in \left({T}×{E}\right)\right)\right)\to {s}\in {E}$
39 simpr2 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({s}\in {E}\wedge {t}\in \left({T}×{E}\right)\wedge {f}\in \left({T}×{E}\right)\right)\right)\to {t}\in \left({T}×{E}\right)$
40 xp1st ${⊢}{t}\in \left({T}×{E}\right)\to {1}^{st}\left({t}\right)\in {T}$
41 39 40 syl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({s}\in {E}\wedge {t}\in \left({T}×{E}\right)\wedge {f}\in \left({T}×{E}\right)\right)\right)\to {1}^{st}\left({t}\right)\in {T}$
42 simpr3 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({s}\in {E}\wedge {t}\in \left({T}×{E}\right)\wedge {f}\in \left({T}×{E}\right)\right)\right)\to {f}\in \left({T}×{E}\right)$
43 xp1st ${⊢}{f}\in \left({T}×{E}\right)\to {1}^{st}\left({f}\right)\in {T}$
44 42 43 syl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({s}\in {E}\wedge {t}\in \left({T}×{E}\right)\wedge {f}\in \left({T}×{E}\right)\right)\right)\to {1}^{st}\left({f}\right)\in {T}$
45 2 3 4 tendospdi1 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({s}\in {E}\wedge {1}^{st}\left({t}\right)\in {T}\wedge {1}^{st}\left({f}\right)\in {T}\right)\right)\to {s}\left({1}^{st}\left({t}\right)\circ {1}^{st}\left({f}\right)\right)={s}\left({1}^{st}\left({t}\right)\right)\circ {s}\left({1}^{st}\left({f}\right)\right)$
46 37 38 41 44 45 syl13anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({s}\in {E}\wedge {t}\in \left({T}×{E}\right)\wedge {f}\in \left({T}×{E}\right)\right)\right)\to {s}\left({1}^{st}\left({t}\right)\circ {1}^{st}\left({f}\right)\right)={s}\left({1}^{st}\left({t}\right)\right)\circ {s}\left({1}^{st}\left({f}\right)\right)$
47 2 3 4 5 6 8 7 dvhvadd
49 48 fveq2d
50 fvex ${⊢}{1}^{st}\left({t}\right)\in \mathrm{V}$
51 fvex ${⊢}{1}^{st}\left({f}\right)\in \mathrm{V}$
52 50 51 coex ${⊢}{1}^{st}\left({t}\right)\circ {1}^{st}\left({f}\right)\in \mathrm{V}$
53 ovex
54 52 53 op1st
55 49 54 syl6eq
56 55 fveq2d
57 2 3 4 5 12 dvhvsca
59 58 fveq2d
60 fvex ${⊢}{s}\left({1}^{st}\left({t}\right)\right)\in \mathrm{V}$
61 vex ${⊢}{s}\in \mathrm{V}$
62 fvex ${⊢}{2}^{nd}\left({t}\right)\in \mathrm{V}$
63 61 62 coex ${⊢}{s}\circ {2}^{nd}\left({t}\right)\in \mathrm{V}$
64 60 63 op1st ${⊢}{1}^{st}\left(⟨{s}\left({1}^{st}\left({t}\right)\right),{s}\circ {2}^{nd}\left({t}\right)⟩\right)={s}\left({1}^{st}\left({t}\right)\right)$
65 59 64 syl6eq
66 2 3 4 5 12 dvhvsca
68 67 fveq2d
69 fvex ${⊢}{s}\left({1}^{st}\left({f}\right)\right)\in \mathrm{V}$
70 fvex ${⊢}{2}^{nd}\left({f}\right)\in \mathrm{V}$
71 61 70 coex ${⊢}{s}\circ {2}^{nd}\left({f}\right)\in \mathrm{V}$
72 69 71 op1st ${⊢}{1}^{st}\left(⟨{s}\left({1}^{st}\left({f}\right)\right),{s}\circ {2}^{nd}\left({f}\right)⟩\right)={s}\left({1}^{st}\left({f}\right)\right)$
73 68 72 syl6eq
74 65 73 coeq12d
75 46 56 74 3eqtr4d
76 33 adantr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({s}\in {E}\wedge {t}\in \left({T}×{E}\right)\wedge {f}\in \left({T}×{E}\right)\right)\right)\to {D}\in \mathrm{Ring}$
77 21 adantr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({s}\in {E}\wedge {t}\in \left({T}×{E}\right)\wedge {f}\in \left({T}×{E}\right)\right)\right)\to {E}={\mathrm{Base}}_{{D}}$
78 38 77 eleqtrd ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({s}\in {E}\wedge {t}\in \left({T}×{E}\right)\wedge {f}\in \left({T}×{E}\right)\right)\right)\to {s}\in {\mathrm{Base}}_{{D}}$
79 xp2nd ${⊢}{t}\in \left({T}×{E}\right)\to {2}^{nd}\left({t}\right)\in {E}$
80 39 79 syl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({s}\in {E}\wedge {t}\in \left({T}×{E}\right)\wedge {f}\in \left({T}×{E}\right)\right)\right)\to {2}^{nd}\left({t}\right)\in {E}$
81 80 77 eleqtrd ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({s}\in {E}\wedge {t}\in \left({T}×{E}\right)\wedge {f}\in \left({T}×{E}\right)\right)\right)\to {2}^{nd}\left({t}\right)\in {\mathrm{Base}}_{{D}}$
82 xp2nd ${⊢}{f}\in \left({T}×{E}\right)\to {2}^{nd}\left({f}\right)\in {E}$
83 42 82 syl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({s}\in {E}\wedge {t}\in \left({T}×{E}\right)\wedge {f}\in \left({T}×{E}\right)\right)\right)\to {2}^{nd}\left({f}\right)\in {E}$
84 83 77 eleqtrd ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({s}\in {E}\wedge {t}\in \left({T}×{E}\right)\wedge {f}\in \left({T}×{E}\right)\right)\right)\to {2}^{nd}\left({f}\right)\in {\mathrm{Base}}_{{D}}$
85 19 7 11 ringdi
86 76 78 81 84 85 syl13anc
87 19 7 ringacl
88 76 81 84 87 syl3anc
89 88 77 eleqtrrd
90 2 3 4 5 6 11 dvhmulr
91 37 38 89 90 syl12anc
92 2 3 4 5 6 11 dvhmulr
93 37 38 80 92 syl12anc
94 2 3 4 5 6 11 dvhmulr
95 37 38 83 94 syl12anc
96 93 95 oveq12d
97 86 91 96 3eqtr3d
98 48 fveq2d
99 52 53 op2nd
100 98 99 syl6eq
101 100 coeq2d
102 58 fveq2d
103 60 63 op2nd ${⊢}{2}^{nd}\left(⟨{s}\left({1}^{st}\left({t}\right)\right),{s}\circ {2}^{nd}\left({t}\right)⟩\right)={s}\circ {2}^{nd}\left({t}\right)$
104 102 103 syl6eq
105 67 fveq2d
106 69 71 op2nd ${⊢}{2}^{nd}\left(⟨{s}\left({1}^{st}\left({f}\right)\right),{s}\circ {2}^{nd}\left({f}\right)⟩\right)={s}\circ {2}^{nd}\left({f}\right)$
107 105 106 syl6eq
108 104 107 oveq12d
109 97 101 108 3eqtr4d
110 75 109 opeq12d
111 2 3 4 5 6 7 8 dvhvaddcl
113 2 3 4 5 12 dvhvsca
114 37 38 112 113 syl12anc
116 2 3 4 5 12 dvhvscacl
118 2 3 4 5 6 8 7 dvhvadd
119 37 115 117 118 syl12anc
120 110 114 119 3eqtr4d
121 simpl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({s}\in {E}\wedge {t}\in {E}\wedge {f}\in \left({T}×{E}\right)\right)\right)\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
122 simpr1 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({s}\in {E}\wedge {t}\in {E}\wedge {f}\in \left({T}×{E}\right)\right)\right)\to {s}\in {E}$
123 simpr2 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({s}\in {E}\wedge {t}\in {E}\wedge {f}\in \left({T}×{E}\right)\right)\right)\to {t}\in {E}$
124 simpr3 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({s}\in {E}\wedge {t}\in {E}\wedge {f}\in \left({T}×{E}\right)\right)\right)\to {f}\in \left({T}×{E}\right)$
125 124 43 syl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({s}\in {E}\wedge {t}\in {E}\wedge {f}\in \left({T}×{E}\right)\right)\right)\to {1}^{st}\left({f}\right)\in {T}$
126 eqid ${⊢}{+}_{\mathrm{EDRing}\left({K}\right)\left({W}\right)}={+}_{\mathrm{EDRing}\left({K}\right)\left({W}\right)}$
127 2 3 4 24 126 erngplus2 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({s}\in {E}\wedge {t}\in {E}\wedge {1}^{st}\left({f}\right)\in {T}\right)\right)\to \left({s}{+}_{\mathrm{EDRing}\left({K}\right)\left({W}\right)}{t}\right)\left({1}^{st}\left({f}\right)\right)={s}\left({1}^{st}\left({f}\right)\right)\circ {t}\left({1}^{st}\left({f}\right)\right)$
128 121 122 123 125 127 syl13anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({s}\in {E}\wedge {t}\in {E}\wedge {f}\in \left({T}×{E}\right)\right)\right)\to \left({s}{+}_{\mathrm{EDRing}\left({K}\right)\left({W}\right)}{t}\right)\left({1}^{st}\left({f}\right)\right)={s}\left({1}^{st}\left({f}\right)\right)\circ {t}\left({1}^{st}\left({f}\right)\right)$
129 25 fveq2d ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {+}_{{D}}={+}_{\mathrm{EDRing}\left({K}\right)\left({W}\right)}$
130 7 129 syl5eq
131 130 oveqd
132 131 fveq1d
135 134 fveq2d
136 135 72 syl6eq
137 2 3 4 5 12 dvhvsca
139 138 fveq2d
140 fvex ${⊢}{t}\left({1}^{st}\left({f}\right)\right)\in \mathrm{V}$
141 vex ${⊢}{t}\in \mathrm{V}$
142 141 70 coex ${⊢}{t}\circ {2}^{nd}\left({f}\right)\in \mathrm{V}$
143 140 142 op1st ${⊢}{1}^{st}\left(⟨{t}\left({1}^{st}\left({f}\right)\right),{t}\circ {2}^{nd}\left({f}\right)⟩\right)={t}\left({1}^{st}\left({f}\right)\right)$
144 139 143 syl6eq
145 136 144 coeq12d
146 128 133 145 3eqtr4d
147 33 adantr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({s}\in {E}\wedge {t}\in {E}\wedge {f}\in \left({T}×{E}\right)\right)\right)\to {D}\in \mathrm{Ring}$
148 21 adantr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({s}\in {E}\wedge {t}\in {E}\wedge {f}\in \left({T}×{E}\right)\right)\right)\to {E}={\mathrm{Base}}_{{D}}$
149 122 148 eleqtrd ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({s}\in {E}\wedge {t}\in {E}\wedge {f}\in \left({T}×{E}\right)\right)\right)\to {s}\in {\mathrm{Base}}_{{D}}$
150 123 148 eleqtrd ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({s}\in {E}\wedge {t}\in {E}\wedge {f}\in \left({T}×{E}\right)\right)\right)\to {t}\in {\mathrm{Base}}_{{D}}$
151 124 82 syl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({s}\in {E}\wedge {t}\in {E}\wedge {f}\in \left({T}×{E}\right)\right)\right)\to {2}^{nd}\left({f}\right)\in {E}$
152 151 148 eleqtrd ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({s}\in {E}\wedge {t}\in {E}\wedge {f}\in \left({T}×{E}\right)\right)\right)\to {2}^{nd}\left({f}\right)\in {\mathrm{Base}}_{{D}}$
153 19 7 11 ringdir
154 147 149 150 152 153 syl13anc
155 19 7 ringacl
156 147 149 150 155 syl3anc
157 156 148 eleqtrrd
158 2 3 4 5 6 11 dvhmulr
159 121 157 151 158 syl12anc
160 121 122 151 94 syl12anc
161 2 3 4 5 6 11 dvhmulr
162 121 123 151 161 syl12anc
163 160 162 oveq12d
164 154 159 163 3eqtr3d
165 134 fveq2d
166 165 106 syl6eq
167 138 fveq2d
168 140 142 op2nd ${⊢}{2}^{nd}\left(⟨{t}\left({1}^{st}\left({f}\right)\right),{t}\circ {2}^{nd}\left({f}\right)⟩\right)={t}\circ {2}^{nd}\left({f}\right)$
169 167 168 syl6eq
170 166 169 oveq12d
171 164 170 eqtr4d
172 146 171 opeq12d
173 2 3 4 5 12 dvhvsca
174 121 157 124 173 syl12anc
176 2 3 4 5 12 dvhvscacl
178 2 3 4 5 6 8 7 dvhvadd
179 121 175 177 178 syl12anc
180 172 174 179 3eqtr4d
181 2 3 4 tendocoval ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({s}\in {E}\wedge {t}\in {E}\right)\wedge {1}^{st}\left({f}\right)\in {T}\right)\to \left({s}\circ {t}\right)\left({1}^{st}\left({f}\right)\right)={s}\left({t}\left({1}^{st}\left({f}\right)\right)\right)$
182 121 122 123 125 181 syl121anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({s}\in {E}\wedge {t}\in {E}\wedge {f}\in \left({T}×{E}\right)\right)\right)\to \left({s}\circ {t}\right)\left({1}^{st}\left({f}\right)\right)={s}\left({t}\left({1}^{st}\left({f}\right)\right)\right)$
183 coass ${⊢}\left({s}\circ {t}\right)\circ {2}^{nd}\left({f}\right)={s}\circ \left({t}\circ {2}^{nd}\left({f}\right)\right)$
184 183 a1i ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({s}\in {E}\wedge {t}\in {E}\wedge {f}\in \left({T}×{E}\right)\right)\right)\to \left({s}\circ {t}\right)\circ {2}^{nd}\left({f}\right)={s}\circ \left({t}\circ {2}^{nd}\left({f}\right)\right)$
185 182 184 opeq12d ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({s}\in {E}\wedge {t}\in {E}\wedge {f}\in \left({T}×{E}\right)\right)\right)\to ⟨\left({s}\circ {t}\right)\left({1}^{st}\left({f}\right)\right),\left({s}\circ {t}\right)\circ {2}^{nd}\left({f}\right)⟩=⟨{s}\left({t}\left({1}^{st}\left({f}\right)\right)\right),{s}\circ \left({t}\circ {2}^{nd}\left({f}\right)\right)⟩$
186 2 4 tendococl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {s}\in {E}\wedge {t}\in {E}\right)\to {s}\circ {t}\in {E}$
187 121 122 123 186 syl3anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({s}\in {E}\wedge {t}\in {E}\wedge {f}\in \left({T}×{E}\right)\right)\right)\to {s}\circ {t}\in {E}$
188 2 3 4 5 12 dvhvsca
189 121 187 124 188 syl12anc
190 2 3 4 tendocl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {t}\in {E}\wedge {1}^{st}\left({f}\right)\in {T}\right)\to {t}\left({1}^{st}\left({f}\right)\right)\in {T}$
191 121 123 125 190 syl3anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({s}\in {E}\wedge {t}\in {E}\wedge {f}\in \left({T}×{E}\right)\right)\right)\to {t}\left({1}^{st}\left({f}\right)\right)\in {T}$
192 2 4 tendococl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {t}\in {E}\wedge {2}^{nd}\left({f}\right)\in {E}\right)\to {t}\circ {2}^{nd}\left({f}\right)\in {E}$
193 121 123 151 192 syl3anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({s}\in {E}\wedge {t}\in {E}\wedge {f}\in \left({T}×{E}\right)\right)\right)\to {t}\circ {2}^{nd}\left({f}\right)\in {E}$
194 2 3 4 5 12 dvhopvsca
195 121 122 191 193 194 syl13anc
196 185 189 195 3eqtr4d
197 2 3 4 5 6 11 dvhmulr
199 198 oveq1d
200 138 oveq2d
201 196 199 200 3eqtr4d
202 xp1st ${⊢}{s}\in \left({T}×{E}\right)\to {1}^{st}\left({s}\right)\in {T}$
203 202 adantl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {s}\in \left({T}×{E}\right)\right)\to {1}^{st}\left({s}\right)\in {T}$
204 fvresi ${⊢}{1}^{st}\left({s}\right)\in {T}\to \left({\mathrm{I}↾}_{{T}}\right)\left({1}^{st}\left({s}\right)\right)={1}^{st}\left({s}\right)$
205 203 204 syl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {s}\in \left({T}×{E}\right)\right)\to \left({\mathrm{I}↾}_{{T}}\right)\left({1}^{st}\left({s}\right)\right)={1}^{st}\left({s}\right)$
206 xp2nd ${⊢}{s}\in \left({T}×{E}\right)\to {2}^{nd}\left({s}\right)\in {E}$
207 2 3 4 tendof ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {2}^{nd}\left({s}\right)\in {E}\right)\to {2}^{nd}\left({s}\right):{T}⟶{T}$
208 206 207 sylan2 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {s}\in \left({T}×{E}\right)\right)\to {2}^{nd}\left({s}\right):{T}⟶{T}$
209 fcoi2 ${⊢}{2}^{nd}\left({s}\right):{T}⟶{T}\to \left({\mathrm{I}↾}_{{T}}\right)\circ {2}^{nd}\left({s}\right)={2}^{nd}\left({s}\right)$
210 208 209 syl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {s}\in \left({T}×{E}\right)\right)\to \left({\mathrm{I}↾}_{{T}}\right)\circ {2}^{nd}\left({s}\right)={2}^{nd}\left({s}\right)$
211 205 210 opeq12d ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {s}\in \left({T}×{E}\right)\right)\to ⟨\left({\mathrm{I}↾}_{{T}}\right)\left({1}^{st}\left({s}\right)\right),\left({\mathrm{I}↾}_{{T}}\right)\circ {2}^{nd}\left({s}\right)⟩=⟨{1}^{st}\left({s}\right),{2}^{nd}\left({s}\right)⟩$
212 2 3 4 tendoidcl ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {\mathrm{I}↾}_{{T}}\in {E}$
213 212 anim1i ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {s}\in \left({T}×{E}\right)\right)\to \left({\mathrm{I}↾}_{{T}}\in {E}\wedge {s}\in \left({T}×{E}\right)\right)$
214 2 3 4 5 12 dvhvsca
215 213 214 syldan
216 1st2nd2 ${⊢}{s}\in \left({T}×{E}\right)\to {s}=⟨{1}^{st}\left({s}\right),{2}^{nd}\left({s}\right)⟩$
217 216 adantl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {s}\in \left({T}×{E}\right)\right)\to {s}=⟨{1}^{st}\left({s}\right),{2}^{nd}\left({s}\right)⟩$
218 211 215 217 3eqtr4d
219 15 16 17 18 21 22 23 29 33 34 36 120 180 201 218 islmodd ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {U}\in \mathrm{LMod}$
220 6 islvec ${⊢}{U}\in \mathrm{LVec}↔\left({U}\in \mathrm{LMod}\wedge {D}\in \mathrm{DivRing}\right)$
221 219 31 220 sylanbrc ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {U}\in \mathrm{LVec}$