Theorem dib1dim2

Description: Two expressions for a 1-dimensional subspace of vector space H (when F is a nonzero vector i.e. non-identity translation). (Contributed by NM, 24-Feb-2014)

	Ref	Expression
Hypotheses	dib1dim2.b	|- B = ( Base ` K )
	dib1dim2.h	|- H = ( LHyp ` K )
	dib1dim2.t	|- T = ( ( LTrn ` K ) ` W )
	dib1dim2.r	|- R = ( ( trL ` K ) ` W )
	dib1dim2.o	|- O = ( h e. T |-> ( _I |` B ) )
	dib1dim2.u	|- U = ( ( DVecH ` K ) ` W )
	dib1dim2.i	|- I = ( ( DIsoB ` K ) ` W )
	dib1dim2.n	|- N = ( LSpan ` U )
Assertion	dib1dim2	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( I ` ( R ` F ) ) = ( N ` { <. F , O >. } ) )

Proof

Step	Hyp	Ref	Expression
1		dib1dim2.b	|- B = ( Base ` K )
2		dib1dim2.h	|- H = ( LHyp ` K )
3		dib1dim2.t	|- T = ( ( LTrn ` K ) ` W )
4		dib1dim2.r	|- R = ( ( trL ` K ) ` W )
5		dib1dim2.o	|- O = ( h e. T |-> ( _I |` B ) )
6		dib1dim2.u	|- U = ( ( DVecH ` K ) ` W )
7		dib1dim2.i	|- I = ( ( DIsoB ` K ) ` W )
8		dib1dim2.n	|- N = ( LSpan ` U )
9		df-rab	|- { u e. ( T X. ( ( TEndo ` K ) ` W ) ) | E. v e. ( ( TEndo ` K ) ` W ) u = <. ( v ` F ) , O >. } = { u | ( u e. ( T X. ( ( TEndo ` K ) ` W ) ) /\ E. v e. ( ( TEndo ` K ) ` W ) u = <. ( v ` F ) , O >. ) }
10		eqid	|- ( ( TEndo ` K ) ` W ) = ( ( TEndo ` K ) ` W )
11	1 2 3 4 10 5 7	dib1dim	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( I ` ( R ` F ) ) = { u e. ( T X. ( ( TEndo ` K ) ` W ) ) | E. v e. ( ( TEndo ` K ) ` W ) u = <. ( v ` F ) , O >. } )
12		eqid	|- ( Scalar ` U ) = ( Scalar ` U )
13		eqid	|- ( Base ` ( Scalar ` U ) ) = ( Base ` ( Scalar ` U ) )
14	2 10 6 12 13	dvhbase	|- ( ( K e. HL /\ W e. H ) -> ( Base ` ( Scalar ` U ) ) = ( ( TEndo ` K ) ` W ) )
15	14	adantr	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( Base ` ( Scalar ` U ) ) = ( ( TEndo ` K ) ` W ) )
16	15	rexeqdv	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( E. v e. ( Base ` ( Scalar ` U ) ) u = ( v ( .s ` U ) <. F , O >. ) <-> E. v e. ( ( TEndo ` K ) ` W ) u = ( v ( .s ` U ) <. F , O >. ) ) )
17		simpll	|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ v e. ( ( TEndo ` K ) ` W ) ) -> ( K e. HL /\ W e. H ) )
18		simpr	|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ v e. ( ( TEndo ` K ) ` W ) ) -> v e. ( ( TEndo ` K ) ` W ) )
19		simplr	|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ v e. ( ( TEndo ` K ) ` W ) ) -> F e. T )
20	1 2 3 10 5	tendo0cl	|- ( ( K e. HL /\ W e. H ) -> O e. ( ( TEndo ` K ) ` W ) )
21	20	ad2antrr	|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ v e. ( ( TEndo ` K ) ` W ) ) -> O e. ( ( TEndo ` K ) ` W ) )
22		eqid	|- ( .s ` U ) = ( .s ` U )
23	2 3 10 6 22	dvhopvsca	|- ( ( ( K e. HL /\ W e. H ) /\ ( v e. ( ( TEndo ` K ) ` W ) /\ F e. T /\ O e. ( ( TEndo ` K ) ` W ) ) ) -> ( v ( .s ` U ) <. F , O >. ) = <. ( v ` F ) , ( v o. O ) >. )
24	17 18 19 21 23	syl13anc	|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ v e. ( ( TEndo ` K ) ` W ) ) -> ( v ( .s ` U ) <. F , O >. ) = <. ( v ` F ) , ( v o. O ) >. )
25	1 2 3 10 5	tendo0mulr	|- ( ( ( K e. HL /\ W e. H ) /\ v e. ( ( TEndo ` K ) ` W ) ) -> ( v o. O ) = O )
26	25	adantlr	|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ v e. ( ( TEndo ` K ) ` W ) ) -> ( v o. O ) = O )
27	26	opeq2d	|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ v e. ( ( TEndo ` K ) ` W ) ) -> <. ( v ` F ) , ( v o. O ) >. = <. ( v ` F ) , O >. )
28	24 27	eqtrd	|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ v e. ( ( TEndo ` K ) ` W ) ) -> ( v ( .s ` U ) <. F , O >. ) = <. ( v ` F ) , O >. )
29	28	eqeq2d	|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ v e. ( ( TEndo ` K ) ` W ) ) -> ( u = ( v ( .s ` U ) <. F , O >. ) <-> u = <. ( v ` F ) , O >. ) )
30	29	rexbidva	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( E. v e. ( ( TEndo ` K ) ` W ) u = ( v ( .s ` U ) <. F , O >. ) <-> E. v e. ( ( TEndo ` K ) ` W ) u = <. ( v ` F ) , O >. ) )
31	2 3 10	tendocl	|- ( ( ( K e. HL /\ W e. H ) /\ v e. ( ( TEndo ` K ) ` W ) /\ F e. T ) -> ( v ` F ) e. T )
32	31	3expa	|- ( ( ( ( K e. HL /\ W e. H ) /\ v e. ( ( TEndo ` K ) ` W ) ) /\ F e. T ) -> ( v ` F ) e. T )
33	32	an32s	|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ v e. ( ( TEndo ` K ) ` W ) ) -> ( v ` F ) e. T )
34		opelxpi	|- ( ( ( v ` F ) e. T /\ O e. ( ( TEndo ` K ) ` W ) ) -> <. ( v ` F ) , O >. e. ( T X. ( ( TEndo ` K ) ` W ) ) )
35	33 21 34	syl2anc	|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ v e. ( ( TEndo ` K ) ` W ) ) -> <. ( v ` F ) , O >. e. ( T X. ( ( TEndo ` K ) ` W ) ) )
36		eleq1a	|- ( <. ( v ` F ) , O >. e. ( T X. ( ( TEndo ` K ) ` W ) ) -> ( u = <. ( v ` F ) , O >. -> u e. ( T X. ( ( TEndo ` K ) ` W ) ) ) )
37	35 36	syl	|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ v e. ( ( TEndo ` K ) ` W ) ) -> ( u = <. ( v ` F ) , O >. -> u e. ( T X. ( ( TEndo ` K ) ` W ) ) ) )
38	37	rexlimdva	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( E. v e. ( ( TEndo ` K ) ` W ) u = <. ( v ` F ) , O >. -> u e. ( T X. ( ( TEndo ` K ) ` W ) ) ) )
39	38	pm4.71rd	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( E. v e. ( ( TEndo ` K ) ` W ) u = <. ( v ` F ) , O >. <-> ( u e. ( T X. ( ( TEndo ` K ) ` W ) ) /\ E. v e. ( ( TEndo ` K ) ` W ) u = <. ( v ` F ) , O >. ) ) )
40	16 30 39	3bitrd	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( E. v e. ( Base ` ( Scalar ` U ) ) u = ( v ( .s ` U ) <. F , O >. ) <-> ( u e. ( T X. ( ( TEndo ` K ) ` W ) ) /\ E. v e. ( ( TEndo ` K ) ` W ) u = <. ( v ` F ) , O >. ) ) )
41	40	abbidv	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> { u | E. v e. ( Base ` ( Scalar ` U ) ) u = ( v ( .s ` U ) <. F , O >. ) } = { u | ( u e. ( T X. ( ( TEndo ` K ) ` W ) ) /\ E. v e. ( ( TEndo ` K ) ` W ) u = <. ( v ` F ) , O >. ) } )
42	9 11 41	3eqtr4a	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( I ` ( R ` F ) ) = { u | E. v e. ( Base ` ( Scalar ` U ) ) u = ( v ( .s ` U ) <. F , O >. ) } )
43		simpl	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( K e. HL /\ W e. H ) )
44	2 6 43	dvhlmod	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> U e. LMod )
45		simpr	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> F e. T )
46	20	adantr	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> O e. ( ( TEndo ` K ) ` W ) )
47		eqid	|- ( Base ` U ) = ( Base ` U )
48	2 3 10 6 47	dvhelvbasei	|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ O e. ( ( TEndo ` K ) ` W ) ) ) -> <. F , O >. e. ( Base ` U ) )
49	43 45 46 48	syl12anc	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> <. F , O >. e. ( Base ` U ) )
50	12 13 47 22 8	lspsn	|- ( ( U e. LMod /\ <. F , O >. e. ( Base ` U ) ) -> ( N ` { <. F , O >. } ) = { u | E. v e. ( Base ` ( Scalar ` U ) ) u = ( v ( .s ` U ) <. F , O >. ) } )
51	44 49 50	syl2anc	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( N ` { <. F , O >. } ) = { u | E. v e. ( Base ` ( Scalar ` U ) ) u = ( v ( .s ` U ) <. F , O >. ) } )
52	42 51	eqtr4d	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( I ` ( R ` F ) ) = ( N ` { <. F , O >. } ) )