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

Metamath Proof Explorer

Theorem dia1dim

Description: Two expressions for the 1-dimensional subspaces of partial vector space A (when F is a nonzero vector i.e. non-identity translation). Remark after Lemma L in Crawley p. 120 line 21. (Contributed by NM, 15-Oct-2013) (Revised by Mario Carneiro, 22-Jun-2014)

Ref Expression
Hypotheses dia1dim.h 
|- H = ( LHyp ` K )
dia1dim.t 
|- T = ( ( LTrn ` K ) ` W )
dia1dim.r 
|- R = ( ( trL ` K ) ` W )
dia1dim.e 
|- E = ( ( TEndo ` K ) ` W )
dia1dim.i 
|- I = ( ( DIsoA ` K ) ` W )
Assertion dia1dim 
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( I ` ( R ` F ) ) = { g | E. s e. E g = ( s ` F ) } )

Proof

Step Hyp Ref Expression
1 dia1dim.h 
 |-  H = ( LHyp ` K )
2 dia1dim.t 
 |-  T = ( ( LTrn ` K ) ` W )
3 dia1dim.r 
 |-  R = ( ( trL ` K ) ` W )
4 dia1dim.e 
 |-  E = ( ( TEndo ` K ) ` W )
5 dia1dim.i 
 |-  I = ( ( DIsoA ` K ) ` W )
6 simpl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( K e. HL /\ W e. H ) )
7 eqid 
 |-  ( Base ` K ) = ( Base ` K )
8 7 1 2 3 trlcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( R ` F ) e. ( Base ` K ) )
9 eqid 
 |-  ( le ` K ) = ( le ` K )
10 9 1 2 3 trlle 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( R ` F ) ( le ` K ) W )
11 7 9 1 2 3 5 diaval 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( R ` F ) e. ( Base ` K ) /\ ( R ` F ) ( le ` K ) W ) ) -> ( I ` ( R ` F ) ) = { g e. T | ( R ` g ) ( le ` K ) ( R ` F ) } )
12 6 8 10 11 syl12anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( I ` ( R ` F ) ) = { g e. T | ( R ` g ) ( le ` K ) ( R ` F ) } )
13 9 1 2 3 4 dva1dim 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> { g | E. s e. E g = ( s ` F ) } = { g e. T | ( R ` g ) ( le ` K ) ( R ` F ) } )
14 12 13 eqtr4d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( I ` ( R ` F ) ) = { g | E. s e. E g = ( s ` F ) } )