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