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 = Base K
dvhgrp.h H = LHyp K
dvhgrp.t T = LTrn K W
dvhgrp.e E = TEndo K W
dvhgrp.u U = DVecH K W
dvhgrp.d D = Scalar U
dvhgrp.p ˙ = + D
dvhgrp.a + ˙ = + U
dvhgrp.o 0 ˙ = 0 D
dvhgrp.i I = inv g D
dvhlvec.m × ˙ = D
dvhlvec.s · ˙ = U
Assertion dvhlveclem K HL W H U LVec

Proof

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