Metamath Proof Explorer

Theorem diclspsn

Description: The value of isomorphism C is spanned by vector F . Part of proof of Lemma N of Crawley p. 121 line 29. (Contributed by NM, 21-Feb-2014) (Revised by Mario Carneiro, 24-Jun-2014)

Ref Expression
Hypotheses diclspsn.l 
|- .<_ = ( le ` K )
diclspsn.a 
|- A = ( Atoms ` K )
diclspsn.h 
|- H = ( LHyp ` K )
diclspsn.p 
|- P = ( ( oc ` K ) ` W )
diclspsn.t 
|- T = ( ( LTrn ` K ) ` W )
diclspsn.i 
|- I = ( ( DIsoC ` K ) ` W )
diclspsn.u 
|- U = ( ( DVecH ` K ) ` W )
diclspsn.n 
|- N = ( LSpan ` U )
diclspsn.f 
|- F = ( iota_ f e. T ( f ` P ) = Q )
Assertion diclspsn 
|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( I ` Q ) = ( N ` { <. F , ( _I |` T ) >. } ) )

Proof

Step Hyp Ref Expression
1 diclspsn.l 
 |-  .<_ = ( le ` K )
2 diclspsn.a 
 |-  A = ( Atoms ` K )
3 diclspsn.h 
 |-  H = ( LHyp ` K )
4 diclspsn.p 
 |-  P = ( ( oc ` K ) ` W )
5 diclspsn.t 
 |-  T = ( ( LTrn ` K ) ` W )
6 diclspsn.i 
 |-  I = ( ( DIsoC ` K ) ` W )
7 diclspsn.u 
 |-  U = ( ( DVecH ` K ) ` W )
8 diclspsn.n 
 |-  N = ( LSpan ` U )
9 diclspsn.f 
 |-  F = ( iota_ f e. T ( f ` P ) = Q )
10 df-rab 
 |-  { v e. ( T X. ( ( TEndo ` K ) ` W ) ) | E. x e. ( Base ` ( Scalar ` U ) ) v = ( x ( .s ` U ) <. F , ( _I |` T ) >. ) } = { v | ( v e. ( T X. ( ( TEndo ` K ) ` W ) ) /\ E. x e. ( Base ` ( Scalar ` U ) ) v = ( x ( .s ` U ) <. F , ( _I |` T ) >. ) ) }
11 relopabv 
 |-  Rel { <. y , z >. | ( y = ( z ` F ) /\ z e. ( ( TEndo ` K ) ` W ) ) }
