Theorem dib1dim

Description: Two expressions for the 1-dimensional subspaces of vector space H. (Contributed by NM, 24-Feb-2014) (Revised by Mario Carneiro, 24-Jun-2014)

	Ref	Expression
Hypotheses	dib1dim.b	|- B = ( Base ` K )
	dib1dim.h	|- H = ( LHyp ` K )
	dib1dim.t	|- T = ( ( LTrn ` K ) ` W )
	dib1dim.r	|- R = ( ( trL ` K ) ` W )
	dib1dim.e	|- E = ( ( TEndo ` K ) ` W )
	dib1dim.o	|- O = ( h e. T |-> ( _I |` B ) )
	dib1dim.i	|- I = ( ( DIsoB ` K ) ` W )
Assertion	dib1dim	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( I ` ( R ` F ) ) = { g e. ( T X. E ) | E. s e. E g = <. ( s ` F ) , O >. } )

Proof

Step	Hyp	Ref	Expression
1		dib1dim.b	|- B = ( Base ` K )
2		dib1dim.h	|- H = ( LHyp ` K )
3		dib1dim.t	|- T = ( ( LTrn ` K ) ` W )
4		dib1dim.r	|- R = ( ( trL ` K ) ` W )
5		dib1dim.e	|- E = ( ( TEndo ` K ) ` W )
6		dib1dim.o	|- O = ( h e. T |-> ( _I |` B ) )
7		dib1dim.i	|- I = ( ( DIsoB ` K ) ` W )
8		simpl	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( K e. HL /\ W e. H ) )
9	1 2 3 4	trlcl	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( R ` F ) e. B )
10		eqid	|- ( le ` K ) = ( le ` K )
11	10 2 3 4	trlle	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( R ` F ) ( le ` K ) W )
12		eqid	|- ( ( DIsoA ` K ) ` W ) = ( ( DIsoA ` K ) ` W )
13	1 10 2 3 6 12 7	dibval2	|- ( ( ( K e. HL /\ W e. H ) /\ ( ( R ` F ) e. B /\ ( R ` F ) ( le ` K ) W ) ) -> ( I ` ( R ` F ) ) = ( ( ( ( DIsoA ` K ) ` W ) ` ( R ` F ) ) X. { O } ) )
14	8 9 11 13	syl12anc	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( I ` ( R ` F ) ) = ( ( ( ( DIsoA ` K ) ` W ) ` ( R ` F ) ) X. { O } ) )
15		relxp	|- Rel ( ( ( ( DIsoA ` K ) ` W ) ` ( R ` F ) ) X. { O } )
16		opelxp	|- ( <. f , t >. e. ( ( ( ( DIsoA ` K ) ` W ) ` ( R ` F ) ) X. { O } ) <-> ( f e. ( ( ( DIsoA ` K ) ` W ) ` ( R ` F ) ) /\ t e. { O } ) )
17	2 3 4 5 12	dia1dim	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( ( ( DIsoA ` K ) ` W ) ` ( R ` F ) ) = { f | E. s e. E f = ( s ` F ) } )
18	17	abeq2d	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( f e. ( ( ( DIsoA ` K ) ` W ) ` ( R ` F ) ) <-> E. s e. E f = ( s ` F ) ) )
19	18	anbi1d	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( ( f e. ( ( ( DIsoA ` K ) ` W ) ` ( R ` F ) ) /\ t e. { O } ) <-> ( E. s e. E f = ( s ` F ) /\ t e. { O } ) ) )
20	2 3 5	tendocl	|- ( ( ( K e. HL /\ W e. H ) /\ s e. E /\ F e. T ) -> ( s ` F ) e. T )
21	20	3expa	|- ( ( ( ( K e. HL /\ W e. H ) /\ s e. E ) /\ F e. T ) -> ( s ` F ) e. T )
22	21	an32s	|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ s e. E ) -> ( s ` F ) e. T )
23	1 2 3 5 6	tendo0cl	|- ( ( K e. HL /\ W e. H ) -> O e. E )
24	23	ad2antrr	|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ s e. E ) -> O e. E )
25	22 24	jca	|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ s e. E ) -> ( ( s ` F ) e. T /\ O e. E ) )
26		eleq1	|- ( f = ( s ` F ) -> ( f e. T <-> ( s ` F ) e. T ) )
27		eleq1	|- ( t = O -> ( t e. E <-> O e. E ) )
28	26 27	bi2anan9	|- ( ( f = ( s ` F ) /\ t = O ) -> ( ( f e. T /\ t e. E ) <-> ( ( s ` F ) e. T /\ O e. E ) ) )
29	25 28	syl5ibrcom	|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ s e. E ) -> ( ( f = ( s ` F ) /\ t = O ) -> ( f e. T /\ t e. E ) ) )
30	29	rexlimdva	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( E. s e. E ( f = ( s ` F ) /\ t = O ) -> ( f e. T /\ t e. E ) ) )
31	30	pm4.71rd	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( E. s e. E ( f = ( s ` F ) /\ t = O ) <-> ( ( f e. T /\ t e. E ) /\ E. s e. E ( f = ( s ` F ) /\ t = O ) ) ) )
32		velsn	|- ( t e. { O } <-> t = O )
33	32	anbi2i	|- ( ( E. s e. E f = ( s ` F ) /\ t e. { O } ) <-> ( E. s e. E f = ( s ` F ) /\ t = O ) )
34		r19.41v	|- ( E. s e. E ( f = ( s ` F ) /\ t = O ) <-> ( E. s e. E f = ( s ` F ) /\ t = O ) )
35	33 34	bitr4i	|- ( ( E. s e. E f = ( s ` F ) /\ t e. { O } ) <-> E. s e. E ( f = ( s ` F ) /\ t = O ) )
36		df-3an	|- ( ( f e. T /\ t e. E /\ E. s e. E ( f = ( s ` F ) /\ t = O ) ) <-> ( ( f e. T /\ t e. E ) /\ E. s e. E ( f = ( s ` F ) /\ t = O ) ) )
37	31 35 36	3bitr4g	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( ( E. s e. E f = ( s ` F ) /\ t e. { O } ) <-> ( f e. T /\ t e. E /\ E. s e. E ( f = ( s ` F ) /\ t = O ) ) ) )
38	19 37	bitrd	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( ( f e. ( ( ( DIsoA ` K ) ` W ) ` ( R ` F ) ) /\ t e. { O } ) <-> ( f e. T /\ t e. E /\ E. s e. E ( f = ( s ` F ) /\ t = O ) ) ) )
39	16 38	syl5bb	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( <. f , t >. e. ( ( ( ( DIsoA ` K ) ` W ) ` ( R ` F ) ) X. { O } ) <-> ( f e. T /\ t e. E /\ E. s e. E ( f = ( s ` F ) /\ t = O ) ) ) )
40	15 39	opabbi2dv	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( ( ( ( DIsoA ` K ) ` W ) ` ( R ` F ) ) X. { O } ) = { <. f , t >. | ( f e. T /\ t e. E /\ E. s e. E ( f = ( s ` F ) /\ t = O ) ) } )
41	14 40	eqtrd	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( I ` ( R ` F ) ) = { <. f , t >. | ( f e. T /\ t e. E /\ E. s e. E ( f = ( s ` F ) /\ t = O ) ) } )
42		eqeq1	|- ( g = <. f , t >. -> ( g = <. ( s ` F ) , O >. <-> <. f , t >. = <. ( s ` F ) , O >. ) )
43		vex	|- f e. _V
44		vex	|- t e. _V
45	43 44	opth	|- ( <. f , t >. = <. ( s ` F ) , O >. <-> ( f = ( s ` F ) /\ t = O ) )
46	42 45	syl6bb	|- ( g = <. f , t >. -> ( g = <. ( s ` F ) , O >. <-> ( f = ( s ` F ) /\ t = O ) ) )
47	46	rexbidv	|- ( g = <. f , t >. -> ( E. s e. E g = <. ( s ` F ) , O >. <-> E. s e. E ( f = ( s ` F ) /\ t = O ) ) )
48	47	rabxp	|- { g e. ( T X. E ) | E. s e. E g = <. ( s ` F ) , O >. } = { <. f , t >. | ( f e. T /\ t e. E /\ E. s e. E ( f = ( s ` F ) /\ t = O ) ) }
49	41 48	eqtr4di	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( I ` ( R ` F ) ) = { g e. ( T X. E ) | E. s e. E g = <. ( s ` F ) , O >. } )