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