12 eqid 
 |-  ( ( TEndo ` K ) ` W ) = ( ( TEndo ` K ) ` W )
13 1 2 3 4 5 12 6 9 dicval2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( I ` Q ) = { <. y , z >. | ( y = ( z ` F ) /\ z e. ( ( TEndo ` K ) ` W ) ) } )
14 13 releqd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( Rel ( I ` Q ) <-> Rel { <. y , z >. | ( y = ( z ` F ) /\ z e. ( ( TEndo ` K ) ` W ) ) } ) )
15 11 14 mpbiri 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> Rel ( I ` Q ) )
16 ssrab2 
 |-  { v e. ( T X. ( ( TEndo ` K ) ` W ) ) | E. x e. ( Base ` ( Scalar ` U ) ) v = ( x ( .s ` U ) <. F , ( _I |` T ) >. ) } C_ ( T X. ( ( TEndo ` K ) ` W ) )
17 relxp 
 |-  Rel ( T X. ( ( TEndo ` K ) ` W ) )
18 relss 
 |-  ( { v e. ( T X. ( ( TEndo ` K ) ` W ) ) | E. x e. ( Base ` ( Scalar ` U ) ) v = ( x ( .s ` U ) <. F , ( _I |` T ) >. ) } C_ ( T X. ( ( TEndo ` K ) ` W ) ) -> ( Rel ( T X. ( ( TEndo ` K ) ` W ) ) -> Rel { v e. ( T X. ( ( TEndo ` K ) ` W ) ) | E. x e. ( Base ` ( Scalar ` U ) ) v = ( x ( .s ` U ) <. F , ( _I |` T ) >. ) } ) )
19 16 17 18 mp2 
 |-  Rel { v e. ( T X. ( ( TEndo ` K ) ` W ) ) | E. x e. ( Base ` ( Scalar ` U ) ) v = ( x ( .s ` U ) <. F , ( _I |` T ) >. ) }
20 19 a1i 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> Rel { v e. ( T X. ( ( TEndo ` K ) ` W ) ) | E. x e. ( Base ` ( Scalar ` U ) ) v = ( x ( .s ` U ) <. F , ( _I |` T ) >. ) } )
21 id 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) )
22 vex 
 |-  g e. _V
23 vex 
 |-  s e. _V
24 1 2 3 4 5 12 6 9 22 23 dicopelval2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( <. g , s >. e. ( I ` Q ) <-> ( g = ( s ` F ) /\ s e. ( ( TEndo ` K ) ` W ) ) ) )
25 simprl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( g = ( s ` F ) /\ s e. ( ( TEndo ` K ) ` W ) ) ) -> g = ( s ` F ) )
26 simpll 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( g = ( s ` F ) /\ s e. ( ( TEndo ` K ) ` W ) ) ) -> ( K e. HL /\ W e. H ) )
27 simprr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( g = ( s ` F ) /\ s e. ( ( TEndo ` K ) ` W ) ) ) -> s e. ( ( TEndo ` K ) ` W ) )
28 simpl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( K e. HL /\ W e. H ) )
29 1 2 3 4 lhpocnel2 
 |-  ( ( K e. HL /\ W e. H ) -> ( P e. A /\ -. P .<_ W ) )
30 29 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( P e. A /\ -. P .<_ W ) )
31 simpr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( Q e. A /\ -. Q .<_ W ) )
32 1 2 3 5 9 ltrniotacl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> F e. T )
33 28 30 31 32 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> F e. T )
34 33 adantr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( g = ( s ` F ) /\ s e. ( ( TEndo ` K ) ` W ) ) ) -> F e. T )
35 3 5 12 tendocl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ s e. ( ( TEndo ` K ) ` W ) /\ F e. T ) -> ( s ` F ) e. T )
36 26 27 34 35 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( g = ( s ` F ) /\ s e. ( ( TEndo ` K ) ` W ) ) ) -> ( s ` F ) e. T )
37 25 36 eqeltrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( g = ( s ` F ) /\ s e. ( ( TEndo ` K ) ` W ) ) ) -> g e. T )
38 37 27 25 3jca 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( g = ( s ` F ) /\ s e. ( ( TEndo ` K ) ` W ) ) ) -> ( g e. T /\ s e. ( ( TEndo ` K ) ` W ) /\ g = ( s ` F ) ) )
39 simpr3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( g e. T /\ s e. ( ( TEndo ` K ) ` W ) /\ g = ( s ` F ) ) ) -> g = ( s ` F ) )
40 simpr2 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( g e. T /\ s e. ( ( TEndo ` K ) ` W ) /\ g = ( s ` F ) ) ) -> s e. ( ( TEndo ` K ) ` W ) )
41 39 40 jca 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( g e. T /\ s e. ( ( TEndo ` K ) ` W ) /\ g = ( s ` F ) ) ) -> ( g = ( s ` F ) /\ s e. ( ( TEndo ` K ) ` W ) ) )
42 38 41 impbida 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( ( g = ( s ` F ) /\ s e. ( ( TEndo ` K ) ` W ) ) <-> ( g e. T /\ s e. ( ( TEndo ` K ) ` W ) /\ g = ( s ` F ) ) ) )
43 eqid 
 |-  ( Scalar ` U ) = ( Scalar ` U )
44 eqid 
 |-  ( Base ` ( Scalar ` U ) ) = ( Base ` ( Scalar ` U ) )
45 3 12 7 43 44 dvhbase 
 |-  ( ( K e. HL /\ W e. H ) -> ( Base ` ( Scalar ` U ) ) = ( ( TEndo ` K ) ` W ) )
46 45 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( Base ` ( Scalar ` U ) ) = ( ( TEndo ` K ) ` W ) )
47 46 rexeqdv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( E. x e. ( Base ` ( Scalar ` U ) ) <. g , s >. = ( x ( .s ` U ) <. F , ( _I |` T ) >. ) <-> E. x e. ( ( TEndo ` K ) ` W ) <. g , s >. = ( x ( .s ` U ) <. F , ( _I |` T ) >. ) ) )
48 simpll 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ x e. ( ( TEndo ` K ) ` W ) ) -> ( K e. HL /\ W e. H ) )
49 simpr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ x e. ( ( TEndo ` K ) ` W ) ) -> x e. ( ( TEndo ` K ) ` W ) )
50 33 adantr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ x e. ( ( TEndo ` K ) ` W ) ) -> F e. T )
51 3 5 12 tendoidcl 
 |-  ( ( K e. HL /\ W e. H ) -> ( _I |` T ) e. ( ( TEndo ` K ) ` W ) )
