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

Theorem dvhlveclem 34772
Description: Lemma for dvhlvec 34773. 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 2443 . . . . 5  |-  ( Base `  U )  =  (
Base `  U )
61, 2, 3, 4, 5dvhvbase 34751 . . . 4  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  ( Base `  U
)  =  ( T  X.  E ) )
76eqcomd 2448 . . 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 2443 . . . . 5  |-  ( Base `  D )  =  (
Base `  D )
151, 3, 4, 10, 14dvhbase 34747 . . . 4  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  ( Base `  D
)  =  E )
1615eqcomd 2448 . . 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 2443 . . . . . 6  |-  ( (
EDRing `  K ) `  W )  =  ( ( EDRing `  K ) `  W )
221, 21, 4, 10dvhsca 34746 . . . . 5  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  D  =  ( (
EDRing `  K ) `  W ) )
2322fveq2d 5710 . . . 4  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  ( 1r `  D
)  =  ( 1r
`  ( ( EDRing `  K ) `  W
) ) )
24 eqid 2443 . . . . 5  |-  ( 1r
`  ( ( EDRing `  K ) `  W
) )  =  ( 1r `  ( (
EDRing `  K ) `  W ) )
251, 2, 21, 24erng1r 34658 . . . 4  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  ( 1r `  (
( EDRing `  K ) `  W ) )  =  (  _I  |`  T ) )
2623, 25eqtr2d 2476 . . 3  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  (  _I  |`  T )  =  ( 1r `  D ) )
271, 21erngdv 34656 . . . . 5  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  ( ( EDRing `  K
) `  W )  e.  DivRing )
2822, 27eqeltrd 2517 . . . 4  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  D  e.  DivRing )
29 drngrng 16854 . . . 4  |-  ( D  e.  DivRing  ->  D  e.  Ring )
3028, 29syl 16 . . 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 34771 . . 3  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  U  e.  Grp )
351, 2, 3, 4, 12dvhvscacl 34767 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  ( T  X.  E
) ) )  -> 
( s  .x.  t
)  e.  ( T  X.  E ) )
36353impb 1183 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  s  e.  E  /\  t  e.  ( T  X.  E ) )  ->  ( s  .x.  t )  e.  ( T  X.  E ) )
37 simpl 457 . . . . . . 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 994 . . . . . . 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 995 . . . . . . . 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 6621 . . . . . . . 8  |-  ( t  e.  ( T  X.  E )  ->  ( 1st `  t )  e.  T )
4139, 40syl 16 . . . . . . 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 996 . . . . . . . 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 6621 . . . . . . . 8  |-  ( f  e.  ( T  X.  E )  ->  ( 1st `  f )  e.  T )
4442, 43syl 16 . . . . . . 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 34684 . . . . . . 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 1220 . . . . . 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 34756 . . . . . . . . . 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 1147 . . . . . . . . 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 5710 . . . . . . . 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 5716 . . . . . . . . . 10  |-  ( 1st `  t )  e.  _V
51 fvex 5716 . . . . . . . . . 10  |-  ( 1st `  f )  e.  _V
5250, 51coex 6544 . . . . . . . . 9  |-  ( ( 1st `  t )  o.  ( 1st `  f
) )  e.  _V
53 ovex 6131 . . . . . . . . 9  |-  ( ( 2nd `  t ) 
.+^  ( 2nd `  f
) )  e.  _V
5452, 53op1st 6600 . . . . . . . 8  |-  ( 1st `  <. ( ( 1st `  t )  o.  ( 1st `  f ) ) ,  ( ( 2nd `  t )  .+^  ( 2nd `  f ) ) >.
)  =  ( ( 1st `  t )  o.  ( 1st `  f
) )
5549, 54syl6eq 2491 . . . . . . 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 5710 . . . . . 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 34765 . . . . . . . . . 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 1149 . . . . . . . . 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 5710 . . . . . . . 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 5716 . . . . . . . . 9  |-  ( s `
 ( 1st `  t
) )  e.  _V
61 vex 2990 . . . . . . . . . 10  |-  s  e. 
_V
62 fvex 5716 . . . . . . . . . 10  |-  ( 2nd `  t )  e.  _V
6361, 62coex 6544 . . . . . . . . 9  |-  ( s  o.  ( 2nd `  t
) )  e.  _V
6460, 63op1st 6600 . . . . . . . 8  |-  ( 1st `  <. ( s `  ( 1st `  t ) ) ,  ( s  o.  ( 2nd `  t
) ) >. )  =  ( s `  ( 1st `  t ) )
6559, 64syl6eq 2491 . . . . . . 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 34765 . . . . . . . . . 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 1148 . . . . . . . . 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 5710 . . . . . . . 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 5716 . . . . . . . . 9  |-  ( s `
 ( 1st `  f
) )  e.  _V
70 fvex 5716 . . . . . . . . . 10  |-  ( 2nd `  f )  e.  _V
7161, 70coex 6544 . . . . . . . . 9  |-  ( s  o.  ( 2nd `  f
) )  e.  _V
7269, 71op1st 6600 . . . . . . . 8  |-  ( 1st `  <. ( s `  ( 1st `  f ) ) ,  ( s  o.  ( 2nd `  f
) ) >. )  =  ( s `  ( 1st `  f ) )
7368, 72syl6eq 2491 . . . . . . 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 5019 . . . . . 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 2485 . . . . 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 465 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  ( T  X.  E
)  /\  f  e.  ( T  X.  E
) ) )  ->  D  e.  Ring )
7716adantr 465 . . . . . . . . 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 2519 . . . . . . . 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 6622 . . . . . . . . . 10  |-  ( t  e.  ( T  X.  E )  ->  ( 2nd `  t )  e.  E )
8039, 79syl 16 . . . . . . . . 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 2519 . . . . . . . 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 6622 . . . . . . . . . 10  |-  ( f  e.  ( T  X.  E )  ->  ( 2nd `  f )  e.  E )
8342, 82syl 16 . . . . . . . . 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 2519 . . . . . . . 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, 19rngdi 16678 . . . . . . . 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 1220 . . . . . . 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, 17rngacl 16687 . . . . . . . . . 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 1218 . . . . . . . . 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 2520 . . . . . . . 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 34750 . . . . . . . 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 1216 . . . . . . 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 34750 . . . . . . . . 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 1216 . . . . . . . 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 34750 . . . . . . . . 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 1216 . . . . . . . 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 6124 . . . . . . 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 2483 . . . . . 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 5710 . . . . . . . 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 6601 . . . . . . . 8  |-  ( 2nd `  <. ( ( 1st `  t )  o.  ( 1st `  f ) ) ,  ( ( 2nd `  t )  .+^  ( 2nd `  f ) ) >.
)  =  ( ( 2nd `  t ) 
.+^  ( 2nd `  f
) )
10098, 99syl6eq 2491 . . . . . . 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 5017 . . . . . 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 5710 . . . . . . . 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 6601 . . . . . . . 8  |-  ( 2nd `  <. ( s `  ( 1st `  t ) ) ,  ( s  o.  ( 2nd `  t
) ) >. )  =  ( s  o.  ( 2nd `  t
) )
104102, 103syl6eq 2491 . . . . . . 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 5710 . . . . . . . 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 6601 . . . . . . . 8  |-  ( 2nd `  <. ( s `  ( 1st `  f ) ) ,  ( s  o.  ( 2nd `  f
) ) >. )  =  ( s  o.  ( 2nd `  f
) )
107105, 106syl6eq 2491 . . . . . . 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 6124 . . . . . 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 2485 . . . . 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 4082 . . . 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 34759 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( t  e.  ( T  X.  E
)  /\  f  e.  ( T  X.  E
) ) )  -> 
( t  .+  f
)  e.  ( T  X.  E ) )
1121113adantr1 1147 . . . . 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 34765 . . . . 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 1216 . . . 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 1149 . . . . 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 34767 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( s  .x.  f
)  e.  ( T  X.  E ) )
1171163adantr2 1148 . . . . 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 34756 . . . . 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 1216 . . . 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 2485 . . 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 457 . . . . . . 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 994 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
s  e.  E )
123 simpr2 995 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
t  e.  E )
124 simpr3 996 . . . . . . . 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 16 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( 1st `  f
)  e.  T )
126 eqid 2443 . . . . . . . 8  |-  ( +g  `  ( ( EDRing `  K
) `  W )
)  =  ( +g  `  ( ( EDRing `  K
) `  W )
)
1271, 2, 3, 21, 126erngplus2 34467 . . . . . . 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 1220 . . . . . 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 5710 . . . . . . . . . 10  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  ( +g  `  D
)  =  ( +g  `  ( ( EDRing `  K
) `  W )
) )
13017, 129syl5eq 2487 . . . . . . . . 9  |-  ( ( K  e.  HL  /\  W  e.  H )  -> 
.+^  =  ( +g  `  ( ( EDRing `  K
) `  W )
) )
131130oveqd 6123 . . . . . . . 8  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  ( s  .+^  t )  =  ( s ( +g  `  ( (
EDRing `  K ) `  W ) ) t ) )
132131fveq1d 5708 . . . . . . 7  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  ( ( s  .+^  t ) `  ( 1st `  f ) )  =  ( ( s ( +g  `  (
( EDRing `  K ) `  W ) ) t ) `  ( 1st `  f ) ) )
133132adantr 465 . . . . . 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 1148 . . . . . . . . 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 5710 . . . . . . . 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 2491 . . . . . . 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 34765 . . . . . . . . . 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 1147 . . . . . . . . 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 5710 . . . . . . . 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 5716 . . . . . . . . 9  |-  ( t `
 ( 1st `  f
) )  e.  _V
141 vex 2990 . . . . . . . . . 10  |-  t  e. 
_V
142141, 70coex 6544 . . . . . . . . 9  |-  ( t  o.  ( 2nd `  f
) )  e.  _V
143140, 142op1st 6600 . . . . . . . 8  |-  ( 1st `  <. ( t `  ( 1st `  f ) ) ,  ( t  o.  ( 2nd `  f
) ) >. )  =  ( t `  ( 1st `  f ) )
144139, 143syl6eq 2491 . . . . . . 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 5019 . . . . . 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 2485 . . . . 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 465 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  ->  D  e.  Ring )
14816adantr 465 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  ->  E  =  ( Base `  D ) )
149122, 148eleqtrd 2519 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
s  e.  ( Base `  D ) )
150123, 148eleqtrd 2519 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
t  e.  ( Base `  D ) )
151124, 82syl 16 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( 2nd `  f
)  e.  E )
152151, 148eleqtrd 2519 . . . . . . . 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, 19rngdir 16679 . . . . . . . 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 1220 . . . . . . 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, 17rngacl 16687 . . . . . . . . . 10  |-  ( ( D  e.  Ring  /\  s  e.  ( Base `  D
)  /\  t  e.  ( Base `  D )
)  ->  ( s  .+^  t )  e.  (
Base `  D )
)
156147, 149, 150, 155syl3anc 1218 . . . . . . . . 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 2520 . . . . . . . 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 34750 . . . . . . . 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 1216 . . . . . . 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 1216 . . . . . . . 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 34750 . . . . . . . . 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 1216 . . . . . . . 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 6124 . . . . . . 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 2483 . . . . . 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 5710 . . . . . . . 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 2491 . . . . . . 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 5710 . . . . . . . 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 6601 . . . . . . . 8  |-  ( 2nd `  <. ( t `  ( 1st `  f ) ) ,  ( t  o.  ( 2nd `  f
) ) >. )  =  ( t  o.  ( 2nd `  f
) )
169167, 168syl6eq 2491 . . . . . . 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 6124 . . . . . 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 2478 . . . . 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 4082 . . . 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 34765 . . . . 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 1216 . . . 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 1148 . . . . 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 34767 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( t  e.  E  /\  f  e.  ( T  X.  E
) ) )  -> 
( t  .x.  f
)  e.  ( T  X.  E ) )
1771763adantr1 1147 . . . . 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 34756 . . . . 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 1216 . . . 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 2485 . . 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 34429 . . . . . . 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 1223 . . . . . 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 5371 . . . . . . 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 4082 . . . . 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 34435 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  s  e.  E  /\  t  e.  E
)  ->  ( s  o.  t )  e.  E
)
187121, 122, 123, 186syl3anc 1218 . . . . . 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 34765 . . . . . 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 1216 . . . . 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 34430 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  t  e.  E  /\  ( 1st `  f
)  e.  T )  ->  ( t `  ( 1st `  f ) )  e.  T )
191121, 123, 125, 190syl3anc 1218 . . . . . 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 34435 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  t  e.  E  /\  ( 2nd `  f
)  e.  E )  ->  ( t  o.  ( 2nd `  f
) )  e.  E
)
193121, 123, 151, 192syl3anc 1218 . . . . . 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 34766 . . . . . 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 1220 . . . . 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 2485 . . . 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 34750 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  E  /\  t  e.  E ) )  -> 
( s  .X.  t
)  =  ( s  o.  t ) )
1981973adantr3 1149 . . . . 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 6121 . . . 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 6122 . . . 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 2485 . . 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 6621 . . . . . . 7  |-  ( s  e.  ( T  X.  E )  ->  ( 1st `  s )  e.  T )
203202adantl 466 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  s  e.  ( T  X.  E ) )  ->  ( 1st `  s )  e.  T
)
204 tendospid 34681 . . . . . 6  |-  ( ( 1st `  s )  e.  T  ->  (
(  _I  |`  T ) `
 ( 1st `  s
) )  =  ( 1st `  s ) )
205203, 204syl 16 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  s  e.  ( T  X.  E ) )  ->  ( (  _I  |`  T ) `  ( 1st `  s ) )  =  ( 1st `  s ) )
206 xp2nd 6622 . . . . . . 7  |-  ( s  e.  ( T  X.  E )  ->  ( 2nd `  s )  e.  E )
2071, 2, 3tendof 34426 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( 2nd `  s
)  e.  E )  ->  ( 2nd `  s
) : T --> T )
208206, 207sylan2 474 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  s  e.  ( T  X.  E ) )  ->  ( 2nd `  s ) : T --> T )
209 fcoi2 5601 . . . . . 6  |-  ( ( 2nd `  s ) : T --> T  -> 
( (  _I  |`  T )  o.  ( 2nd `  s
) )  =  ( 2nd `  s ) )
210208, 209syl 16 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  s  e.  ( T  X.  E ) )  ->  ( (  _I  |`  T )  o.  ( 2nd `  s
) )  =  ( 2nd `  s ) )
211205, 210opeq12d 4082 . . . 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 34432 . . . . . 6  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  (  _I  |`  T )  e.  E )
213212anim1i 568 . . . . 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 34765 . . . . 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 470 . . . 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 6628 . . . . 5  |-  ( s  e.  ( T  X.  E )  ->  s  =  <. ( 1st `  s
) ,  ( 2nd `  s ) >. )
217216adantl 466 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  s  e.  ( T  X.  E ) )  ->  s  =  <. ( 1st `  s
) ,  ( 2nd `  s ) >. )
218211, 215, 2173eqtr4d 2485 . . 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 16969 . 2  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  U  e.  LMod )
22010islvec 17200 . 2  |-  ( U  e.  LVec  <->  ( U  e. 
LMod  /\  D  e.  DivRing ) )
221219, 28, 220sylanbrc 664 1  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  U  e.  LVec )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965    = wceq 1369    e. wcel 1756   <.cop 3898    _I cid 4646    X. cxp 4853    |` cres 4857    o. ccom 4859   -->wf 5429   ` cfv 5433  (class class class)co 6106   1stc1st 6590   2ndc2nd 6591   Basecbs 14189   +g cplusg 14253   .rcmulr 14254  Scalarcsca 14256   .scvsca 14257   0gc0g 14393   invgcminusg 15426   1rcur 16618   Ringcrg 16660   DivRingcdr 16847   LModclmod 16963   LVecclvec 17198   HLchlt 33014   LHypclh 33647   LTrncltrn 33764   TEndoctendo 34415   EDRingcedring 34416   DVecHcdvh 34742
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4418  ax-sep 4428  ax-nul 4436  ax-pow 4485  ax-pr 4546  ax-un 6387  ax-cnex 9353  ax-resscn 9354  ax-1cn 9355  ax-icn 9356  ax-addcl 9357  ax-addrcl 9358  ax-mulcl 9359  ax-mulrcl 9360  ax-mulcom 9361  ax-addass 9362  ax-mulass 9363  ax-distr 9364  ax-i2m1 9365  ax-1ne0 9366  ax-1rid 9367  ax-rnegex 9368  ax-rrecex 9369  ax-cnre 9370  ax-pre-lttri 9371  ax-pre-lttrn 9372  ax-pre-ltadd 9373  ax-pre-mulgt0 9374  ax-riotaBAD 32623
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-fal 1375  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-nel 2623  df-ral 2735  df-rex 2736  df-reu 2737  df-rmo 2738  df-rab 2739  df-v 2989  df-sbc 3202  df-csb 3304  df-dif 3346  df-un 3348  df-in 3350  df-ss 3357  df-pss 3359  df-nul 3653  df-if 3807  df-pw 3877  df-sn 3893  df-pr 3895  df-tp 3897  df-op 3899  df-uni 4107  df-int 4144  df-iun 4188  df-iin 4189  df-br 4308  df-opab 4366  df-mpt 4367  df-tr 4401  df-eprel 4647  df-id 4651  df-po 4656  df-so 4657  df-fr 4694  df-we 4696  df-ord 4737  df-on 4738  df-lim 4739  df-suc 4740  df-xp 4861  df-rel 4862  df-cnv 4863  df-co 4864  df-dm 4865  df-rn 4866  df-res 4867  df-ima 4868  df-iota 5396  df-fun 5435  df-fn 5436  df-f 5437  df-f1 5438  df-fo 5439  df-f1o 5440  df-fv 5441  df-riota 6067  df-ov 6109  df-oprab 6110  df-mpt2 6111  df-om 6492  df-1st 6592  df-2nd 6593  df-tpos 6760  df-undef 6807  df-recs 6847  df-rdg 6881  df-1o 6935  df-oadd 6939  df-er 7116  df-map 7231  df-en 7326  df-dom 7327  df-sdom 7328  df-fin 7329  df-pnf 9435  df-mnf 9436  df-xr 9437  df-ltxr 9438  df-le 9439  df-sub 9612  df-neg 9613  df-nn 10338  df-2 10395  df-3 10396  df-4 10397  df-5 10398  df-6 10399  df-n0 10595  df-z 10662  df-uz 10877  df-fz 11453  df-struct 14191  df-ndx 14192  df-slot 14193  df-base 14194  df-sets 14195  df-ress 14196  df-plusg 14266  df-mulr 14267  df-sca 14269  df-vsca 14270  df-0g 14395  df-poset 15131  df-plt 15143  df-lub 15159  df-glb 15160  df-join 15161  df-meet 15162  df-p0 15224  df-p1 15225  df-lat 15231  df-clat 15293  df-mnd 15430  df-grp 15560  df-minusg 15561  df-mgp 16607  df-ur 16619  df-rng 16662  df-oppr 16730  df-dvdsr 16748  df-unit 16749  df-invr 16779  df-dvr 16790  df-drng 16849  df-lmod 16965  df-lvec 17199  df-oposet 32840  df-ol 32842  df-oml 32843  df-covers 32930  df-ats 32931  df-atl 32962  df-cvlat 32986  df-hlat 33015  df-llines 33161  df-lplanes 33162  df-lvols 33163  df-lines 33164  df-psubsp 33166  df-pmap 33167  df-padd 33459  df-lhyp 33651  df-laut 33652  df-ldil 33767  df-ltrn 33768  df-trl 33822  df-tendo 34418  df-edring 34420  df-dvech 34743
This theorem is referenced by:  dvhlvec  34773
  Copyright terms: Public domain W3C validator