Metamath Proof Explorer

Theorem diblss

Description: The value of partial isomorphism B is a subspace of partial vector space H. TODO: use dib* specific theorems instead of dia* ones to shorten proof? (Contributed by NM, 11-Feb-2014)

Ref Expression
Hypotheses diblss.b 
|- B = ( Base ` K )
diblss.l 
|- .<_ = ( le ` K )
diblss.h 
|- H = ( LHyp ` K )
diblss.u 
|- U = ( ( DVecH ` K ) ` W )
diblss.i 
|- I = ( ( DIsoB ` K ) ` W )
diblss.s 
|- S = ( LSubSp ` U )
Assertion diblss 
|- ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( I ` X ) e. S )

Proof

Step Hyp Ref Expression
1 diblss.b 
 |-  B = ( Base ` K )
2 diblss.l 
 |-  .<_ = ( le ` K )
3 diblss.h 
 |-  H = ( LHyp ` K )
4 diblss.u 
 |-  U = ( ( DVecH ` K ) ` W )
5 diblss.i 
 |-  I = ( ( DIsoB ` K ) ` W )
6 diblss.s 
 |-  S = ( LSubSp ` U )
7 eqidd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( Scalar ` U ) = ( Scalar ` U ) )
8 eqid 
 |-  ( ( TEndo ` K ) ` W ) = ( ( TEndo ` K ) ` W )
9 eqid 
 |-  ( Scalar ` U ) = ( Scalar ` U )
10 eqid 
 |-  ( Base ` ( Scalar ` U ) ) = ( Base ` ( Scalar ` U ) )
11 3 8 4 9 10 dvhbase 
 |-  ( ( K e. HL /\ W e. H ) -> ( Base ` ( Scalar ` U ) ) = ( ( TEndo ` K ) ` W ) )
12 11 eqcomd 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( TEndo ` K ) ` W ) = ( Base ` ( Scalar ` U ) ) )
13 12 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( ( TEndo ` K ) ` W ) = ( Base ` ( Scalar ` U ) ) )
14 eqid 
 |-  ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W )
15 eqid 
 |-  ( Base ` U ) = ( Base ` U )
16 3 14 8 4 15 dvhvbase 
 |-  ( ( K e. HL /\ W e. H ) -> ( Base ` U ) = ( ( ( LTrn ` K ) ` W ) X. ( ( TEndo ` K ) ` W ) ) )
17 16 eqcomd 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( ( LTrn ` K ) ` W ) X. ( ( TEndo ` K ) ` W ) ) = ( Base ` U ) )
18 17 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( ( ( LTrn ` K ) ` W ) X. ( ( TEndo ` K ) ` W ) ) = ( Base ` U ) )
19 eqidd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( +g ` U ) = ( +g ` U ) )
20 eqidd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( .s ` U ) = ( .s ` U ) )
21 6 a1i 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> S = ( LSubSp ` U ) )
22 1 2 3 5 4 15 dibss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( I ` X ) C_ ( Base ` U ) )
23 22 18 sseqtrrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( I ` X ) C_ ( ( ( LTrn ` K ) ` W ) X. ( ( TEndo ` K ) ` W ) ) )
24 1 2 3 5 dibn0 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( I ` X ) =/= (/) )
25 fvex 
 |-  ( x ` ( 1st ` a ) ) e. _V
26 vex 
 |-  x e. _V
27 fvex 
 |-  ( 2nd ` a ) e. _V
28 26 27 coex 
 |-  ( x o. ( 2nd ` a ) ) e. _V
29 25 28 op1st 
 |-  ( 1st ` <. ( x ` ( 1st ` a ) ) , ( x o. ( 2nd ` a ) ) >. ) = ( x ` ( 1st ` a ) )
30 29 coeq1i 
 |-  ( ( 1st ` <. ( x ` ( 1st ` a ) ) , ( x o. ( 2nd ` a ) ) >. ) o. ( 1st ` b ) ) = ( ( x ` ( 1st ` a ) ) o. ( 1st ` b ) )
31 simpll 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( K e. HL /\ W e. H ) )
32 simpr1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> x e. ( ( TEndo ` K ) ` W ) )
33 simplr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( X e. B /\ X .<_ W ) )
34 simpr2 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> a e. ( I ` X ) )
35 1 2 3 14 5 dibelval1st1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ a e. ( I ` X ) ) -> ( 1st ` a ) e. ( ( LTrn ` K ) ` W ) )
36 31 33 34 35 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( 1st ` a ) e. ( ( LTrn ` K ) ` W ) )
37 3 14 8 tendocl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ x e. ( ( TEndo ` K ) ` W ) /\ ( 1st ` a ) e. ( ( LTrn ` K ) ` W ) ) -> ( x ` ( 1st ` a ) ) e. ( ( LTrn ` K ) ` W ) )
38 31 32 36 37 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( x ` ( 1st ` a ) ) e. ( ( LTrn ` K ) ` W ) )
39 simpr3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> b e. ( I ` X ) )
40 1 2 3 14 5 dibelval1st1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ b e. ( I ` X ) ) -> ( 1st ` b ) e. ( ( LTrn ` K ) ` W ) )
41 31 33 39 40 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( 1st ` b ) e. ( ( LTrn ` K ) ` W ) )
42 3 14 ltrnco 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( x ` ( 1st ` a ) ) e. ( ( LTrn ` K ) ` W ) /\ ( 1st ` b ) e. ( ( LTrn ` K ) ` W ) ) -> ( ( x ` ( 1st ` a ) ) o. ( 1st ` b ) ) e. ( ( LTrn ` K ) ` W ) )
43 31 38 41 42 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( ( x ` ( 1st ` a ) ) o. ( 1st ` b ) ) e. ( ( LTrn ` K ) ` W ) )
44 simplll 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> K e. HL )
45 44 hllatd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> K e. Lat )
46 eqid 
 |-  ( ( trL ` K ) ` W ) = ( ( trL ` K ) ` W )
47 1 3 14 46 trlcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( x ` ( 1st ` a ) ) o. ( 1st ` b ) ) e. ( ( LTrn ` K ) ` W ) ) -> ( ( ( trL ` K ) ` W ) ` ( ( x ` ( 1st ` a ) ) o. ( 1st ` b ) ) ) e. B )
48 31 43 47 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( ( ( trL ` K ) ` W ) ` ( ( x ` ( 1st ` a ) ) o. ( 1st ` b ) ) ) e. B )
49 1 3 14 46 trlcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( x ` ( 1st ` a ) ) e. ( ( LTrn ` K ) ` W ) ) -> ( ( ( trL ` K ) ` W ) ` ( x ` ( 1st ` a ) ) ) e. B )
50 31 38 49 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( ( ( trL ` K ) ` W ) ` ( x ` ( 1st ` a ) ) ) e. B )
51 1 3 14 46 trlcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( 1st ` b ) e. ( ( LTrn ` K ) ` W ) ) -> ( ( ( trL ` K ) ` W ) ` ( 1st ` b ) ) e. B )
52 31 41 51 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( ( ( trL ` K ) ` W ) ` ( 1st ` b ) ) e. B )
53 eqid 
 |-  ( join ` K ) = ( join ` K )
54 1 53 latjcl 
 |-  ( ( K e. Lat /\ ( ( ( trL ` K ) ` W ) ` ( x ` ( 1st ` a ) ) ) e. B /\ ( ( ( trL ` K ) ` W ) ` ( 1st ` b ) ) e. B ) -> ( ( ( ( trL ` K ) ` W ) ` ( x ` ( 1st ` a ) ) ) ( join ` K ) ( ( ( trL ` K ) ` W ) ` ( 1st ` b ) ) ) e. B )
55 45 50 52 54 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( ( ( ( trL ` K ) ` W ) ` ( x ` ( 1st ` a ) ) ) ( join ` K ) ( ( ( trL ` K ) ` W ) ` ( 1st ` b ) ) ) e. B )
56 simplrl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> X e. B )
57 2 53 3 14 46 trlco 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( x ` ( 1st ` a ) ) e. ( ( LTrn ` K ) ` W ) /\ ( 1st ` b ) e. ( ( LTrn ` K ) ` W ) ) -> ( ( ( trL ` K ) ` W ) ` ( ( x ` ( 1st ` a ) ) o. ( 1st ` b ) ) ) .<_ ( ( ( ( trL ` K ) ` W ) ` ( x ` ( 1st ` a ) ) ) ( join ` K ) ( ( ( trL ` K ) ` W ) ` ( 1st ` b ) ) ) )
58 31 38 41 57 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( ( ( trL ` K ) ` W ) ` ( ( x ` ( 1st ` a ) ) o. ( 1st ` b ) ) ) .<_ ( ( ( ( trL ` K ) ` W ) ` ( x ` ( 1st ` a ) ) ) ( join ` K ) ( ( ( trL ` K ) ` W ) ` ( 1st ` b ) ) ) )
59 1 3 14 46 trlcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( 1st ` a ) e. ( ( LTrn ` K ) ` W ) ) -> ( ( ( trL ` K ) ` W ) ` ( 1st ` a ) ) e. B )
60 31 36 59 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( ( ( trL ` K ) ` W ) ` ( 1st ` a ) ) e. B )
61 2 3 14 46 8 tendotp 
 |-  ( ( ( K e. HL /\ W e. H ) /\ x e. ( ( TEndo ` K ) ` W ) /\ ( 1st ` a ) e. ( ( LTrn ` K ) ` W ) ) -> ( ( ( trL ` K ) ` W ) ` ( x ` ( 1st ` a ) ) ) .<_ ( ( ( trL ` K ) ` W ) ` ( 1st ` a ) ) )