52 51 ad2antrr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ x e. ( ( TEndo ` K ) ` W ) ) -> ( _I |` T ) e. ( ( TEndo ` K ) ` W ) )
53 eqid 
 |-  ( .s ` U ) = ( .s ` U )
54 3 5 12 7 53 dvhopvsca 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ F e. T /\ ( _I |` T ) e. ( ( TEndo ` K ) ` W ) ) ) -> ( x ( .s ` U ) <. F , ( _I |` T ) >. ) = <. ( x ` F ) , ( x o. ( _I |` T ) ) >. )
55 48 49 50 52 54 syl13anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ x e. ( ( TEndo ` K ) ` W ) ) -> ( x ( .s ` U ) <. F , ( _I |` T ) >. ) = <. ( x ` F ) , ( x o. ( _I |` T ) ) >. )
56 55 eqeq2d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ x e. ( ( TEndo ` K ) ` W ) ) -> ( <. g , s >. = ( x ( .s ` U ) <. F , ( _I |` T ) >. ) <-> <. g , s >. = <. ( x ` F ) , ( x o. ( _I |` T ) ) >. ) )
57 22 23 opth 
 |-  ( <. g , s >. = <. ( x ` F ) , ( x o. ( _I |` T ) ) >. <-> ( g = ( x ` F ) /\ s = ( x o. ( _I |` T ) ) ) )
58 56 57 bitrdi 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ x e. ( ( TEndo ` K ) ` W ) ) -> ( <. g , s >. = ( x ( .s ` U ) <. F , ( _I |` T ) >. ) <-> ( g = ( x ` F ) /\ s = ( x o. ( _I |` T ) ) ) ) )
59 3 5 12 tendo1mulr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ x e. ( ( TEndo ` K ) ` W ) ) -> ( x o. ( _I |` T ) ) = x )
60 59 adantlr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ x e. ( ( TEndo ` K ) ` W ) ) -> ( x o. ( _I |` T ) ) = x )
61 60 eqeq2d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ x e. ( ( TEndo ` K ) ` W ) ) -> ( s = ( x o. ( _I |` T ) ) <-> s = x ) )
62 equcom 
 |-  ( s = x <-> x = s )
63 61 62 bitrdi 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ x e. ( ( TEndo ` K ) ` W ) ) -> ( s = ( x o. ( _I |` T ) ) <-> x = s ) )
64 63 anbi2d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ x e. ( ( TEndo ` K ) ` W ) ) -> ( ( g = ( x ` F ) /\ s = ( x o. ( _I |` T ) ) ) <-> ( g = ( x ` F ) /\ x = s ) ) )
65 58 64 bitrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ x e. ( ( TEndo ` K ) ` W ) ) -> ( <. g , s >. = ( x ( .s ` U ) <. F , ( _I |` T ) >. ) <-> ( g = ( x ` F ) /\ x = s ) ) )
66 ancom 
 |-  ( ( g = ( x ` F ) /\ x = s ) <-> ( x = s /\ g = ( x ` F ) ) )
67 65 66 bitrdi 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ x e. ( ( TEndo ` K ) ` W ) ) -> ( <. g , s >. = ( x ( .s ` U ) <. F , ( _I |` T ) >. ) <-> ( x = s /\ g = ( x ` F ) ) ) )
68 67 rexbidva 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( E. x e. ( ( TEndo ` K ) ` W ) <. g , s >. = ( x ( .s ` U ) <. F , ( _I |` T ) >. ) <-> E. x e. ( ( TEndo ` K ) ` W ) ( x = s /\ g = ( x ` F ) ) ) )
69 47 68 bitrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( E. x e. ( Base ` ( Scalar ` U ) ) <. g , s >. = ( x ( .s ` U ) <. F , ( _I |` T ) >. ) <-> E. x e. ( ( TEndo ` K ) ` W ) ( x = s /\ g = ( x ` F ) ) ) )
70 69 3anbi3d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( ( g e. T /\ s e. ( ( TEndo ` K ) ` W ) /\ E. x e. ( Base ` ( Scalar ` U ) ) <. g , s >. = ( x ( .s ` U ) <. F , ( _I |` T ) >. ) ) <-> ( g e. T /\ s e. ( ( TEndo ` K ) ` W ) /\ E. x e. ( ( TEndo ` K ) ` W ) ( x = s /\ g = ( x ` F ) ) ) ) )
71 fveq1 
 |-  ( x = s -> ( x ` F ) = ( s ` F ) )
