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

Metamath Proof Explorer

Theorem dih1dimb

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, 27-Apr-2014)

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

Proof

Step Hyp Ref Expression
1 dih1dimb.b 
 |-  B = ( Base ` K )
2 dih1dimb.h 
 |-  H = ( LHyp ` K )
3 dih1dimb.t 
 |-  T = ( ( LTrn ` K ) ` W )
4 dih1dimb.r 
 |-  R = ( ( trL ` K ) ` W )
5 dih1dimb.o 
 |-  O = ( h e. T |-> ( _I |` B ) )
6 dih1dimb.u 
 |-  U = ( ( DVecH ` K ) ` W )
7 dih1dimb.i 
 |-  I = ( ( DIsoH ` K ) ` W )
8 dih1dimb.n 
 |-  N = ( LSpan ` U )
9 simpl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( K e. HL /\ W e. H ) )
10 1 2 3 4 trlcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( R ` F ) e. B )
11 eqid 
 |-  ( le ` K ) = ( le ` K )
12 11 2 3 4 trlle 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( R ` F ) ( le ` K ) W )
13 eqid 
 |-  ( ( DIsoB ` K ) ` W ) = ( ( DIsoB ` K ) ` W )
14 1 11 2 7 13 dihvalb 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( R ` F ) e. B /\ ( R ` F ) ( le ` K ) W ) ) -> ( I ` ( R ` F ) ) = ( ( ( DIsoB ` K ) ` W ) ` ( R ` F ) ) )
15 9 10 12 14 syl12anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( I ` ( R ` F ) ) = ( ( ( DIsoB ` K ) ` W ) ` ( R ` F ) ) )
16 1 2 3 4 5 6 13 8 dib1dim2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( ( ( DIsoB ` K ) ` W ) ` ( R ` F ) ) = ( N ` { <. F , O >. } ) )
17 15 16 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( I ` ( R ` F ) ) = ( N ` { <. F , O >. } ) )