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