This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dva1dim

Description: Two expressions for the 1-dimensional subspaces of partial vector space A. Remark in Crawley p. 120 line 21, but using a non-identity translation (nonzero vector) F whose trace is P rather than P itself; F exists by cdlemf . E is the division ring base by erngdv , and sF is the scalar product by dvavsca . F must be a non-identity translation for the expression to be a 1-dimensional subspace, although the theorem doesn't require it. (Contributed by NM, 14-Oct-2013)

Ref Expression
Hypotheses dva1dim.l 
|- .<_ = ( le ` K )
dva1dim.h 
|- H = ( LHyp ` K )
dva1dim.t 
|- T = ( ( LTrn ` K ) ` W )
dva1dim.r 
|- R = ( ( trL ` K ) ` W )
dva1dim.e 
|- E = ( ( TEndo ` K ) ` W )
Assertion dva1dim 
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> { g | E. s e. E g = ( s ` F ) } = { g e. T | ( R ` g ) .<_ ( R ` F ) } )

Proof

Step Hyp Ref Expression
1 dva1dim.l 
 |-  .<_ = ( le ` K )
2 dva1dim.h 
 |-  H = ( LHyp ` K )
3 dva1dim.t 
 |-  T = ( ( LTrn ` K ) ` W )
4 dva1dim.r 
 |-  R = ( ( trL ` K ) ` W )
5 dva1dim.e 
 |-  E = ( ( TEndo ` K ) ` W )
6 2 3 5 tendocl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ s e. E /\ F e. T ) -> ( s ` F ) e. T )
7 1 2 3 4 5 tendotp 
 |-  ( ( ( K e. HL /\ W e. H ) /\ s e. E /\ F e. T ) -> ( R ` ( s ` F ) ) .<_ ( R ` F ) )
8 6 7 jca 
 |-  ( ( ( K e. HL /\ W e. H ) /\ s e. E /\ F e. T ) -> ( ( s ` F ) e. T /\ ( R ` ( s ` F ) ) .<_ ( R ` F ) ) )
9 8 3expb 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ F e. T ) ) -> ( ( s ` F ) e. T /\ ( R ` ( s ` F ) ) .<_ ( R ` F ) ) )
10 9 anass1rs 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ s e. E ) -> ( ( s ` F ) e. T /\ ( R ` ( s ` F ) ) .<_ ( R ` F ) ) )
11 eleq1 
 |-  ( g = ( s ` F ) -> ( g e. T <-> ( s ` F ) e. T ) )
12 fveq2 
 |-  ( g = ( s ` F ) -> ( R ` g ) = ( R ` ( s ` F ) ) )
13 12 breq1d 
 |-  ( g = ( s ` F ) -> ( ( R ` g ) .<_ ( R ` F ) <-> ( R ` ( s ` F ) ) .<_ ( R ` F ) ) )
14 11 13 anbi12d 
 |-  ( g = ( s ` F ) -> ( ( g e. T /\ ( R ` g ) .<_ ( R ` F ) ) <-> ( ( s ` F ) e. T /\ ( R ` ( s ` F ) ) .<_ ( R ` F ) ) ) )
15 10 14 syl5ibrcom 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ s e. E ) -> ( g = ( s ` F ) -> ( g e. T /\ ( R ` g ) .<_ ( R ` F ) ) ) )
16 15 rexlimdva 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( E. s e. E g = ( s ` F ) -> ( g e. T /\ ( R ` g ) .<_ ( R ` F ) ) ) )
17 simpll 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ ( g e. T /\ ( R ` g ) .<_ ( R ` F ) ) ) -> ( K e. HL /\ W e. H ) )
18 simplr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ ( g e. T /\ ( R ` g ) .<_ ( R ` F ) ) ) -> F e. T )
19 simprl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ ( g e. T /\ ( R ` g ) .<_ ( R ` F ) ) ) -> g e. T )
20 simprr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ ( g e. T /\ ( R ` g ) .<_ ( R ` F ) ) ) -> ( R ` g ) .<_ ( R ` F ) )
21 1 2 3 4 5 tendoex 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ g e. T ) /\ ( R ` g ) .<_ ( R ` F ) ) -> E. s e. E ( s ` F ) = g )
22 17 18 19 20 21 syl121anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ ( g e. T /\ ( R ` g ) .<_ ( R ` F ) ) ) -> E. s e. E ( s ` F ) = g )
23 eqcom 
 |-  ( ( s ` F ) = g <-> g = ( s ` F ) )
24 23 rexbii 
 |-  ( E. s e. E ( s ` F ) = g <-> E. s e. E g = ( s ` F ) )
25 22 24 sylib 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ ( g e. T /\ ( R ` g ) .<_ ( R ` F ) ) ) -> E. s e. E g = ( s ` F ) )
26 25 ex 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( ( g e. T /\ ( R ` g ) .<_ ( R ` F ) ) -> E. s e. E g = ( s ` F ) ) )
27 16 26 impbid 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( E. s e. E g = ( s ` F ) <-> ( g e. T /\ ( R ` g ) .<_ ( R ` F ) ) ) )
28 27 abbidv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> { g | E. s e. E g = ( s ` F ) } = { g | ( g e. T /\ ( R ` g ) .<_ ( R ` F ) ) } )
29 df-rab 
 |-  { g e. T | ( R ` g ) .<_ ( R ` F ) } = { g | ( g e. T /\ ( R ` g ) .<_ ( R ` F ) ) }
30 28 29 eqtr4di 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> { g | E. s e. E g = ( s ` F ) } = { g e. T | ( R ` g ) .<_ ( R ` F ) } )