Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dvhlveclem Structured version   Unicode version

Theorem dvhlveclem 34582
Description: Lemma for dvhlvec 34583. 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.)
Hypotheses
Ref Expression
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  |-  .+^  =  ( +g  `  D )
dvhgrp.a  |-  .+  =  ( +g  `  U )
dvhgrp.o  |-  .0.  =  ( 0g `  D )
dvhgrp.i  |-  I  =  ( invg `  D )
dvhlvec.m  |-  .X.  =  ( .r `  D )
dvhlvec.s  |-  .x.  =  ( .s `  U )
Assertion
Ref Expression
dvhlveclem  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  U  e.  LVec )

Proof of Theorem dvhlveclem
Dummy variables  t 
f  s are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dvhgrp.h . . . . 5  |-  H  =  ( LHyp `  K
)
2 dvhgrp.t . . . . 5  |-  T  =  ( ( LTrn `  K
) `  W )
3 dvhgrp.e . . . . 5  |-  E  =  ( ( TEndo `  K
) `  W )
4 dvhgrp.u . . . . 5  |-  U  =  ( ( DVecH `  K
) `  W )
5 eqid 2422 . . . . 5  |-  ( Base `  U )  =  (
Base `  U )
61, 2, 3, 4, 5dvhvbase 34561 . . . 4  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  ( Base `  U
)  =  ( T  X.  E ) )
76eqcomd 2428 . . 3  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  ( T  X.  E
)  =  ( Base `  U ) )
8 dvhgrp.a . . . 4  |-  .+  =  ( +g  `  U )
98a1i 11 . . 3  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  .+  =  ( +g  `  U ) )
10 dvhgrp.d . . . 4  |-  D  =  (Scalar `  U )
1110a1i 11 . . 3  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  D  =  (Scalar `  U ) )
12 dvhlvec.s . . . 4  |-  .x.  =  ( .s `  U )
1312a1i 11 . . 3  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  .x.  =  ( .s
`  U ) )
14 eqid 2422 . . . . 5  |-  ( Base `  D )  =  (
Base `  D )
151, 3, 4, 10, 14dvhbase 34557 . . . 4  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  ( Base `  D
)  =  E )
1615eqcomd 2428 . . 3  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  E  =  ( Base `  D ) )
17 dvhgrp.p . . . 4  |-  .+^  =  ( +g  `  D )
1817a1i 11 . . 3  |-  ( ( K  e.  HL  /\  W  e.  H )  -> 
.+^  =  ( +g  `  D ) )
19 dvhlvec.m . . . 4  |-  .X.  =  ( .r `  D )
2019a1i 11 . . 3  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  .X.  =  ( .r
`  D ) )
21 eqid 2422 . . . . . 6  |-  ( (
EDRing `  K ) `  W )  =  ( ( EDRing `  K ) `  W )
221, 21, 4, 10dvhsca 34556 . . . . 5  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  D  =  ( (
EDRing `  K ) `  W ) )
2322fveq2d 5822 . . . 4  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  ( 1r `  D
)  =  ( 1r
`  ( ( EDRing `  K ) `  W
) ) )
24 eqid 2422 . . . . 5  |-  ( 1r
`  ( ( EDRing `  K ) `  W
) )  =  ( 1r `  ( (
EDRing `  K ) `  W ) )
251, 2, 21, 24erng1r 34468 . . . 4  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  ( 1r `  (
( EDRing `  K ) `  W ) )  =  (  _I  |`  T ) )
2623, 25eqtr2d 2457 . . 3  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  (  _I  |`  T )  =  ( 1r `  D ) )
271, 21erngdv 34466 . . . . 5  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  ( ( EDRing `  K
) `  W )  e.  DivRing )
2822, 27eqeltrd 2500 . . . 4  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  D  e.  DivRing )
29 drngring 17918 . . . 4  |-  ( D  e.  DivRing  ->  D  e.  Ring )
3028, 29syl 17 . . 3  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  D  e.  Ring )
31 dvhgrp.b . . . 4  |-  B  =  ( Base `  K
)
32 dvhgrp.o . . . 4  |-  .0.  =  ( 0g `  D )
33 dvhgrp.i . . . 4  |-  I  =  ( invg `  D )
3431, 1, 2, 3, 4, 10, 17, 8, 32, 33dvhgrp 34581 . . 3  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  U  e.  Grp )
351, 2, 3, 4, 12dvhvscacl 34577 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  ( T  X.  E
) ) )  -> 
( s  .x.  t
)  e.  ( T  X.  E ) )
36353impb 1201 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  s  e.  E  /\  t  e.  ( T  X.  E ) )  ->  ( s  .x.  t )  e.  ( T  X.  E ) )
37 simpl 458 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  ( T  X.  E
)  /\  f  e.  ( T  X.  E
) ) )  -> 
( K  e.  HL  /\  W  e.  H ) )
38 simpr1 1011 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  ( T  X.  E
)  /\  f  e.  ( T  X.  E
) ) )  -> 
s  e.  E )
39 simpr2 1012 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  ( T  X.  E
)  /\  f  e.  ( T  X.  E
) ) )  -> 
t  e.  ( T  X.  E ) )
40 xp1st 6774 . . . . . . . 8  |-  ( t  e.  ( T  X.  E )  ->  ( 1st `  t )  e.  T )
4139, 40syl 17 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  ( T  X.  E
)  /\  f  e.  ( T  X.  E
) ) )  -> 
( 1st `  t
)  e.  T )
42 simpr3 1013 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  ( T  X.  E
)  /\  f  e.  ( T  X.  E
) ) )  -> 
f  e.  ( T  X.  E ) )
43 xp1st 6774 . . . . . . . 8  |-  ( f  e.  ( T  X.  E )  ->  ( 1st `  f )  e.  T )
4442, 43syl 17 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  ( T  X.  E
)  /\  f  e.  ( T  X.  E
) ) )  -> 
( 1st `  f
)  e.  T )
451, 2, 3tendospdi1 34494 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  ( 1st `  t )  e.  T  /\  ( 1st `  f
)  e.  T ) )  ->  ( s `  ( ( 1st `  t
)  o.  ( 1st `  f ) ) )  =  ( ( s `
 ( 1st `  t
) )  o.  (
s `  ( 1st `  f ) ) ) )
4637, 38, 41, 44, 45syl13anc 1266 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  ( T  X.  E
)  /\  f  e.  ( T  X.  E
) ) )  -> 
( s `  (
( 1st `  t
)  o.  ( 1st `  f ) ) )  =  ( ( s `
 ( 1st `  t
) )  o.  (
s `  ( 1st `  f ) ) ) )
471, 2, 3, 4, 10, 8, 17dvhvadd 34566 . . . . . . . . . 10  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( t  e.  ( T  X.  E
)  /\  f  e.  ( T  X.  E
) ) )  -> 
( t  .+  f
)  =  <. (
( 1st `  t
)  o.  ( 1st `  f ) ) ,  ( ( 2nd `  t
)  .+^  ( 2nd `  f
) ) >. )
48473adantr1 1164 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  ( T  X.  E
)  /\  f  e.  ( T  X.  E
) ) )  -> 
( t  .+  f
)  =  <. (
( 1st `  t
)  o.  ( 1st `  f ) ) ,  ( ( 2nd `  t
)  .+^  ( 2nd `  f
) ) >. )
4948fveq2d 5822 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  ( T  X.  E
)  /\  f  e.  ( T  X.  E
) ) )  -> 
( 1st `  (
t  .+  f )
)  =  ( 1st `  <. ( ( 1st `  t )  o.  ( 1st `  f ) ) ,  ( ( 2nd `  t )  .+^  ( 2nd `  f ) ) >.
) )
50 fvex 5828 . . . . . . . . . 10  |-  ( 1st `  t )  e.  _V
51 fvex 5828 . . . . . . . . . 10  |-  ( 1st `  f )  e.  _V
5250, 51coex 6696 . . . . . . . . 9  |-  ( ( 1st `  t )  o.  ( 1st `  f
) )  e.  _V
53 ovex 6270 . . . . . . . . 9  |-  ( ( 2nd `  t ) 
.+^  ( 2nd `  f
) )  e.  _V
5452, 53op1st 6752 . . . . . . . 8  |-  ( 1st `  <. ( ( 1st `  t )  o.  ( 1st `  f ) ) ,  ( ( 2nd `  t )  .+^  ( 2nd `  f ) ) >.
)  =  ( ( 1st `  t )  o.  ( 1st `  f
) )
5549, 54syl6eq 2472 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  ( T  X.  E
)  /\  f  e.  ( T  X.  E
) ) )  -> 
( 1st `  (
t  .+  f )
)  =  ( ( 1st `  t )  o.  ( 1st `  f
) ) )
5655fveq2d 5822 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  ( T  X.  E
)  /\  f  e.  ( T  X.  E
) ) )  -> 
( s `  ( 1st `  ( t  .+  f ) ) )  =  ( s `  ( ( 1st `  t
)  o.  ( 1st `  f ) ) ) )
571, 2, 3, 4, 12dvhvsca 34575 . . . . . . . . . 10  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  ( T  X.  E
) ) )  -> 
( s  .x.  t
)  =  <. (
s `  ( 1st `  t ) ) ,  ( s  o.  ( 2nd `  t ) )
>. )
58573adantr3 1166 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  ( T  X.  E
)  /\  f  e.  ( T  X.  E
) ) )  -> 
( s  .x.  t
)  =  <. (
s `  ( 1st `  t ) ) ,  ( s  o.  ( 2nd `  t ) )
>. )
5958fveq2d 5822 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  ( T  X.  E
)  /\  f  e.  ( T  X.  E
) ) )  -> 
( 1st `  (
s  .x.  t )
)  =  ( 1st `  <. ( s `  ( 1st `  t ) ) ,  ( s  o.  ( 2nd `  t
) ) >. )
)
60 fvex 5828 . . . . . . . . 9  |-  ( s `
 ( 1st `  t
) )  e.  _V
61 vex 3019 . . . . . . . . . 10  |-  s  e. 
_V
62 fvex 5828 . . . . . . . . . 10  |-  ( 2nd `  t )  e.  _V
6361, 62coex 6696 . . . . . . . . 9  |-  ( s  o.  ( 2nd `  t
) )  e.  _V
6460, 63op1st 6752 . . . . . . . 8  |-  ( 1st `  <. ( s `  ( 1st `  t ) ) ,  ( s  o.  ( 2nd `  t
) ) >. )  =  ( s `  ( 1st `  t ) )
6559, 64syl6eq 2472 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  ( T  X.  E
)  /\  f  e.  ( T  X.  E
) ) )  -> 
( 1st `  (
s  .x.  t )
)  =  ( s `
 ( 1st `  t
) ) )
661, 2, 3, 4, 12dvhvsca 34575 . . . . . . . . . 10  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( s  .x.  f
)  =  <. (
s `  ( 1st `  f ) ) ,  ( s  o.  ( 2nd `  f ) )
>. )
67663adantr2 1165 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  ( T  X.  E
)  /\  f  e.  ( T  X.  E
) ) )  -> 
( s  .x.  f
)  =  <. (
s `  ( 1st `  f ) ) ,  ( s  o.  ( 2nd `  f ) )
>. )
6867fveq2d 5822 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  ( T  X.  E
)  /\  f  e.  ( T  X.  E
) ) )  -> 
( 1st `  (
s  .x.  f )
)  =  ( 1st `  <. ( s `  ( 1st `  f ) ) ,  ( s  o.  ( 2nd `  f
) ) >. )
)
69 fvex 5828 . . . . . . . . 9  |-  ( s `
 ( 1st `  f
) )  e.  _V
70 fvex 5828 . . . . . . . . . 10  |-  ( 2nd `  f )  e.  _V
7161, 70coex 6696 . . . . . . . . 9  |-  ( s  o.  ( 2nd `  f
) )  e.  _V
7269, 71op1st 6752 . . . . . . . 8  |-  ( 1st `  <. ( s `  ( 1st `  f ) ) ,  ( s  o.  ( 2nd `  f
) ) >. )  =  ( s `  ( 1st `  f ) )
7368, 72syl6eq 2472 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  ( T  X.  E
)  /\  f  e.  ( T  X.  E
) ) )  -> 
( 1st `  (
s  .x.  f )
)  =  ( s `
 ( 1st `  f
) ) )
7465, 73coeq12d 4954 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  ( T  X.  E
)  /\  f  e.  ( T  X.  E
) ) )  -> 
( ( 1st `  (
s  .x.  t )
)  o.  ( 1st `  ( s  .x.  f
) ) )  =  ( ( s `  ( 1st `  t ) )  o.  ( s `
 ( 1st `  f
) ) ) )
7546, 56, 743eqtr4d 2466 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  ( T  X.  E
)  /\  f  e.  ( T  X.  E
) ) )  -> 
( s `  ( 1st `  ( t  .+  f ) ) )  =  ( ( 1st `  ( s  .x.  t
) )  o.  ( 1st `  ( s  .x.  f ) ) ) )
7630adantr 466 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  ( T  X.  E
)  /\  f  e.  ( T  X.  E
) ) )  ->  D  e.  Ring )
7716adantr 466 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  ( T  X.  E
)  /\  f  e.  ( T  X.  E
) ) )  ->  E  =  ( Base `  D ) )
7838, 77eleqtrd 2502 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  ( T  X.  E
)  /\  f  e.  ( T  X.  E
) ) )  -> 
s  e.  ( Base `  D ) )
79 xp2nd 6775 . . . . . . . . . 10  |-  ( t  e.  ( T  X.  E )  ->  ( 2nd `  t )  e.  E )
8039, 79syl 17 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  ( T  X.  E
)  /\  f  e.  ( T  X.  E
) ) )  -> 
( 2nd `  t
)  e.  E )
8180, 77eleqtrd 2502 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  ( T  X.  E
)  /\  f  e.  ( T  X.  E
) ) )  -> 
( 2nd `  t
)  e.  ( Base `  D ) )
82 xp2nd 6775 . . . . . . . . . 10  |-  ( f  e.  ( T  X.  E )  ->  ( 2nd `  f )  e.  E )
8342, 82syl 17 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  ( T  X.  E
)  /\  f  e.  ( T  X.  E
) ) )  -> 
( 2nd `  f
)  e.  E )
8483, 77eleqtrd 2502 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  ( T  X.  E
)  /\  f  e.  ( T  X.  E
) ) )  -> 
( 2nd `  f
)  e.  ( Base `  D ) )
8514, 17, 19ringdi 17735 . . . . . . . 8  |-  ( ( D  e.  Ring  /\  (
s  e.  ( Base `  D )  /\  ( 2nd `  t )  e.  ( Base `  D
)  /\  ( 2nd `  f )  e.  (
Base `  D )
) )  ->  (
s  .X.  ( ( 2nd `  t )  .+^  ( 2nd `  f ) ) )  =  ( ( s  .X.  ( 2nd `  t ) ) 
.+^  ( s  .X.  ( 2nd `  f ) ) ) )
8676, 78, 81, 84, 85syl13anc 1266 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  ( T  X.  E
)  /\  f  e.  ( T  X.  E
) ) )  -> 
( s  .X.  (
( 2nd `  t
)  .+^  ( 2nd `  f
) ) )  =  ( ( s  .X.  ( 2nd `  t ) )  .+^  ( s  .X.  ( 2nd `  f
) ) ) )
8714, 17ringacl 17744 . . . . . . . . . 10  |-  ( ( D  e.  Ring  /\  ( 2nd `  t )  e.  ( Base `  D
)  /\  ( 2nd `  f )  e.  (
Base `  D )
)  ->  ( ( 2nd `  t )  .+^  ( 2nd `  f ) )  e.  ( Base `  D ) )
8876, 81, 84, 87syl3anc 1264 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  ( T  X.  E
)  /\  f  e.  ( T  X.  E
) ) )  -> 
( ( 2nd `  t
)  .+^  ( 2nd `  f
) )  e.  (
Base `  D )
)
8988, 77eleqtrrd 2503 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  ( T  X.  E
)  /\  f  e.  ( T  X.  E
) ) )  -> 
( ( 2nd `  t
)  .+^  ( 2nd `  f
) )  e.  E
)
901, 2, 3, 4, 10, 19dvhmulr 34560 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  ( ( 2nd `  t ) 
.+^  ( 2nd `  f
) )  e.  E
) )  ->  (
s  .X.  ( ( 2nd `  t )  .+^  ( 2nd `  f ) ) )  =  ( s  o.  ( ( 2nd `  t ) 
.+^  ( 2nd `  f
) ) ) )
9137, 38, 89, 90syl12anc 1262 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  ( T  X.  E
)  /\  f  e.  ( T  X.  E
) ) )  -> 
( s  .X.  (
( 2nd `  t
)  .+^  ( 2nd `  f
) ) )  =  ( s  o.  (
( 2nd `  t
)  .+^  ( 2nd `  f
) ) ) )
921, 2, 3, 4, 10, 19dvhmulr 34560 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  ( 2nd `  t )  e.  E
) )  ->  (
s  .X.  ( 2nd `  t ) )  =  ( s  o.  ( 2nd `  t ) ) )
9337, 38, 80, 92syl12anc 1262 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  ( T  X.  E
)  /\  f  e.  ( T  X.  E
) ) )  -> 
( s  .X.  ( 2nd `  t ) )  =  ( s  o.  ( 2nd `  t
) ) )
941, 2, 3, 4, 10, 19dvhmulr 34560 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  ( 2nd `  f )  e.  E
) )  ->  (
s  .X.  ( 2nd `  f ) )  =  ( s  o.  ( 2nd `  f ) ) )
9537, 38, 83, 94syl12anc 1262 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  ( T  X.  E
)  /\  f  e.  ( T  X.  E
) ) )  -> 
( s  .X.  ( 2nd `  f ) )  =  ( s  o.  ( 2nd `  f
) ) )
9693, 95oveq12d 6260 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  ( T  X.  E
)  /\  f  e.  ( T  X.  E
) ) )  -> 
( ( s  .X.  ( 2nd `  t ) )  .+^  ( s  .X.  ( 2nd `  f
) ) )  =  ( ( s  o.  ( 2nd `  t
) )  .+^  ( s  o.  ( 2nd `  f
) ) ) )
9786, 91, 963eqtr3d 2464 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  ( T  X.  E
)  /\  f  e.  ( T  X.  E
) ) )  -> 
( s  o.  (
( 2nd `  t
)  .+^  ( 2nd `  f
) ) )  =  ( ( s  o.  ( 2nd `  t
) )  .+^  ( s  o.  ( 2nd `  f
) ) ) )
9848fveq2d 5822 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  ( T  X.  E
)  /\  f  e.  ( T  X.  E
) ) )  -> 
( 2nd `  (
t  .+  f )
)  =  ( 2nd `  <. ( ( 1st `  t )  o.  ( 1st `  f ) ) ,  ( ( 2nd `  t )  .+^  ( 2nd `  f ) ) >.
) )
9952, 53op2nd 6753 . . . . . . . 8  |-  ( 2nd `  <. ( ( 1st `  t )  o.  ( 1st `  f ) ) ,  ( ( 2nd `  t )  .+^  ( 2nd `  f ) ) >.
)  =  ( ( 2nd `  t ) 
.+^  ( 2nd `  f
) )
10098, 99syl6eq 2472 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  ( T  X.  E
)  /\  f  e.  ( T  X.  E
) ) )  -> 
( 2nd `  (
t  .+  f )
)  =  ( ( 2nd `  t ) 
.+^  ( 2nd `  f
) ) )
101100coeq2d 4952 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  ( T  X.  E
)  /\  f  e.  ( T  X.  E
) ) )  -> 
( s  o.  ( 2nd `  ( t  .+  f ) ) )  =  ( s  o.  ( ( 2nd `  t
)  .+^  ( 2nd `  f
) ) ) )
10258fveq2d 5822 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  ( T  X.  E
)  /\  f  e.  ( T  X.  E
) ) )  -> 
( 2nd `  (
s  .x.  t )
)  =  ( 2nd `  <. ( s `  ( 1st `  t ) ) ,  ( s  o.  ( 2nd `  t
) ) >. )
)
10360, 63op2nd 6753 . . . . . . . 8  |-  ( 2nd `  <. ( s `  ( 1st `  t ) ) ,  ( s  o.  ( 2nd `  t
) ) >. )  =  ( s  o.  ( 2nd `  t
) )
104102, 103syl6eq 2472 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  ( T  X.  E
)  /\  f  e.  ( T  X.  E
) ) )  -> 
( 2nd `  (
s  .x.  t )
)  =  ( s  o.  ( 2nd `  t
) ) )
10567fveq2d 5822 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  ( T  X.  E
)  /\  f  e.  ( T  X.  E
) ) )  -> 
( 2nd `  (
s  .x.  f )
)  =  ( 2nd `  <. ( s `  ( 1st `  f ) ) ,  ( s  o.  ( 2nd `  f
) ) >. )
)
10669, 71op2nd 6753 . . . . . . . 8  |-  ( 2nd `  <. ( s `  ( 1st `  f ) ) ,  ( s  o.  ( 2nd `  f
) ) >. )  =  ( s  o.  ( 2nd `  f
) )
107105, 106syl6eq 2472 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  ( T  X.  E
)  /\  f  e.  ( T  X.  E
) ) )  -> 
( 2nd `  (
s  .x.  f )
)  =  ( s  o.  ( 2nd `  f
) ) )
108104, 107oveq12d 6260 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  ( T  X.  E
)  /\  f  e.  ( T  X.  E
) ) )  -> 
( ( 2nd `  (
s  .x.  t )
)  .+^  ( 2nd `  (
s  .x.  f )
) )  =  ( ( s  o.  ( 2nd `  t ) ) 
.+^  ( s  o.  ( 2nd `  f
) ) ) )
10997, 101, 1083eqtr4d 2466 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  ( T  X.  E
)  /\  f  e.  ( T  X.  E
) ) )  -> 
( s  o.  ( 2nd `  ( t  .+  f ) ) )  =  ( ( 2nd `  ( s  .x.  t
) )  .+^  ( 2nd `  ( s  .x.  f
) ) ) )
11075, 109opeq12d 4131 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  ( T  X.  E
)  /\  f  e.  ( T  X.  E
) ) )  ->  <. ( s `  ( 1st `  ( t  .+  f ) ) ) ,  ( s  o.  ( 2nd `  (
t  .+  f )
) ) >.  =  <. ( ( 1st `  (
s  .x.  t )
)  o.  ( 1st `  ( s  .x.  f
) ) ) ,  ( ( 2nd `  (
s  .x.  t )
)  .+^  ( 2nd `  (
s  .x.  f )
) ) >. )
1111, 2, 3, 4, 10, 17, 8dvhvaddcl 34569 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( t  e.  ( T  X.  E
)  /\  f  e.  ( T  X.  E
) ) )  -> 
( t  .+  f
)  e.  ( T  X.  E ) )
1121113adantr1 1164 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  ( T  X.  E
)  /\  f  e.  ( T  X.  E
) ) )  -> 
( t  .+  f
)  e.  ( T  X.  E ) )
1131, 2, 3, 4, 12dvhvsca 34575 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  ( t 
.+  f )  e.  ( T  X.  E
) ) )  -> 
( s  .x.  (
t  .+  f )
)  =  <. (
s `  ( 1st `  ( t  .+  f
) ) ) ,  ( s  o.  ( 2nd `  ( t  .+  f ) ) )
>. )
11437, 38, 112, 113syl12anc 1262 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  ( T  X.  E
)  /\  f  e.  ( T  X.  E
) ) )  -> 
( s  .x.  (
t  .+  f )
)  =  <. (
s `  ( 1st `  ( t  .+  f
) ) ) ,  ( s  o.  ( 2nd `  ( t  .+  f ) ) )
>. )
115353adantr3 1166 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  ( T  X.  E
)  /\  f  e.  ( T  X.  E
) ) )  -> 
( s  .x.  t
)  e.  ( T  X.  E ) )
1161, 2, 3, 4, 12dvhvscacl 34577 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( s  .x.  f
)  e.  ( T  X.  E ) )
1171163adantr2 1165 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  ( T  X.  E
)  /\  f  e.  ( T  X.  E
) ) )  -> 
( s  .x.  f
)  e.  ( T  X.  E ) )
1181, 2, 3, 4, 10, 8, 17dvhvadd 34566 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( s 
.x.  t )  e.  ( T  X.  E
)  /\  ( s  .x.  f )  e.  ( T  X.  E ) ) )  ->  (
( s  .x.  t
)  .+  ( s  .x.  f ) )  = 
<. ( ( 1st `  (
s  .x.  t )
)  o.  ( 1st `  ( s  .x.  f
) ) ) ,  ( ( 2nd `  (
s  .x.  t )
)  .+^  ( 2nd `  (
s  .x.  f )
) ) >. )
11937, 115, 117, 118syl12anc 1262 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  ( T  X.  E
)  /\  f  e.  ( T  X.  E
) ) )  -> 
( ( s  .x.  t )  .+  (
s  .x.  f )
)  =  <. (
( 1st `  (
s  .x.  t )
)  o.  ( 1st `  ( s  .x.  f
) ) ) ,  ( ( 2nd `  (
s  .x.  t )
)  .+^  ( 2nd `  (
s  .x.  f )
) ) >. )
120110, 114, 1193eqtr4d 2466 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  ( T  X.  E
)  /\  f  e.  ( T  X.  E
) ) )  -> 
( s  .x.  (
t  .+  f )
)  =  ( ( s  .x.  t ) 
.+  ( s  .x.  f ) ) )
121 simpl 458 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( K  e.  HL  /\  W  e.  H ) )
122 simpr1 1011 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
s  e.  E )
123 simpr2 1012 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
t  e.  E )
124 simpr3 1013 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
f  e.  ( T  X.  E ) )
125124, 43syl 17 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( 1st `  f
)  e.  T )
126 eqid 2422 . . . . . . . 8  |-  ( +g  `  ( ( EDRing `  K
) `  W )
)  =  ( +g  `  ( ( EDRing `  K
) `  W )
)
1271, 2, 3, 21, 126erngplus2 34277 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  ( 1st `  f )  e.  T
) )  ->  (
( s ( +g  `  ( ( EDRing `  K
) `  W )
) t ) `  ( 1st `  f ) )  =  ( ( s `  ( 1st `  f ) )  o.  ( t `  ( 1st `  f ) ) ) )
128121, 122, 123, 125, 127syl13anc 1266 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( ( s ( +g  `  ( (
EDRing `  K ) `  W ) ) t ) `  ( 1st `  f ) )  =  ( ( s `  ( 1st `  f ) )  o.  ( t `
 ( 1st `  f
) ) ) )
12922fveq2d 5822 . . . . . . . . . 10  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  ( +g  `  D
)  =  ( +g  `  ( ( EDRing `  K
) `  W )
) )
13017, 129syl5eq 2468 . . . . . . . . 9  |-  ( ( K  e.  HL  /\  W  e.  H )  -> 
.+^  =  ( +g  `  ( ( EDRing `  K
) `  W )
) )
131130oveqd 6259 . . . . . . . 8  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  ( s  .+^  t )  =  ( s ( +g  `  ( (
EDRing `  K ) `  W ) ) t ) )
132131fveq1d 5820 . . . . . . 7  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  ( ( s  .+^  t ) `  ( 1st `  f ) )  =  ( ( s ( +g  `  (
( EDRing `  K ) `  W ) ) t ) `  ( 1st `  f ) ) )
133132adantr 466 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( ( s  .+^  t ) `  ( 1st `  f ) )  =  ( ( s ( +g  `  (
( EDRing `  K ) `  W ) ) t ) `  ( 1st `  f ) ) )
134663adantr2 1165 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( s  .x.  f
)  =  <. (
s `  ( 1st `  f ) ) ,  ( s  o.  ( 2nd `  f ) )
>. )
135134fveq2d 5822 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( 1st `  (
s  .x.  f )
)  =  ( 1st `  <. ( s `  ( 1st `  f ) ) ,  ( s  o.  ( 2nd `  f
) ) >. )
)
136135, 72syl6eq 2472 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( 1st `  (
s  .x.  f )
)  =  ( s `
 ( 1st `  f
) ) )
1371, 2, 3, 4, 12dvhvsca 34575 . . . . . . . . . 10  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( t  .x.  f
)  =  <. (
t `  ( 1st `  f ) ) ,  ( t  o.  ( 2nd `  f ) )
>. )
1381373adantr1 1164 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( t  .x.  f
)  =  <. (
t `  ( 1st `  f ) ) ,  ( t  o.  ( 2nd `  f ) )
>. )
139138fveq2d 5822 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( 1st `  (
t  .x.  f )
)  =  ( 1st `  <. ( t `  ( 1st `  f ) ) ,  ( t  o.  ( 2nd `  f
) ) >. )
)
140 fvex 5828 . . . . . . . . 9  |-  ( t `
 ( 1st `  f
) )  e.  _V
141 vex 3019 . . . . . . . . . 10  |-  t  e. 
_V
142141, 70coex 6696 . . . . . . . . 9  |-  ( t  o.  ( 2nd `  f
) )  e.  _V
143140, 142op1st 6752 . . . . . . . 8  |-  ( 1st `  <. ( t `  ( 1st `  f ) ) ,  ( t  o.  ( 2nd `  f
) ) >. )  =  ( t `  ( 1st `  f ) )
144139, 143syl6eq 2472 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( 1st `  (
t  .x.  f )
)  =  ( t `
 ( 1st `  f
) ) )
145136, 144coeq12d 4954 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( ( 1st `  (
s  .x.  f )
)  o.  ( 1st `  ( t  .x.  f
) ) )  =  ( ( s `  ( 1st `  f ) )  o.  ( t `
 ( 1st `  f
) ) ) )
146128, 133, 1453eqtr4d 2466 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( ( s  .+^  t ) `  ( 1st `  f ) )  =  ( ( 1st `  ( s  .x.  f
) )  o.  ( 1st `  ( t  .x.  f ) ) ) )
14730adantr 466 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  ->  D  e.  Ring )
14816adantr 466 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  ->  E  =  ( Base `  D ) )
149122, 148eleqtrd 2502 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
s  e.  ( Base `  D ) )
150123, 148eleqtrd 2502 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
t  e.  ( Base `  D ) )
151124, 82syl 17 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( 2nd `  f
)  e.  E )
152151, 148eleqtrd 2502 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( 2nd `  f
)  e.  ( Base `  D ) )
15314, 17, 19ringdir 17736 . . . . . . . 8  |-  ( ( D  e.  Ring  /\  (
s  e.  ( Base `  D )  /\  t  e.  ( Base `  D
)  /\  ( 2nd `  f )  e.  (
Base `  D )
) )  ->  (
( s  .+^  t ) 
.X.  ( 2nd `  f
) )  =  ( ( s  .X.  ( 2nd `  f ) ) 
.+^  ( t  .X.  ( 2nd `  f ) ) ) )
154147, 149, 150, 152, 153syl13anc 1266 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( ( s  .+^  t )  .X.  ( 2nd `  f ) )  =  ( ( s 
.X.  ( 2nd `  f
) )  .+^  ( t 
.X.  ( 2nd `  f
) ) ) )
15514, 17ringacl 17744 . . . . . . . . . 10  |-  ( ( D  e.  Ring  /\  s  e.  ( Base `  D
)  /\  t  e.  ( Base `  D )
)  ->  ( s  .+^  t )  e.  (
Base `  D )
)
156147, 149, 150, 155syl3anc 1264 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( s  .+^  t )  e.  ( Base `  D
) )
157156, 148eleqtrrd 2503 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( s  .+^  t )  e.  E )
1581, 2, 3, 4, 10, 19dvhmulr 34560 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( s 
.+^  t )  e.  E  /\  ( 2nd `  f )  e.  E
) )  ->  (
( s  .+^  t ) 
.X.  ( 2nd `  f
) )  =  ( ( s  .+^  t )  o.  ( 2nd `  f
) ) )
159121, 157, 151, 158syl12anc 1262 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( ( s  .+^  t )  .X.  ( 2nd `  f ) )  =  ( ( s 
.+^  t )  o.  ( 2nd `  f
) ) )
160121, 122, 151, 94syl12anc 1262 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( s  .X.  ( 2nd `  f ) )  =  ( s  o.  ( 2nd `  f
) ) )
1611, 2, 3, 4, 10, 19dvhmulr 34560 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( t  e.  E  /\  ( 2nd `  f )  e.  E
) )  ->  (
t  .X.  ( 2nd `  f ) )  =  ( t  o.  ( 2nd `  f ) ) )
162121, 123, 151, 161syl12anc 1262 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( t  .X.  ( 2nd `  f ) )  =  ( t  o.  ( 2nd `  f
) ) )
163160, 162oveq12d 6260 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( ( s  .X.  ( 2nd `  f ) )  .+^  ( t  .X.  ( 2nd `  f
) ) )  =  ( ( s  o.  ( 2nd `  f
) )  .+^  ( t  o.  ( 2nd `  f
) ) ) )
164154, 159, 1633eqtr3d 2464 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( ( s  .+^  t )  o.  ( 2nd `  f ) )  =  ( ( s  o.  ( 2nd `  f
) )  .+^  ( t  o.  ( 2nd `  f
) ) ) )
165134fveq2d 5822 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( 2nd `  (
s  .x.  f )
)  =  ( 2nd `  <. ( s `  ( 1st `  f ) ) ,  ( s  o.  ( 2nd `  f
) ) >. )
)
166165, 106syl6eq 2472 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( 2nd `  (
s  .x.  f )
)  =  ( s  o.  ( 2nd `  f
) ) )
167138fveq2d 5822 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( 2nd `  (
t  .x.  f )
)  =  ( 2nd `  <. ( t `  ( 1st `  f ) ) ,  ( t  o.  ( 2nd `  f
) ) >. )
)
168140, 142op2nd 6753 . . . . . . . 8  |-  ( 2nd `  <. ( t `  ( 1st `  f ) ) ,  ( t  o.  ( 2nd `  f
) ) >. )  =  ( t  o.  ( 2nd `  f
) )
169167, 168syl6eq 2472 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( 2nd `  (
t  .x.  f )
)  =  ( t  o.  ( 2nd `  f
) ) )
170166, 169oveq12d 6260 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( ( 2nd `  (
s  .x.  f )
)  .+^  ( 2nd `  (
t  .x.  f )
) )  =  ( ( s  o.  ( 2nd `  f ) ) 
.+^  ( t  o.  ( 2nd `  f
) ) ) )
171164, 170eqtr4d 2459 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( ( s  .+^  t )  o.  ( 2nd `  f ) )  =  ( ( 2nd `  ( s  .x.  f
) )  .+^  ( 2nd `  ( t  .x.  f
) ) ) )
172146, 171opeq12d 4131 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  ->  <. ( ( s  .+^  t ) `  ( 1st `  f ) ) ,  ( ( s 
.+^  t )  o.  ( 2nd `  f
) ) >.  =  <. ( ( 1st `  (
s  .x.  f )
)  o.  ( 1st `  ( t  .x.  f
) ) ) ,  ( ( 2nd `  (
s  .x.  f )
)  .+^  ( 2nd `  (
t  .x.  f )
) ) >. )
1731, 2, 3, 4, 12dvhvsca 34575 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( s 
.+^  t )  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( ( s  .+^  t )  .x.  f
)  =  <. (
( s  .+^  t ) `
 ( 1st `  f
) ) ,  ( ( s  .+^  t )  o.  ( 2nd `  f
) ) >. )
174121, 157, 124, 173syl12anc 1262 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( ( s  .+^  t )  .x.  f
)  =  <. (
( s  .+^  t ) `
 ( 1st `  f
) ) ,  ( ( s  .+^  t )  o.  ( 2nd `  f
) ) >. )
1751163adantr2 1165 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( s  .x.  f
)  e.  ( T  X.  E ) )
1761, 2, 3, 4, 12dvhvscacl 34577 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( t  .x.  f
)  e.  ( T  X.  E ) )
1771763adantr1 1164 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( t  .x.  f
)  e.  ( T  X.  E ) )
1781, 2, 3, 4, 10, 8, 17dvhvadd 34566 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( s 
.x.  f )  e.  ( T  X.  E
)  /\  ( t  .x.  f )  e.  ( T  X.  E ) ) )  ->  (
( s  .x.  f
)  .+  ( t  .x.  f ) )  = 
<. ( ( 1st `  (
s  .x.  f )
)  o.  ( 1st `  ( t  .x.  f
) ) ) ,  ( ( 2nd `  (
s  .x.  f )
)  .+^  ( 2nd `  (
t  .x.  f )
) ) >. )
179121, 175, 177, 178syl12anc 1262 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( ( s  .x.  f )  .+  (
t  .x.  f )
)  =  <. (
( 1st `  (
s  .x.  f )
)  o.  ( 1st `  ( t  .x.  f
) ) ) ,  ( ( 2nd `  (
s  .x.  f )
)  .+^  ( 2nd `  (
t  .x.  f )
) ) >. )
180172, 174, 1793eqtr4d 2466 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( ( s  .+^  t )  .x.  f
)  =  ( ( s  .x.  f ) 
.+  ( t  .x.  f ) ) )
1811, 2, 3tendocoval 34239 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E )  /\  ( 1st `  f )  e.  T )  ->  (
( s  o.  t
) `  ( 1st `  f ) )  =  ( s `  (
t `  ( 1st `  f ) ) ) )
182121, 122, 123, 125, 181syl121anc 1269 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( ( s  o.  t ) `  ( 1st `  f ) )  =  ( s `  ( t `  ( 1st `  f ) ) ) )
183 coass 5309 . . . . . . 7  |-  ( ( s  o.  t )  o.  ( 2nd `  f
) )  =  ( s  o.  ( t  o.  ( 2nd `  f
) ) )
184183a1i 11 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( ( s  o.  t )  o.  ( 2nd `  f ) )  =  ( s  o.  ( t  o.  ( 2nd `  f ) ) ) )
185182, 184opeq12d 4131 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  ->  <. ( ( s  o.  t ) `  ( 1st `  f ) ) ,  ( ( s  o.  t )  o.  ( 2nd `  f
) ) >.  =  <. ( s `  ( t `
 ( 1st `  f
) ) ) ,  ( s  o.  (
t  o.  ( 2nd `  f ) ) )
>. )
1861, 3tendococl 34245 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  s  e.  E  /\  t  e.  E
)  ->  ( s  o.  t )  e.  E
)
187121, 122, 123, 186syl3anc 1264 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( s  o.  t
)  e.  E )
1881, 2, 3, 4, 12dvhvsca 34575 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( s  o.  t )  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( ( s  o.  t )  .x.  f
)  =  <. (
( s  o.  t
) `  ( 1st `  f ) ) ,  ( ( s  o.  t )  o.  ( 2nd `  f ) )
>. )
189121, 187, 124, 188syl12anc 1262 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( ( s  o.  t )  .x.  f
)  =  <. (
( s  o.  t
) `  ( 1st `  f ) ) ,  ( ( s  o.  t )  o.  ( 2nd `  f ) )
>. )
1901, 2, 3tendocl 34240 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  t  e.  E  /\  ( 1st `  f
)  e.  T )  ->  ( t `  ( 1st `  f ) )  e.  T )
191121, 123, 125, 190syl3anc 1264 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( t `  ( 1st `  f ) )  e.  T )
1921, 3tendococl 34245 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  t  e.  E  /\  ( 2nd `  f
)  e.  E )  ->  ( t  o.  ( 2nd `  f
) )  e.  E
)
193121, 123, 151, 192syl3anc 1264 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( t  o.  ( 2nd `  f ) )  e.  E )
1941, 2, 3, 4, 12dvhopvsca 34576 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  ( t `
 ( 1st `  f
) )  e.  T  /\  ( t  o.  ( 2nd `  f ) )  e.  E ) )  ->  ( s  .x.  <.
( t `  ( 1st `  f ) ) ,  ( t  o.  ( 2nd `  f
) ) >. )  =  <. ( s `  ( t `  ( 1st `  f ) ) ) ,  ( s  o.  ( t  o.  ( 2nd `  f
) ) ) >.
)
195121, 122, 191, 193, 194syl13anc 1266 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( s  .x.  <. (
t `  ( 1st `  f ) ) ,  ( t  o.  ( 2nd `  f ) )
>. )  =  <. ( s `  ( t `
 ( 1st `  f
) ) ) ,  ( s  o.  (
t  o.  ( 2nd `  f ) ) )
>. )
196185, 189, 1953eqtr4d 2466 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( ( s  o.  t )  .x.  f
)  =  ( s 
.x.  <. ( t `  ( 1st `  f ) ) ,  ( t  o.  ( 2nd `  f
) ) >. )
)
1971, 2, 3, 4, 10, 19dvhmulr 34560 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E ) )  -> 
( s  .X.  t
)  =  ( s  o.  t ) )
1981973adantr3 1166 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( s  .X.  t
)  =  ( s  o.  t ) )
199198oveq1d 6257 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( ( s  .X.  t )  .x.  f
)  =  ( ( s  o.  t ) 
.x.  f ) )
200138oveq2d 6258 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( s  .x.  (
t  .x.  f )
)  =  ( s 
.x.  <. ( t `  ( 1st `  f ) ) ,  ( t  o.  ( 2nd `  f
) ) >. )
)
201196, 199, 2003eqtr4d 2466 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( ( s  .X.  t )  .x.  f
)  =  ( s 
.x.  ( t  .x.  f ) ) )
202 xp1st 6774 . . . . . . 7  |-  ( s  e.  ( T  X.  E )  ->  ( 1st `  s )  e.  T )
203202adantl 467 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  s  e.  ( T  X.  E ) )  ->  ( 1st `  s )  e.  T
)
204 tendospid 34491 . . . . . 6  |-  ( ( 1st `  s )  e.  T  ->  (
(  _I  |`  T ) `
 ( 1st `  s
) )  =  ( 1st `  s ) )
205203, 204syl 17 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  s  e.  ( T  X.  E ) )  ->  ( (  _I  |`  T ) `  ( 1st `  s ) )  =  ( 1st `  s ) )
206 xp2nd 6775 . . . . . . 7  |-  ( s  e.  ( T  X.  E )  ->  ( 2nd `  s )  e.  E )
2071, 2, 3tendof 34236 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( 2nd `  s
)  e.  E )  ->  ( 2nd `  s
) : T --> T )
208206, 207sylan2 476 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  s  e.  ( T  X.  E ) )  ->  ( 2nd `  s ) : T --> T )
209 fcoi2 5711 . . . . . 6  |-  ( ( 2nd `  s ) : T --> T  -> 
( (  _I  |`  T )  o.  ( 2nd `  s
) )  =  ( 2nd `  s ) )
210208, 209syl 17 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  s  e.  ( T  X.  E ) )  ->  ( (  _I  |`  T )  o.  ( 2nd `  s
) )  =  ( 2nd `  s ) )
211205, 210opeq12d 4131 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  s  e.  ( T  X.  E ) )  ->  <. ( (  _I  |`  T ) `  ( 1st `  s
) ) ,  ( (  _I  |`  T )  o.  ( 2nd `  s
) ) >.  =  <. ( 1st `  s ) ,  ( 2nd `  s
) >. )
2121, 2, 3tendoidcl 34242 . . . . . 6  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  (  _I  |`  T )  e.  E )
213212anim1i 570 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  s  e.  ( T  X.  E ) )  ->  ( (  _I  |`  T )  e.  E  /\  s  e.  ( T  X.  E
) ) )
2141, 2, 3, 4, 12dvhvsca 34575 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( (  _I  |`  T )  e.  E  /\  s  e.  ( T  X.  E ) ) )  ->  ( (  _I  |`  T )  .x.  s )  =  <. ( (  _I  |`  T ) `
 ( 1st `  s
) ) ,  ( (  _I  |`  T )  o.  ( 2nd `  s
) ) >. )
215213, 214syldan 472 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  s  e.  ( T  X.  E ) )  ->  ( (  _I  |`  T )  .x.  s )  =  <. ( (  _I  |`  T ) `
 ( 1st `  s
) ) ,  ( (  _I  |`  T )  o.  ( 2nd `  s
) ) >. )
216 1st2nd2 6781 . . . . 5  |-  ( s  e.  ( T  X.  E )  ->  s  =  <. ( 1st `  s
) ,  ( 2nd `  s ) >. )
217216adantl 467 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  s  e.  ( T  X.  E ) )  ->  s  =  <. ( 1st `  s
) ,  ( 2nd `  s ) >. )
218211, 215, 2173eqtr4d 2466 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  s  e.  ( T  X.  E ) )  ->  ( (  _I  |`  T )  .x.  s )  =  s )
2197, 9, 11, 13, 16, 18, 20, 26, 30, 34, 36, 120, 180, 201, 218islmodd 18033 . 2  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  U  e.  LMod )
22010islvec 18263 . 2  |-  ( U  e.  LVec  <->  ( U  e. 
LMod  /\  D  e.  DivRing ) )
221219, 28, 220sylanbrc 668 1  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  U  e.  LVec )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982    = wceq 1437    e. wcel 1872   <.cop 3940    _I cid 4699    X. cxp 4787    |` cres 4791    o. ccom 4793   -->wf 5533   ` cfv 5537  (class class class)co 6242   1stc1st 6742   2ndc2nd 6743   Basecbs 15057   +g cplusg 15126   .rcmulr 15127  Scalarcsca 15129   .scvsca 15130   0gc0g 15274   invgcminusg 16606   1rcur 17671   Ringcrg 17716   DivRingcdr 17911   LModclmod 18027   LVecclvec 18261   HLchlt 32822   LHypclh 33455   LTrncltrn 33572   TEndoctendo 34225   EDRingcedring 34226   DVecHcdvh 34552
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2402  ax-rep 4472  ax-sep 4482  ax-nul 4491  ax-pow 4538  ax-pr 4596  ax-un 6534  ax-cnex 9539  ax-resscn 9540  ax-1cn 9541  ax-icn 9542  ax-addcl 9543  ax-addrcl 9544  ax-mulcl 9545  ax-mulrcl 9546  ax-mulcom 9547  ax-addass 9548  ax-mulass 9549  ax-distr 9550  ax-i2m1 9551  ax-1ne0 9552  ax-1rid 9553  ax-rnegex 9554  ax-rrecex 9555  ax-cnre 9556  ax-pre-lttri 9557  ax-pre-lttrn 9558  ax-pre-ltadd 9559  ax-pre-mulgt0 9560  ax-riotaBAD 32431
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-fal 1443  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2274  df-mo 2275  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2552  df-ne 2595  df-nel 2596  df-ral 2713  df-rex 2714  df-reu 2715  df-rmo 2716  df-rab 2717  df-v 3018  df-sbc 3236  df-csb 3332  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-pss 3388  df-nul 3698  df-if 3848  df-pw 3919  df-sn 3935  df-pr 3937  df-tp 3939  df-op 3941  df-uni 4156  df-int 4192  df-iun 4237  df-iin 4238  df-br 4360  df-opab 4419  df-mpt 4420  df-tr 4455  df-eprel 4700  df-id 4704  df-po 4710  df-so 4711  df-fr 4748  df-we 4750  df-xp 4795  df-rel 4796  df-cnv 4797  df-co 4798  df-dm 4799  df-rn 4800  df-res 4801  df-ima 4802  df-pred 5335  df-ord 5381  df-on 5382  df-lim 5383  df-suc 5384  df-iota 5501  df-fun 5539  df-fn 5540  df-f 5541  df-f1 5542  df-fo 5543  df-f1o 5544  df-fv 5545  df-riota 6204  df-ov 6245  df-oprab 6246  df-mpt2 6247  df-om 6644  df-1st 6744  df-2nd 6745  df-tpos 6921  df-undef 6968  df-wrecs 6976  df-recs 7038  df-rdg 7076  df-1o 7130  df-oadd 7134  df-er 7311  df-map 7422  df-en 7518  df-dom 7519  df-sdom 7520  df-fin 7521  df-pnf 9621  df-mnf 9622  df-xr 9623  df-ltxr 9624  df-le 9625  df-sub 9806  df-neg 9807  df-nn 10554  df-2 10612  df-3 10613  df-4 10614  df-5 10615  df-6 10616  df-n0 10814  df-z 10882  df-uz 11104  df-fz 11729  df-struct 15059  df-ndx 15060  df-slot 15061  df-base 15062  df-sets 15063  df-ress 15064  df-plusg 15139  df-mulr 15140  df-sca 15142  df-vsca 15143  df-0g 15276  df-preset 16109  df-poset 16127  df-plt 16140  df-lub 16156  df-glb 16157  df-join 16158  df-meet 16159  df-p0 16221  df-p1 16222  df-lat 16228  df-clat 16290  df-mgm 16424  df-sgrp 16463  df-mnd 16473  df-grp 16609  df-minusg 16610  df-mgp 17660  df-ur 17672  df-ring 17718  df-oppr 17787  df-dvdsr 17805  df-unit 17806  df-invr 17836  df-dvr 17847  df-drng 17913  df-lmod 18029  df-lvec 18262  df-oposet 32648  df-ol 32650  df-oml 32651  df-covers 32738  df-ats 32739  df-atl 32770  df-cvlat 32794  df-hlat 32823  df-llines 32969  df-lplanes 32970  df-lvols 32971  df-lines 32972  df-psubsp 32974  df-pmap 32975  df-padd 33267  df-lhyp 33459  df-laut 33460  df-ldil 33575  df-ltrn 33576  df-trl 33631  df-tendo 34228  df-edring 34230  df-dvech 34553
This theorem is referenced by:  dvhlvec  34583
  Copyright terms: Public domain W3C validator