62 31 32 36 61 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( ( ( trL ` K ) ` W ) ` ( x ` ( 1st ` a ) ) ) .<_ ( ( ( trL ` K ) ` W ) ` ( 1st ` a ) ) )
63 eqid 
 |-  ( ( DIsoA ` K ) ` W ) = ( ( DIsoA ` K ) ` W )
64 1 2 3 63 5 dibelval1st 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ a e. ( I ` X ) ) -> ( 1st ` a ) e. ( ( ( DIsoA ` K ) ` W ) ` X ) )
65 31 33 34 64 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( 1st ` a ) e. ( ( ( DIsoA ` K ) ` W ) ` X ) )
66 1 2 3 14 46 63 diatrl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( 1st ` a ) e. ( ( ( DIsoA ` K ) ` W ) ` X ) ) -> ( ( ( trL ` K ) ` W ) ` ( 1st ` a ) ) .<_ X )
67 31 33 65 66 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( ( ( trL ` K ) ` W ) ` ( 1st ` a ) ) .<_ X )
68 1 2 45 50 60 56 62 67 lattrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( ( ( trL ` K ) ` W ) ` ( x ` ( 1st ` a ) ) ) .<_ X )
69 1 2 3 63 5 dibelval1st 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ b e. ( I ` X ) ) -> ( 1st ` b ) e. ( ( ( DIsoA ` K ) ` W ) ` X ) )
70 31 33 39 69 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( 1st ` b ) e. ( ( ( DIsoA ` K ) ` W ) ` X ) )
71 1 2 3 14 46 63 diatrl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( 1st ` b ) e. ( ( ( DIsoA ` K ) ` W ) ` X ) ) -> ( ( ( trL ` K ) ` W ) ` ( 1st ` b ) ) .<_ X )
72 31 33 70 71 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( ( ( trL ` K ) ` W ) ` ( 1st ` b ) ) .<_ X )
73 1 2 53 latjle12 
 |-  ( ( K e. Lat /\ ( ( ( ( trL ` K ) ` W ) ` ( x ` ( 1st ` a ) ) ) e. B /\ ( ( ( trL ` K ) ` W ) ` ( 1st ` b ) ) e. B /\ X e. B ) ) -> ( ( ( ( ( trL ` K ) ` W ) ` ( x ` ( 1st ` a ) ) ) .<_ X /\ ( ( ( trL ` K ) ` W ) ` ( 1st ` b ) ) .<_ X ) <-> ( ( ( ( trL ` K ) ` W ) ` ( x ` ( 1st ` a ) ) ) ( join ` K ) ( ( ( trL ` K ) ` W ) ` ( 1st ` b ) ) ) .<_ X ) )
74 45 50 52 56 73 syl13anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( ( ( ( ( trL ` K ) ` W ) ` ( x ` ( 1st ` a ) ) ) .<_ X /\ ( ( ( trL ` K ) ` W ) ` ( 1st ` b ) ) .<_ X ) <-> ( ( ( ( trL ` K ) ` W ) ` ( x ` ( 1st ` a ) ) ) ( join ` K ) ( ( ( trL ` K ) ` W ) ` ( 1st ` b ) ) ) .<_ X ) )
75 68 72 74 mpbi2and 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( ( ( ( trL ` K ) ` W ) ` ( x ` ( 1st ` a ) ) ) ( join ` K ) ( ( ( trL ` K ) ` W ) ` ( 1st ` b ) ) ) .<_ X )
76 1 2 45 48 55 56 58 75 lattrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( ( ( trL ` K ) ` W ) ` ( ( x ` ( 1st ` a ) ) o. ( 1st ` b ) ) ) .<_ X )
77 1 2 3 14 46 63 diaelval 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( ( ( x ` ( 1st ` a ) ) o. ( 1st ` b ) ) e. ( ( ( DIsoA ` K ) ` W ) ` X ) <-> ( ( ( x ` ( 1st ` a ) ) o. ( 1st ` b ) ) e. ( ( LTrn ` K ) ` W ) /\ ( ( ( trL ` K ) ` W ) ` ( ( x ` ( 1st ` a ) ) o. ( 1st ` b ) ) ) .<_ X ) ) )
78 77 adantr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( ( ( x ` ( 1st ` a ) ) o. ( 1st ` b ) ) e. ( ( ( DIsoA ` K ) ` W ) ` X ) <-> ( ( ( x ` ( 1st ` a ) ) o. ( 1st ` b ) ) e. ( ( LTrn ` K ) ` W ) /\ ( ( ( trL ` K ) ` W ) ` ( ( x ` ( 1st ` a ) ) o. ( 1st ` b ) ) ) .<_ X ) ) )
79 43 76 78 mpbir2and 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( ( x ` ( 1st ` a ) ) o. ( 1st ` b ) ) e. ( ( ( DIsoA ` K ) ` W ) ` X ) )
80 30 79 eqeltrid 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( ( 1st ` <. ( x ` ( 1st ` a ) ) , ( x o. ( 2nd ` a ) ) >. ) o. ( 1st ` b ) ) e. ( ( ( DIsoA ` K ) ` W ) ` X ) )
81 eqid 
 |-  ( s e. ( ( TEndo ` K ) ` W ) , t e. ( ( TEndo ` K ) ` W ) |-> ( h e. ( ( LTrn ` K ) ` W ) |-> ( ( s ` h ) o. ( t ` h ) ) ) ) = ( s e. ( ( TEndo ` K ) ` W ) , t e. ( ( TEndo ` K ) ` W ) |-> ( h e. ( ( LTrn ` K ) ` W ) |-> ( ( s ` h ) o. ( t ` h ) ) ) )
82 eqid 
 |-  ( +g ` ( Scalar ` U ) ) = ( +g ` ( Scalar ` U ) )
83 3 14 8 4 9 81 82 dvhfplusr 
 |-  ( ( K e. HL /\ W e. H ) -> ( +g ` ( Scalar ` U ) ) = ( s e. ( ( TEndo ` K ) ` W ) , t e. ( ( TEndo ` K ) ` W ) |-> ( h e. ( ( LTrn ` K ) ` W ) |-> ( ( s ` h ) o. ( t ` h ) ) ) ) )
84 83 ad2antrr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( +g ` ( Scalar ` U ) ) = ( s e. ( ( TEndo ` K ) ` W ) , t e. ( ( TEndo ` K ) ` W ) |-> ( h e. ( ( LTrn ` K ) ` W ) |-> ( ( s ` h ) o. ( t ` h ) ) ) ) )
85 25 28 op2nd 
 |-  ( 2nd ` <. ( x ` ( 1st ` a ) ) , ( x o. ( 2nd ` a ) ) >. ) = ( x o. ( 2nd ` a ) )
