Metamath Proof Explorer

Theorem dib1dim

Description: Two expressions for the 1-dimensional subspaces of vector space H. (Contributed by NM, 24-Feb-2014) (Revised by Mario Carneiro, 24-Jun-2014)

Ref Expression
Hypotheses dib1dim.b 
|- B = ( Base ` K )
dib1dim.h 
|- H = ( LHyp ` K )
dib1dim.t 
|- T = ( ( LTrn ` K ) ` W )
dib1dim.r 
|- R = ( ( trL ` K ) ` W )
dib1dim.e 
|- E = ( ( TEndo ` K ) ` W )
dib1dim.o 
|- O = ( h e. T |-> ( _I |` B ) )
dib1dim.i 
|- I = ( ( DIsoB ` K ) ` W )
Assertion dib1dim 
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( I ` ( R ` F ) ) = { g e. ( T X. E ) | E. s e. E g = <. ( s ` F ) , O >. } )

Proof

Step Hyp Ref Expression
1 dib1dim.b 
 |-  B = ( Base ` K )
2 dib1dim.h 
 |-  H = ( LHyp ` K )
3 dib1dim.t 
 |-  T = ( ( LTrn ` K ) ` W )
4 dib1dim.r 
 |-  R = ( ( trL ` K ) ` W )
5 dib1dim.e 
 |-  E = ( ( TEndo ` K ) ` W )
6 dib1dim.o 
 |-  O = ( h e. T |-> ( _I |` B ) )
7 dib1dim.i 
 |-  I = ( ( DIsoB ` K ) ` W )
8 simpl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( K e. HL /\ W e. H ) )
9 1 2 3 4 trlcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( R ` F ) e. B )
10 eqid 
 |-  ( le ` K ) = ( le ` K )
11 10 2 3 4 trlle 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( R ` F ) ( le ` K ) W )
12 eqid 
 |-  ( ( DIsoA ` K ) ` W ) = ( ( DIsoA ` K ) ` W )
13 1 10 2 3 6 12 7 dibval2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( R ` F ) e. B /\ ( R ` F ) ( le ` K ) W ) ) -> ( I ` ( R ` F ) ) = ( ( ( ( DIsoA ` K ) ` W ) ` ( R ` F ) ) X. { O } ) )
14 8 9 11 13 syl12anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( I ` ( R ` F ) ) = ( ( ( ( DIsoA ` K ) ` W ) ` ( R ` F ) ) X. { O } ) )
15 relxp 
 |-  Rel ( ( ( ( DIsoA ` K ) ` W ) ` ( R ` F ) ) X. { O } )
16 opelxp 
 |-  ( <. f , t >. e. ( ( ( ( DIsoA ` K ) ` W ) ` ( R ` F ) ) X. { O } ) <-> ( f e. ( ( ( DIsoA ` K ) ` W ) ` ( R ` F ) ) /\ t e. { O } ) )
17 2 3 4 5 12 dia1dim 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( ( ( DIsoA ` K ) ` W ) ` ( R ` F ) ) = { f | E. s e. E f = ( s ` F ) } )
18 17 abeq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( f e. ( ( ( DIsoA ` K ) ` W ) ` ( R ` F ) ) <-> E. s e. E f = ( s ` F ) ) )
19 18 anbi1d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( ( f e. ( ( ( DIsoA ` K ) ` W ) ` ( R ` F ) ) /\ t e. { O } ) <-> ( E. s e. E f = ( s ` F ) /\ t e. { O } ) ) )
20 2 3 5 tendocl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ s e. E /\ F e. T ) -> ( s ` F ) e. T )
21 20 3expa 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ s e. E ) /\ F e. T ) -> ( s ` F ) e. T )
22 21 an32s 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ s e. E ) -> ( s ` F ) e. T )
23 1 2 3 5 6 tendo0cl 
 |-  ( ( K e. HL /\ W e. H ) -> O e. E )
24 23 ad2antrr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ s e. E ) -> O e. E )
25 22 24 jca 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ s e. E ) -> ( ( s ` F ) e. T /\ O e. E ) )
26 eleq1 
 |-  ( f = ( s ` F ) -> ( f e. T <-> ( s ` F ) e. T ) )
27 eleq1 
 |-  ( t = O -> ( t e. E <-> O e. E ) )
