This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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