# 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}=\mathrm{LHyp}\left({K}\right)$
dvheveccl.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
dvheveccl.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
dvheveccl.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
dvheveccl.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
dvheveccl.z
dvheveccl.e ${⊢}{E}=⟨{\mathrm{I}↾}_{{B}},{\mathrm{I}↾}_{{T}}⟩$
dvheveccl.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
Assertion dvheveccl

### Proof

Step Hyp Ref Expression
1 dvheveccl.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 dvheveccl.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
3 dvheveccl.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
4 dvheveccl.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
5 dvheveccl.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
6 dvheveccl.z
7 dvheveccl.e ${⊢}{E}=⟨{\mathrm{I}↾}_{{B}},{\mathrm{I}↾}_{{T}}⟩$
8 dvheveccl.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
9 2 1 3 idltrn ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {\mathrm{I}↾}_{{B}}\in {T}$
10 8 9 syl ${⊢}{\phi }\to {\mathrm{I}↾}_{{B}}\in {T}$
11 eqid ${⊢}\mathrm{TEndo}\left({K}\right)\left({W}\right)=\mathrm{TEndo}\left({K}\right)\left({W}\right)$
12 1 3 11 tendoidcl ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {\mathrm{I}↾}_{{T}}\in \mathrm{TEndo}\left({K}\right)\left({W}\right)$
13 8 12 syl ${⊢}{\phi }\to {\mathrm{I}↾}_{{T}}\in \mathrm{TEndo}\left({K}\right)\left({W}\right)$
14 1 3 11 4 5 dvhelvbasei ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({\mathrm{I}↾}_{{B}}\in {T}\wedge {\mathrm{I}↾}_{{T}}\in \mathrm{TEndo}\left({K}\right)\left({W}\right)\right)\right)\to ⟨{\mathrm{I}↾}_{{B}},{\mathrm{I}↾}_{{T}}⟩\in {V}$
15 8 10 13 14 syl12anc ${⊢}{\phi }\to ⟨{\mathrm{I}↾}_{{B}},{\mathrm{I}↾}_{{T}}⟩\in {V}$
16 eqid ${⊢}\left({f}\in {T}⟼{\mathrm{I}↾}_{{B}}\right)=\left({f}\in {T}⟼{\mathrm{I}↾}_{{B}}\right)$
17 2 1 3 11 16 tendo1ne0 ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {\mathrm{I}↾}_{{T}}\ne \left({f}\in {T}⟼{\mathrm{I}↾}_{{B}}\right)$
18 8 17 syl ${⊢}{\phi }\to {\mathrm{I}↾}_{{T}}\ne \left({f}\in {T}⟼{\mathrm{I}↾}_{{B}}\right)$
19 2 1 3 4 6 16 dvh0g
20 8 19 syl
21 eqtr
22 opthg ${⊢}\left({\mathrm{I}↾}_{{B}}\in {T}\wedge {\mathrm{I}↾}_{{T}}\in \mathrm{TEndo}\left({K}\right)\left({W}\right)\right)\to \left(⟨{\mathrm{I}↾}_{{B}},{\mathrm{I}↾}_{{T}}⟩=⟨{\mathrm{I}↾}_{{B}},\left({f}\in {T}⟼{\mathrm{I}↾}_{{B}}\right)⟩↔\left({\mathrm{I}↾}_{{B}}={\mathrm{I}↾}_{{B}}\wedge {\mathrm{I}↾}_{{T}}=\left({f}\in {T}⟼{\mathrm{I}↾}_{{B}}\right)\right)\right)$
23 10 13 22 syl2anc ${⊢}{\phi }\to \left(⟨{\mathrm{I}↾}_{{B}},{\mathrm{I}↾}_{{T}}⟩=⟨{\mathrm{I}↾}_{{B}},\left({f}\in {T}⟼{\mathrm{I}↾}_{{B}}\right)⟩↔\left({\mathrm{I}↾}_{{B}}={\mathrm{I}↾}_{{B}}\wedge {\mathrm{I}↾}_{{T}}=\left({f}\in {T}⟼{\mathrm{I}↾}_{{B}}\right)\right)\right)$
24 simpr ${⊢}\left({\mathrm{I}↾}_{{B}}={\mathrm{I}↾}_{{B}}\wedge {\mathrm{I}↾}_{{T}}=\left({f}\in {T}⟼{\mathrm{I}↾}_{{B}}\right)\right)\to {\mathrm{I}↾}_{{T}}=\left({f}\in {T}⟼{\mathrm{I}↾}_{{B}}\right)$
25 23 24 syl6bi ${⊢}{\phi }\to \left(⟨{\mathrm{I}↾}_{{B}},{\mathrm{I}↾}_{{T}}⟩=⟨{\mathrm{I}↾}_{{B}},\left({f}\in {T}⟼{\mathrm{I}↾}_{{B}}\right)⟩\to {\mathrm{I}↾}_{{T}}=\left({f}\in {T}⟼{\mathrm{I}↾}_{{B}}\right)\right)$
26 21 25 syl5
27 20 26 mpan2d
28 27 necon3d
29 18 28 mpd
30 eldifsn
31 15 29 30 sylanbrc
32 7 31 eqeltrid