Metamath Proof Explorer

Theorem dvhb1dimN

Description: Two expressions for the 1-dimensional subspaces of vector space H, in the isomorphism B case where the 2nd vector component is zero. (Contributed by NM, 23-Feb-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dvhb1dim.l 
|- .<_ = ( le ` K )
dvhb1dim.h 
|- H = ( LHyp ` K )
dvhb1dim.t 
|- T = ( ( LTrn ` K ) ` W )
dvhb1dim.r 
|- R = ( ( trL ` K ) ` W )
dvhb1dim.e 
|- E = ( ( TEndo ` K ) ` W )
dvhb1dim.o 
|- .0. = ( h e. T |-> ( _I |` B ) )
Assertion dvhb1dimN 
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> { g e. ( T X. E ) | E. s e. E g = <. ( s ` F ) , .0. >. } = { g e. ( T X. E ) | ( ( R ` ( 1st ` g ) ) .<_ ( R ` F ) /\ ( 2nd ` g ) = .0. ) } )

Proof

Step Hyp Ref Expression
1 dvhb1dim.l 
 |-  .<_ = ( le ` K )
2 dvhb1dim.h 
 |-  H = ( LHyp ` K )
3 dvhb1dim.t 
 |-  T = ( ( LTrn ` K ) ` W )
4 dvhb1dim.r 
 |-  R = ( ( trL ` K ) ` W )
5 dvhb1dim.e 
 |-  E = ( ( TEndo ` K ) ` W )
6 dvhb1dim.o 
 |-  .0. = ( h e. T |-> ( _I |` B ) )
7 eqop 
 |-  ( g e. ( T X. E ) -> ( g = <. ( s ` F ) , .0. >. <-> ( ( 1st ` g ) = ( s ` F ) /\ ( 2nd ` g ) = .0. ) ) )
8 7 adantl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ g e. ( T X. E ) ) -> ( g = <. ( s ` F ) , .0. >. <-> ( ( 1st ` g ) = ( s ` F ) /\ ( 2nd ` g ) = .0. ) ) )
9 8 rexbidv 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ g e. ( T X. E ) ) -> ( E. s e. E g = <. ( s ` F ) , .0. >. <-> E. s e. E ( ( 1st ` g ) = ( s ` F ) /\ ( 2nd ` g ) = .0. ) ) )
10 r19.41v 
 |-  ( E. s e. E ( ( 1st ` g ) = ( s ` F ) /\ ( 2nd ` g ) = .0. ) <-> ( E. s e. E ( 1st ` g ) = ( s ` F ) /\ ( 2nd ` g ) = .0. ) )
11 fvex 
 |-  ( 1st ` g ) e. _V
12 eqeq1 
 |-  ( f = ( 1st ` g ) -> ( f = ( s ` F ) <-> ( 1st ` g ) = ( s ` F ) ) )
13 12 rexbidv 
 |-  ( f = ( 1st ` g ) -> ( E. s e. E f = ( s ` F ) <-> E. s e. E ( 1st ` g ) = ( s ` F ) ) )
14 11 13 elab 
 |-  ( ( 1st ` g ) e. { f | E. s e. E f = ( s ` F ) } <-> E. s e. E ( 1st ` g ) = ( s ` F ) )
15 1 2 3 4 5 dva1dim 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> { f | E. s e. E f = ( s ` F ) } = { f e. T | ( R ` f ) .<_ ( R ` F ) } )
16 15 adantr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ g e. ( T X. E ) ) -> { f | E. s e. E f = ( s ` F ) } = { f e. T | ( R ` f ) .<_ ( R ` F ) } )
17 16 eleq2d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ g e. ( T X. E ) ) -> ( ( 1st ` g ) e. { f | E. s e. E f = ( s ` F ) } <-> ( 1st ` g ) e. { f e. T | ( R ` f ) .<_ ( R ` F ) } ) )
18 14 17 bitr3id 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ g e. ( T X. E ) ) -> ( E. s e. E ( 1st ` g ) = ( s ` F ) <-> ( 1st ` g ) e. { f e. T | ( R ` f ) .<_ ( R ` F ) } ) )
19 xp1st 
 |-  ( g e. ( T X. E ) -> ( 1st ` g ) e. T )
20 19 adantl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ g e. ( T X. E ) ) -> ( 1st ` g ) e. T )
21 fveq2 
 |-  ( f = ( 1st ` g ) -> ( R ` f ) = ( R ` ( 1st ` g ) ) )
22 21 breq1d 
 |-  ( f = ( 1st ` g ) -> ( ( R ` f ) .<_ ( R ` F ) <-> ( R ` ( 1st ` g ) ) .<_ ( R ` F ) ) )
23 22 elrab3 
 |-  ( ( 1st ` g ) e. T -> ( ( 1st ` g ) e. { f e. T | ( R ` f ) .<_ ( R ` F ) } <-> ( R ` ( 1st ` g ) ) .<_ ( R ` F ) ) )
24 20 23 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ g e. ( T X. E ) ) -> ( ( 1st ` g ) e. { f e. T | ( R ` f ) .<_ ( R ` F ) } <-> ( R ` ( 1st ` g ) ) .<_ ( R ` F ) ) )
25 18 24 bitrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ g e. ( T X. E ) ) -> ( E. s e. E ( 1st ` g ) = ( s ` F ) <-> ( R ` ( 1st ` g ) ) .<_ ( R ` F ) ) )
26 25 anbi1d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ g e. ( T X. E ) ) -> ( ( E. s e. E ( 1st ` g ) = ( s ` F ) /\ ( 2nd ` g ) = .0. ) <-> ( ( R ` ( 1st ` g ) ) .<_ ( R ` F ) /\ ( 2nd ` g ) = .0. ) ) )
27 10 26 syl5bb 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ g e. ( T X. E ) ) -> ( E. s e. E ( ( 1st ` g ) = ( s ` F ) /\ ( 2nd ` g ) = .0. ) <-> ( ( R ` ( 1st ` g ) ) .<_ ( R ` F ) /\ ( 2nd ` g ) = .0. ) ) )
28 9 27 bitrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ g e. ( T X. E ) ) -> ( E. s e. E g = <. ( s ` F ) , .0. >. <-> ( ( R ` ( 1st ` g ) ) .<_ ( R ` F ) /\ ( 2nd ` g ) = .0. ) ) )
29 28 rabbidva 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> { g e. ( T X. E ) | E. s e. E g = <. ( s ` F ) , .0. >. } = { g e. ( T X. E ) | ( ( R ` ( 1st ` g ) ) .<_ ( R ` F ) /\ ( 2nd ` g ) = .0. ) } )