86 eqid 
 |-  ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) = ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) )
87 1 2 3 14 86 5 dibelval2nd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ a e. ( I ` X ) ) -> ( 2nd ` a ) = ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) )
88 31 33 34 87 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( 2nd ` a ) = ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) )
89 88 coeq2d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( x o. ( 2nd ` a ) ) = ( x o. ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) ) )
90 1 3 14 8 86 tendo0mulr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ x e. ( ( TEndo ` K ) ` W ) ) -> ( x o. ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) ) = ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) )
91 31 32 90 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( x o. ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) ) = ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) )
92 89 91 eqtrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( x o. ( 2nd ` a ) ) = ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) )
93 85 92 syl5eq 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( 2nd ` <. ( x ` ( 1st ` a ) ) , ( x o. ( 2nd ` a ) ) >. ) = ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) )
94 1 2 3 14 86 5 dibelval2nd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ b e. ( I ` X ) ) -> ( 2nd ` b ) = ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) )
95 31 33 39 94 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( 2nd ` b ) = ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) )
96 84 93 95 oveq123d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( ( 2nd ` <. ( x ` ( 1st ` a ) ) , ( x o. ( 2nd ` a ) ) >. ) ( +g ` ( Scalar ` U ) ) ( 2nd ` b ) ) = ( ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) ( s e. ( ( TEndo ` K ) ` W ) , t e. ( ( TEndo ` K ) ` W ) |-> ( h e. ( ( LTrn ` K ) ` W ) |-> ( ( s ` h ) o. ( t ` h ) ) ) ) ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) ) )
97 simpllr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> W e. H )
98 1 3 14 8 86 tendo0cl 
 |-  ( ( K e. HL /\ W e. H ) -> ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) e. ( ( TEndo ` K ) ` W ) )
99 98 ad2antrr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) e. ( ( TEndo ` K ) ` W ) )
100 1 3 14 8 86 81 tendo0pl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) e. ( ( TEndo ` K ) ` W ) ) -> ( ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) ( s e. ( ( TEndo ` K ) ` W ) , t e. ( ( TEndo ` K ) ` W ) |-> ( h e. ( ( LTrn ` K ) ` W ) |-> ( ( s ` h ) o. ( t ` h ) ) ) ) ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) ) = ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) )
101 44 97 99 100 syl21anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) ( s e. ( ( TEndo ` K ) ` W ) , t e. ( ( TEndo ` K ) ` W ) |-> ( h e. ( ( LTrn ` K ) ` W ) |-> ( ( s ` h ) o. ( t ` h ) ) ) ) ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) ) = ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) )
102 96 101 eqtrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( ( 2nd ` <. ( x ` ( 1st ` a ) ) , ( x o. ( 2nd ` a ) ) >. ) ( +g ` ( Scalar ` U ) ) ( 2nd ` b ) ) = ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) )
103 ovex 
 |-  ( ( 2nd ` <. ( x ` ( 1st ` a ) ) , ( x o. ( 2nd ` a ) ) >. ) ( +g ` ( Scalar ` U ) ) ( 2nd ` b ) ) e. _V
104 103 elsn 
 |-  ( ( ( 2nd ` <. ( x ` ( 1st ` a ) ) , ( x o. ( 2nd ` a ) ) >. ) ( +g ` ( Scalar ` U ) ) ( 2nd ` b ) ) e. { ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) } <-> ( ( 2nd ` <. ( x ` ( 1st ` a ) ) , ( x o. ( 2nd ` a ) ) >. ) ( +g ` ( Scalar ` U ) ) ( 2nd ` b ) ) = ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) )
105 102 104 sylibr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( ( 2nd ` <. ( x ` ( 1st ` a ) ) , ( x o. ( 2nd ` a ) ) >. ) ( +g ` ( Scalar ` U ) ) ( 2nd ` b ) ) e. { ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) } )
106 opelxpi 
 |-  ( ( ( ( 1st ` <. ( x ` ( 1st ` a ) ) , ( x o. ( 2nd ` a ) ) >. ) o. ( 1st ` b ) ) e. ( ( ( DIsoA ` K ) ` W ) ` X ) /\ ( ( 2nd ` <. ( x ` ( 1st ` a ) ) , ( x o. ( 2nd ` a ) ) >. ) ( +g ` ( Scalar ` U ) ) ( 2nd ` b ) ) e. { ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) } ) -> <. ( ( 1st ` <. ( x ` ( 1st ` a ) ) , ( x o. ( 2nd ` a ) ) >. ) o. ( 1st ` b ) ) , ( ( 2nd ` <. ( x ` ( 1st ` a ) ) , ( x o. ( 2nd ` a ) ) >. ) ( +g ` ( Scalar ` U ) ) ( 2nd ` b ) ) >. e. ( ( ( ( DIsoA ` K ) ` W ) ` X ) X. { ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) } ) )