28 26 27 bi2anan9 
 |-  ( ( f = ( s ` F ) /\ t = O ) -> ( ( f e. T /\ t e. E ) <-> ( ( s ` F ) e. T /\ O e. E ) ) )
29 25 28 syl5ibrcom 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ s e. E ) -> ( ( f = ( s ` F ) /\ t = O ) -> ( f e. T /\ t e. E ) ) )
30 29 rexlimdva 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( E. s e. E ( f = ( s ` F ) /\ t = O ) -> ( f e. T /\ t e. E ) ) )
31 30 pm4.71rd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( E. s e. E ( f = ( s ` F ) /\ t = O ) <-> ( ( f e. T /\ t e. E ) /\ E. s e. E ( f = ( s ` F ) /\ t = O ) ) ) )
32 velsn 
 |-  ( t e. { O } <-> t = O )
33 32 anbi2i 
 |-  ( ( E. s e. E f = ( s ` F ) /\ t e. { O } ) <-> ( E. s e. E f = ( s ` F ) /\ t = O ) )
34 r19.41v 
 |-  ( E. s e. E ( f = ( s ` F ) /\ t = O ) <-> ( E. s e. E f = ( s ` F ) /\ t = O ) )
35 33 34 bitr4i 
 |-  ( ( E. s e. E f = ( s ` F ) /\ t e. { O } ) <-> E. s e. E ( f = ( s ` F ) /\ t = O ) )
36 df-3an 
 |-  ( ( f e. T /\ t e. E /\ E. s e. E ( f = ( s ` F ) /\ t = O ) ) <-> ( ( f e. T /\ t e. E ) /\ E. s e. E ( f = ( s ` F ) /\ t = O ) ) )
37 31 35 36 3bitr4g 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( ( E. s e. E f = ( s ` F ) /\ t e. { O } ) <-> ( f e. T /\ t e. E /\ E. s e. E ( f = ( s ` F ) /\ t = O ) ) ) )
38 19 37 bitrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( ( f e. ( ( ( DIsoA ` K ) ` W ) ` ( R ` F ) ) /\ t e. { O } ) <-> ( f e. T /\ t e. E /\ E. s e. E ( f = ( s ` F ) /\ t = O ) ) ) )
39 16 38 syl5bb 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( <. f , t >. e. ( ( ( ( DIsoA ` K ) ` W ) ` ( R ` F ) ) X. { O } ) <-> ( f e. T /\ t e. E /\ E. s e. E ( f = ( s ` F ) /\ t = O ) ) ) )
40 15 39 opabbi2dv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( ( ( ( DIsoA ` K ) ` W ) ` ( R ` F ) ) X. { O } ) = { <. f , t >. | ( f e. T /\ t e. E /\ E. s e. E ( f = ( s ` F ) /\ t = O ) ) } )
41 14 40 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( I ` ( R ` F ) ) = { <. f , t >. | ( f e. T /\ t e. E /\ E. s e. E ( f = ( s ` F ) /\ t = O ) ) } )
42 eqeq1 
 |-  ( g = <. f , t >. -> ( g = <. ( s ` F ) , O >. <-> <. f , t >. = <. ( s ` F ) , O >. ) )
43 vex 
 |-  f e. _V
44 vex 
 |-  t e. _V
45 43 44 opth 
 |-  ( <. f , t >. = <. ( s ` F ) , O >. <-> ( f = ( s ` F ) /\ t = O ) )
46 42 45 bitrdi 
 |-  ( g = <. f , t >. -> ( g = <. ( s ` F ) , O >. <-> ( f = ( s ` F ) /\ t = O ) ) )
47 46 rexbidv 
 |-  ( g = <. f , t >. -> ( E. s e. E g = <. ( s ` F ) , O >. <-> E. s e. E ( f = ( s ` F ) /\ t = O ) ) )
48 47 rabxp 
 |-  { g e. ( T X. E ) | E. s e. E g = <. ( s ` F ) , O >. } = { <. f , t >. | ( f e. T /\ t e. E /\ E. s e. E ( f = ( s ` F ) /\ t = O ) ) }
49 41 48 eqtr4di 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( I ` ( R ` F ) ) = { g e. ( T X. E ) | E. s e. E g = <. ( s ` F ) , O >. } )