This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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