Metamath Proof Explorer

Theorem dvheveccl

Description: Properties of a unit vector that we will use later as a convenient reference vector. This vector is called "e" in the remark after Lemma M of Crawley p. 121. line 17. See also dvhopN and dihpN . (Contributed by NM, 27-Mar-2015)

Ref Expression
Hypotheses dvheveccl.h 
|- H = ( LHyp ` K )
dvheveccl.b 
|- B = ( Base ` K )
dvheveccl.t 
|- T = ( ( LTrn ` K ) ` W )
dvheveccl.u 
|- U = ( ( DVecH ` K ) ` W )
dvheveccl.v 
|- V = ( Base ` U )
dvheveccl.z 
|- .0. = ( 0g ` U )
dvheveccl.e 
|- E = <. ( _I |` B ) , ( _I |` T ) >.
dvheveccl.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
Assertion dvheveccl 
|- ( ph -> E e. ( V \ { .0. } ) )

Proof

Step Hyp Ref Expression
1 dvheveccl.h 
 |-  H = ( LHyp ` K )
2 dvheveccl.b 
 |-  B = ( Base ` K )
3 dvheveccl.t 
 |-  T = ( ( LTrn ` K ) ` W )
4 dvheveccl.u 
 |-  U = ( ( DVecH ` K ) ` W )
5 dvheveccl.v 
 |-  V = ( Base ` U )
6 dvheveccl.z 
 |-  .0. = ( 0g ` U )
7 dvheveccl.e 
 |-  E = <. ( _I |` B ) , ( _I |` T ) >.
8 dvheveccl.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
9 2 1 3 idltrn 
 |-  ( ( K e. HL /\ W e. H ) -> ( _I |` B ) e. T )
10 8 9 syl 
 |-  ( ph -> ( _I |` B ) e. T )
11 eqid 
 |-  ( ( TEndo ` K ) ` W ) = ( ( TEndo ` K ) ` W )
12 1 3 11 tendoidcl 
 |-  ( ( K e. HL /\ W e. H ) -> ( _I |` T ) e. ( ( TEndo ` K ) ` W ) )
13 8 12 syl 
 |-  ( ph -> ( _I |` T ) e. ( ( TEndo ` K ) ` W ) )
14 1 3 11 4 5 dvhelvbasei 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( _I |` B ) e. T /\ ( _I |` T ) e. ( ( TEndo ` K ) ` W ) ) ) -> <. ( _I |` B ) , ( _I |` T ) >. e. V )
15 8 10 13 14 syl12anc 
 |-  ( ph -> <. ( _I |` B ) , ( _I |` T ) >. e. V )
16 eqid 
 |-  ( f e. T |-> ( _I |` B ) ) = ( f e. T |-> ( _I |` B ) )
17 2 1 3 11 16 tendo1ne0 
 |-  ( ( K e. HL /\ W e. H ) -> ( _I |` T ) =/= ( f e. T |-> ( _I |` B ) ) )
18 8 17 syl 
 |-  ( ph -> ( _I |` T ) =/= ( f e. T |-> ( _I |` B ) ) )
19 2 1 3 4 6 16 dvh0g 
 |-  ( ( K e. HL /\ W e. H ) -> .0. = <. ( _I |` B ) , ( f e. T |-> ( _I |` B ) ) >. )
20 8 19 syl 
 |-  ( ph -> .0. = <. ( _I |` B ) , ( f e. T |-> ( _I |` B ) ) >. )
21 eqtr 
 |-  ( ( <. ( _I |` B ) , ( _I |` T ) >. = .0. /\ .0. = <. ( _I |` B ) , ( f e. T |-> ( _I |` B ) ) >. ) -> <. ( _I |` B ) , ( _I |` T ) >. = <. ( _I |` B ) , ( f e. T |-> ( _I |` B ) ) >. )
22 opthg 
 |-  ( ( ( _I |` B ) e. T /\ ( _I |` T ) e. ( ( TEndo ` K ) ` W ) ) -> ( <. ( _I |` B ) , ( _I |` T ) >. = <. ( _I |` B ) , ( f e. T |-> ( _I |` B ) ) >. <-> ( ( _I |` B ) = ( _I |` B ) /\ ( _I |` T ) = ( f e. T |-> ( _I |` B ) ) ) ) )
23 10 13 22 syl2anc 
 |-  ( ph -> ( <. ( _I |` B ) , ( _I |` T ) >. = <. ( _I |` B ) , ( f e. T |-> ( _I |` B ) ) >. <-> ( ( _I |` B ) = ( _I |` B ) /\ ( _I |` T ) = ( f e. T |-> ( _I |` B ) ) ) ) )
24 simpr 
 |-  ( ( ( _I |` B ) = ( _I |` B ) /\ ( _I |` T ) = ( f e. T |-> ( _I |` B ) ) ) -> ( _I |` T ) = ( f e. T |-> ( _I |` B ) ) )
25 23 24 syl6bi 
 |-  ( ph -> ( <. ( _I |` B ) , ( _I |` T ) >. = <. ( _I |` B ) , ( f e. T |-> ( _I |` B ) ) >. -> ( _I |` T ) = ( f e. T |-> ( _I |` B ) ) ) )
26 21 25 syl5 
 |-  ( ph -> ( ( <. ( _I |` B ) , ( _I |` T ) >. = .0. /\ .0. = <. ( _I |` B ) , ( f e. T |-> ( _I |` B ) ) >. ) -> ( _I |` T ) = ( f e. T |-> ( _I |` B ) ) ) )
27 20 26 mpan2d 
 |-  ( ph -> ( <. ( _I |` B ) , ( _I |` T ) >. = .0. -> ( _I |` T ) = ( f e. T |-> ( _I |` B ) ) ) )
28 27 necon3d 
 |-  ( ph -> ( ( _I |` T ) =/= ( f e. T |-> ( _I |` B ) ) -> <. ( _I |` B ) , ( _I |` T ) >. =/= .0. ) )
29 18 28 mpd 
 |-  ( ph -> <. ( _I |` B ) , ( _I |` T ) >. =/= .0. )
30 eldifsn 
 |-  ( <. ( _I |` B ) , ( _I |` T ) >. e. ( V \ { .0. } ) <-> ( <. ( _I |` B ) , ( _I |` T ) >. e. V /\ <. ( _I |` B ) , ( _I |` T ) >. =/= .0. ) )
31 15 29 30 sylanbrc 
 |-  ( ph -> <. ( _I |` B ) , ( _I |` T ) >. e. ( V \ { .0. } ) )
32 7 31 eqeltrid 
 |-  ( ph -> E e. ( V \ { .0. } ) )