72 71 eqeq2d 
 |-  ( x = s -> ( g = ( x ` F ) <-> g = ( s ` F ) ) )
73 72 ceqsrexv 
 |-  ( s e. ( ( TEndo ` K ) ` W ) -> ( E. x e. ( ( TEndo ` K ) ` W ) ( x = s /\ g = ( x ` F ) ) <-> g = ( s ` F ) ) )
74 73 pm5.32i 
 |-  ( ( s e. ( ( TEndo ` K ) ` W ) /\ E. x e. ( ( TEndo ` K ) ` W ) ( x = s /\ g = ( x ` F ) ) ) <-> ( s e. ( ( TEndo ` K ) ` W ) /\ g = ( s ` F ) ) )
75 74 anbi2i 
 |-  ( ( g e. T /\ ( s e. ( ( TEndo ` K ) ` W ) /\ E. x e. ( ( TEndo ` K ) ` W ) ( x = s /\ g = ( x ` F ) ) ) ) <-> ( g e. T /\ ( s e. ( ( TEndo ` K ) ` W ) /\ g = ( s ` F ) ) ) )
76 3anass 
 |-  ( ( g e. T /\ s e. ( ( TEndo ` K ) ` W ) /\ E. x e. ( ( TEndo ` K ) ` W ) ( x = s /\ g = ( x ` F ) ) ) <-> ( g e. T /\ ( s e. ( ( TEndo ` K ) ` W ) /\ E. x e. ( ( TEndo ` K ) ` W ) ( x = s /\ g = ( x ` F ) ) ) ) )
77 3anass 
 |-  ( ( g e. T /\ s e. ( ( TEndo ` K ) ` W ) /\ g = ( s ` F ) ) <-> ( g e. T /\ ( s e. ( ( TEndo ` K ) ` W ) /\ g = ( s ` F ) ) ) )
78 75 76 77 3bitr4i 
 |-  ( ( g e. T /\ s e. ( ( TEndo ` K ) ` W ) /\ E. x e. ( ( TEndo ` K ) ` W ) ( x = s /\ g = ( x ` F ) ) ) <-> ( g e. T /\ s e. ( ( TEndo ` K ) ` W ) /\ g = ( s ` F ) ) )
79 70 78 bitr2di 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( ( g e. T /\ s e. ( ( TEndo ` K ) ` W ) /\ g = ( s ` F ) ) <-> ( g e. T /\ s e. ( ( TEndo ` K ) ` W ) /\ E. x e. ( Base ` ( Scalar ` U ) ) <. g , s >. = ( x ( .s ` U ) <. F , ( _I |` T ) >. ) ) ) )
80 42 79 bitrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( ( g = ( s ` F ) /\ s e. ( ( TEndo ` K ) ` W ) ) <-> ( g e. T /\ s e. ( ( TEndo ` K ) ` W ) /\ E. x e. ( Base ` ( Scalar ` U ) ) <. g , s >. = ( x ( .s ` U ) <. F , ( _I |` T ) >. ) ) ) )
81 eqeq1 
 |-  ( v = <. g , s >. -> ( v = ( x ( .s ` U ) <. F , ( _I |` T ) >. ) <-> <. g , s >. = ( x ( .s ` U ) <. F , ( _I |` T ) >. ) ) )
82 81 rexbidv 
 |-  ( v = <. g , s >. -> ( E. x e. ( Base ` ( Scalar ` U ) ) v = ( x ( .s ` U ) <. F , ( _I |` T ) >. ) <-> E. x e. ( Base ` ( Scalar ` U ) ) <. g , s >. = ( x ( .s ` U ) <. F , ( _I |` T ) >. ) ) )
83 82 rabxp 
 |-  { v e. ( T X. ( ( TEndo ` K ) ` W ) ) | E. x e. ( Base ` ( Scalar ` U ) ) v = ( x ( .s ` U ) <. F , ( _I |` T ) >. ) } = { <. g , s >. | ( g e. T /\ s e. ( ( TEndo ` K ) ` W ) /\ E. x e. ( Base ` ( Scalar ` U ) ) <. g , s >. = ( x ( .s ` U ) <. F , ( _I |` T ) >. ) ) }
84 83 eleq2i 
 |-  ( <. g , s >. e. { v e. ( T X. ( ( TEndo ` K ) ` W ) ) | E. x e. ( Base ` ( Scalar ` U ) ) v = ( x ( .s ` U ) <. F , ( _I |` T ) >. ) } <-> <. g , s >. e. { <. g , s >. | ( g e. T /\ s e. ( ( TEndo ` K ) ` W ) /\ E. x e. ( Base ` ( Scalar ` U ) ) <. g , s >. = ( x ( .s ` U ) <. F , ( _I |` T ) >. ) ) } )
85 opabidw 
 |-  ( <. g , s >. e. { <. g , s >. | ( g e. T /\ s e. ( ( TEndo ` K ) ` W ) /\ E. x e. ( Base ` ( Scalar ` U ) ) <. g , s >. = ( x ( .s ` U ) <. F , ( _I |` T ) >. ) ) } <-> ( g e. T /\ s e. ( ( TEndo ` K ) ` W ) /\ E. x e. ( Base ` ( Scalar ` U ) ) <. g , s >. = ( x ( .s ` U ) <. F , ( _I |` T ) >. ) ) )
86 84 85 bitr2i 
 |-  ( ( g e. T /\ s e. ( ( TEndo ` K ) ` W ) /\ E. x e. ( Base ` ( Scalar ` U ) ) <. g , s >. = ( x ( .s ` U ) <. F , ( _I |` T ) >. ) ) <-> <. g , s >. e. { v e. ( T X. ( ( TEndo ` K ) ` W ) ) | E. x e. ( Base ` ( Scalar ` U ) ) v = ( x ( .s ` U ) <. F , ( _I |` T ) >. ) } )
87 80 86 bitrdi 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( ( g = ( s ` F ) /\ s e. ( ( TEndo ` K ) ` W ) ) <-> <. g , s >. e. { v e. ( T X. ( ( TEndo ` K ) ` W ) ) | E. x e. ( Base ` ( Scalar ` U ) ) v = ( x ( .s ` U ) <. F , ( _I |` T ) >. ) } ) )
88 24 87 bitrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( <. g , s >. e. ( I ` Q ) <-> <. g , s >. e. { v e. ( T X. ( ( TEndo ` K ) ` W ) ) | E. x e. ( Base ` ( Scalar ` U ) ) v = ( x ( .s ` U ) <. F , ( _I |` T ) >. ) } ) )
89 88 eqrelrdv2 
 |-  ( ( ( Rel ( I ` Q ) /\ Rel { v e. ( T X. ( ( TEndo ` K ) ` W ) ) | E. x e. ( Base ` ( Scalar ` U ) ) v = ( x ( .s ` U ) <. F , ( _I |` T ) >. ) } ) /\ ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) ) -> ( I ` Q ) = { v e. ( T X. ( ( TEndo ` K ) ` W ) ) | E. x e. ( Base ` ( Scalar ` U ) ) v = ( x ( .s ` U ) <. F , ( _I |` T ) >. ) } )
90 15 20 21 89 syl21anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( I ` Q ) = { v e. ( T X. ( ( TEndo ` K ) ` W ) ) | E. x e. ( Base ` ( Scalar ` U ) ) v = ( x ( .s ` U ) <. F , ( _I |` T ) >. ) } )
91 simpll 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ x e. ( Base ` ( Scalar ` U ) ) ) -> ( K e. HL /\ W e. H ) )
92 46 eleq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( x e. ( Base ` ( Scalar ` U ) ) <-> x e. ( ( TEndo ` K ) ` W ) ) )
93 92 biimpa 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ x e. ( Base ` ( Scalar ` U ) ) ) -> x e. ( ( TEndo ` K ) ` W ) )
94 51 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( _I |` T ) e. ( ( TEndo ` K ) ` W ) )
95 opelxpi 
 |-  ( ( F e. T /\ ( _I |` T ) e. ( ( TEndo ` K ) ` W ) ) -> <. F , ( _I |` T ) >. e. ( T X. ( ( TEndo ` K ) ` W ) ) )
96 33 94 95 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> <. F , ( _I |` T ) >. e. ( T X. ( ( TEndo ` K ) ` W ) ) )
97 96 adantr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ x e. ( Base ` ( Scalar ` U ) ) ) -> <. F , ( _I |` T ) >. e. ( T X. ( ( TEndo ` K ) ` W ) ) )
98 3 5 12 7 53 dvhvscacl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ <. F , ( _I |` T ) >. e. ( T X. ( ( TEndo ` K ) ` W ) ) ) ) -> ( x ( .s ` U ) <. F , ( _I |` T ) >. ) e. ( T X. ( ( TEndo ` K ) ` W ) ) )
99 91 93 97 98 syl12anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ x e. ( Base ` ( Scalar ` U ) ) ) -> ( x ( .s ` U ) <. F , ( _I |` T ) >. ) e. ( T X. ( ( TEndo ` K ) ` W ) ) )
100 eleq1a 
 |-  ( ( x ( .s ` U ) <. F , ( _I |` T ) >. ) e. ( T X. ( ( TEndo ` K ) ` W ) ) -> ( v = ( x ( .s ` U ) <. F , ( _I |` T ) >. ) -> v e. ( T X. ( ( TEndo ` K ) ` W ) ) ) )
101 99 100 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ x e. ( Base ` ( Scalar ` U ) ) ) -> ( v = ( x ( .s ` U ) <. F , ( _I |` T ) >. ) -> v e. ( T X. ( ( TEndo ` K ) ` W ) ) ) )
102 101 rexlimdva 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( E. x e. ( Base ` ( Scalar ` U ) ) v = ( x ( .s ` U ) <. F , ( _I |` T ) >. ) -> v e. ( T X. ( ( TEndo ` K ) ` W ) ) ) )
103 102 pm4.71rd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( E. x e. ( Base ` ( Scalar ` U ) ) v = ( x ( .s ` U ) <. F , ( _I |` T ) >. ) <-> ( v e. ( T X. ( ( TEndo ` K ) ` W ) ) /\ E. x e. ( Base ` ( Scalar ` U ) ) v = ( x ( .s ` U ) <. F , ( _I |` T ) >. ) ) ) )
104 103 abbidv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> { v | E. x e. ( Base ` ( Scalar ` U ) ) v = ( x ( .s ` U ) <. F , ( _I |` T ) >. ) } = { v | ( v e. ( T X. ( ( TEndo ` K ) ` W ) ) /\ E. x e. ( Base ` ( Scalar ` U ) ) v = ( x ( .s ` U ) <. F , ( _I |` T ) >. ) ) } )
105 10 90 104 3eqtr4a 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( I ` Q ) = { v | E. x e. ( Base ` ( Scalar ` U ) ) v = ( x ( .s ` U ) <. F , ( _I |` T ) >. ) } )
106 3 7 28 dvhlmod 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> U e. LMod )
107 eqid 
 |-  ( Base ` U ) = ( Base ` U )
108 3 5 12 7 107 dvhelvbasei 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ ( _I |` T ) e. ( ( TEndo ` K ) ` W ) ) ) -> <. F , ( _I |` T ) >. e. ( Base ` U ) )
109 28 33 94 108 syl12anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> <. F , ( _I |` T ) >. e. ( Base ` U ) )
110 43 44 107 53 8 lspsn 
 |-  ( ( U e. LMod /\ <. F , ( _I |` T ) >. e. ( Base ` U ) ) -> ( N ` { <. F , ( _I |` T ) >. } ) = { v | E. x e. ( Base ` ( Scalar ` U ) ) v = ( x ( .s ` U ) <. F , ( _I |` T ) >. ) } )
111 106 109 110 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( N ` { <. F , ( _I |` T ) >. } ) = { v | E. x e. ( Base ` ( Scalar ` U ) ) v = ( x ( .s ` U ) <. F , ( _I |` T ) >. ) } )
112 105 111 eqtr4d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( I ` Q ) = ( N ` { <. F , ( _I |` T ) >. } ) )