Metamath Proof Explorer

Theorem dia1dim2

Description: Two expressions for a 1-dimensional subspace of partial vector space A (when F is a nonzero vector i.e. non-identity translation). (Contributed by NM, 15-Jan-2014) (Revised by Mario Carneiro, 22-Jun-2014)

Ref Expression
Hypotheses dia1dim2.h 
|- H = ( LHyp ` K )
dia1dim2.t 
|- T = ( ( LTrn ` K ) ` W )
dia1dim2.r 
|- R = ( ( trL ` K ) ` W )
dva1dim2.u 
|- U = ( ( DVecA ` K ) ` W )
dia1dim2.i 
|- I = ( ( DIsoA ` K ) ` W )
dva1dim2.n 
|- N = ( LSpan ` U )
Assertion dia1dim2 
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( I ` ( R ` F ) ) = ( N ` { F } ) )

Proof

Step Hyp Ref Expression
1 dia1dim2.h 
 |-  H = ( LHyp ` K )
2 dia1dim2.t 
 |-  T = ( ( LTrn ` K ) ` W )
3 dia1dim2.r 
 |-  R = ( ( trL ` K ) ` W )
4 dva1dim2.u 
 |-  U = ( ( DVecA ` K ) ` W )
5 dia1dim2.i 
 |-  I = ( ( DIsoA ` K ) ` W )
6 dva1dim2.n 
 |-  N = ( LSpan ` U )
7 eqid 
 |-  ( ( TEndo ` K ) ` W ) = ( ( TEndo ` K ) ` W )
8 eqid 
 |-  ( Scalar ` U ) = ( Scalar ` U )
9 eqid 
 |-  ( Base ` ( Scalar ` U ) ) = ( Base ` ( Scalar ` U ) )
10 1 7 4 8 9 dvabase 
 |-  ( ( K e. HL /\ W e. H ) -> ( Base ` ( Scalar ` U ) ) = ( ( TEndo ` K ) ` W ) )
11 10 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( Base ` ( Scalar ` U ) ) = ( ( TEndo ` K ) ` W ) )
12 11 rexeqdv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( E. s e. ( Base ` ( Scalar ` U ) ) g = ( s ( .s ` U ) F ) <-> E. s e. ( ( TEndo ` K ) ` W ) g = ( s ( .s ` U ) F ) ) )
13 eqid 
 |-  ( .s ` U ) = ( .s ` U )
14 1 2 7 4 13 dvavsca 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( s e. ( ( TEndo ` K ) ` W ) /\ F e. T ) ) -> ( s ( .s ` U ) F ) = ( s ` F ) )
15 14 anass1rs 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ s e. ( ( TEndo ` K ) ` W ) ) -> ( s ( .s ` U ) F ) = ( s ` F ) )
16 15 eqeq2d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ s e. ( ( TEndo ` K ) ` W ) ) -> ( g = ( s ( .s ` U ) F ) <-> g = ( s ` F ) ) )
17 16 rexbidva 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( E. s e. ( ( TEndo ` K ) ` W ) g = ( s ( .s ` U ) F ) <-> E. s e. ( ( TEndo ` K ) ` W ) g = ( s ` F ) ) )
18 12 17 bitrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( E. s e. ( Base ` ( Scalar ` U ) ) g = ( s ( .s ` U ) F ) <-> E. s e. ( ( TEndo ` K ) ` W ) g = ( s ` F ) ) )
19 18 abbidv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> { g | E. s e. ( Base ` ( Scalar ` U ) ) g = ( s ( .s ` U ) F ) } = { g | E. s e. ( ( TEndo ` K ) ` W ) g = ( s ` F ) } )
20 1 4 dvalvec 
 |-  ( ( K e. HL /\ W e. H ) -> U e. LVec )
21 20 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> U e. LVec )
22 lveclmod 
 |-  ( U e. LVec -> U e. LMod )
23 21 22 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> U e. LMod )
24 simpr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> F e. T )
25 eqid 
 |-  ( Base ` U ) = ( Base ` U )
26 1 2 4 25 dvavbase 
 |-  ( ( K e. HL /\ W e. H ) -> ( Base ` U ) = T )
27 26 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( Base ` U ) = T )
28 24 27 eleqtrrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> F e. ( Base ` U ) )
29 8 9 25 13 6 lspsn 
 |-  ( ( U e. LMod /\ F e. ( Base ` U ) ) -> ( N ` { F } ) = { g | E. s e. ( Base ` ( Scalar ` U ) ) g = ( s ( .s ` U ) F ) } )
30 23 28 29 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( N ` { F } ) = { g | E. s e. ( Base ` ( Scalar ` U ) ) g = ( s ( .s ` U ) F ) } )
31 1 2 3 7 5 dia1dim 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( I ` ( R ` F ) ) = { g | E. s e. ( ( TEndo ` K ) ` W ) g = ( s ` F ) } )
32 19 30 31 3eqtr4rd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( I ` ( R ` F ) ) = ( N ` { F } ) )