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