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 >. } )