107 80 105 106 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> <. ( ( 1st ` <. ( x ` ( 1st ` a ) ) , ( x o. ( 2nd ` a ) ) >. ) o. ( 1st ` b ) ) , ( ( 2nd ` <. ( x ` ( 1st ` a ) ) , ( x o. ( 2nd ` a ) ) >. ) ( +g ` ( Scalar ` U ) ) ( 2nd ` b ) ) >. e. ( ( ( ( DIsoA ` K ) ` W ) ` X ) X. { ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) } ) )
108 23 adantr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( I ` X ) C_ ( ( ( LTrn ` K ) ` W ) X. ( ( TEndo ` K ) ` W ) ) )
109 108 34 sseldd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> a e. ( ( ( LTrn ` K ) ` W ) X. ( ( TEndo ` K ) ` W ) ) )
110 eqid 
 |-  ( .s ` U ) = ( .s ` U )
111 3 14 8 4 110 dvhvsca 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( ( ( LTrn ` K ) ` W ) X. ( ( TEndo ` K ) ` W ) ) ) ) -> ( x ( .s ` U ) a ) = <. ( x ` ( 1st ` a ) ) , ( x o. ( 2nd ` a ) ) >. )
112 31 32 109 111 syl12anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( x ( .s ` U ) a ) = <. ( x ` ( 1st ` a ) ) , ( x o. ( 2nd ` a ) ) >. )
113 112 oveq1d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( ( x ( .s ` U ) a ) ( +g ` U ) b ) = ( <. ( x ` ( 1st ` a ) ) , ( x o. ( 2nd ` a ) ) >. ( +g ` U ) b ) )
114 88 99 eqeltrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( 2nd ` a ) e. ( ( TEndo ` K ) ` W ) )
115 3 8 tendococl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ x e. ( ( TEndo ` K ) ` W ) /\ ( 2nd ` a ) e. ( ( TEndo ` K ) ` W ) ) -> ( x o. ( 2nd ` a ) ) e. ( ( TEndo ` K ) ` W ) )
116 31 32 114 115 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( x o. ( 2nd ` a ) ) e. ( ( TEndo ` K ) ` W ) )
117 opelxpi 
 |-  ( ( ( x ` ( 1st ` a ) ) e. ( ( LTrn ` K ) ` W ) /\ ( x o. ( 2nd ` a ) ) e. ( ( TEndo ` K ) ` W ) ) -> <. ( x ` ( 1st ` a ) ) , ( x o. ( 2nd ` a ) ) >. e. ( ( ( LTrn ` K ) ` W ) X. ( ( TEndo ` K ) ` W ) ) )
118 38 116 117 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> <. ( x ` ( 1st ` a ) ) , ( x o. ( 2nd ` a ) ) >. e. ( ( ( LTrn ` K ) ` W ) X. ( ( TEndo ` K ) ` W ) ) )
119 108 39 sseldd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> b e. ( ( ( LTrn ` K ) ` W ) X. ( ( TEndo ` K ) ` W ) ) )
120 eqid 
 |-  ( +g ` U ) = ( +g ` U )
121 3 14 8 4 9 120 82 dvhvadd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( <. ( x ` ( 1st ` a ) ) , ( x o. ( 2nd ` a ) ) >. e. ( ( ( LTrn ` K ) ` W ) X. ( ( TEndo ` K ) ` W ) ) /\ b e. ( ( ( LTrn ` K ) ` W ) X. ( ( TEndo ` K ) ` W ) ) ) ) -> ( <. ( x ` ( 1st ` a ) ) , ( x o. ( 2nd ` a ) ) >. ( +g ` U ) b ) = <. ( ( 1st ` <. ( x ` ( 1st ` a ) ) , ( x o. ( 2nd ` a ) ) >. ) o. ( 1st ` b ) ) , ( ( 2nd ` <. ( x ` ( 1st ` a ) ) , ( x o. ( 2nd ` a ) ) >. ) ( +g ` ( Scalar ` U ) ) ( 2nd ` b ) ) >. )
122 31 118 119 121 syl12anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( <. ( x ` ( 1st ` a ) ) , ( x o. ( 2nd ` a ) ) >. ( +g ` U ) b ) = <. ( ( 1st ` <. ( x ` ( 1st ` a ) ) , ( x o. ( 2nd ` a ) ) >. ) o. ( 1st ` b ) ) , ( ( 2nd ` <. ( x ` ( 1st ` a ) ) , ( x o. ( 2nd ` a ) ) >. ) ( +g ` ( Scalar ` U ) ) ( 2nd ` b ) ) >. )
123 113 122 eqtrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( ( x ( .s ` U ) a ) ( +g ` U ) b ) = <. ( ( 1st ` <. ( x ` ( 1st ` a ) ) , ( x o. ( 2nd ` a ) ) >. ) o. ( 1st ` b ) ) , ( ( 2nd ` <. ( x ` ( 1st ` a ) ) , ( x o. ( 2nd ` a ) ) >. ) ( +g ` ( Scalar ` U ) ) ( 2nd ` b ) ) >. )
124 1 2 3 14 86 63 5 dibval2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( I ` X ) = ( ( ( ( DIsoA ` K ) ` W ) ` X ) X. { ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) } ) )
125 124 adantr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( I ` X ) = ( ( ( ( DIsoA ` K ) ` W ) ` X ) X. { ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) } ) )
126 107 123 125 3eltr4d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( ( x ( .s ` U ) a ) ( +g ` U ) b ) e. ( I ` X ) )
127 7 13 18 19 20 21 23 24 126 islssd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( I ` X ) e. S )