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	$$⊢\underset{\dot{}}{0}=0_U$$
	dvheveccl.e	$$⊢E=⟨{\mathrm{I}\upharpoonright }_B,{\mathrm{I}\upharpoonright }_T⟩$$
	dvheveccl.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
Assertion	dvheveccl	$$⊢\phi \to E\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$

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	$$⊢\underset{\dot{}}{0}=0_U$$
7		dvheveccl.e	$$⊢E=⟨{\mathrm{I}\upharpoonright }_B,{\mathrm{I}\upharpoonright }_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}\upharpoonright }_B\in T$$
10	8 9	syl	$$⊢\phi \to {\mathrm{I}\upharpoonright }_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}\upharpoonright }_T\in \mathrm{TEndo}\left(K\right)\left(W\right)$$
13	8 12	syl	$$⊢\phi \to {\mathrm{I}\upharpoonright }_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}\upharpoonright }_B\in T\wedge {\mathrm{I}\upharpoonright }_T\in \mathrm{TEndo}\left(K\right)\left(W\right)\right)\right)\to ⟨{\mathrm{I}\upharpoonright }_B,{\mathrm{I}\upharpoonright }_T⟩\in V$$
15	8 10 13 14	syl12anc	$$⊢\phi \to ⟨{\mathrm{I}\upharpoonright }_B,{\mathrm{I}\upharpoonright }_T⟩\in V$$
16		eqid	$$⊢\left(f\in T⟼{\mathrm{I}\upharpoonright }_B\right)=\left(f\in T⟼{\mathrm{I}\upharpoonright }_B\right)$$
17	2 1 3 11 16	tendo1ne0	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to {\mathrm{I}\upharpoonright }_T\ne \left(f\in T⟼{\mathrm{I}\upharpoonright }_B\right)$$
18	8 17	syl	$$⊢\phi \to {\mathrm{I}\upharpoonright }_T\ne \left(f\in T⟼{\mathrm{I}\upharpoonright }_B\right)$$
19	2 1 3 4 6 16	dvh0g	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to \underset{\dot{}}{0}=⟨{\mathrm{I}\upharpoonright }_B,\left(f\in T⟼{\mathrm{I}\upharpoonright }_B\right)⟩$$
20	8 19	syl	$$⊢\phi \to \underset{\dot{}}{0}=⟨{\mathrm{I}\upharpoonright }_B,\left(f\in T⟼{\mathrm{I}\upharpoonright }_B\right)⟩$$
21		eqtr	$$⊢\left(⟨{\mathrm{I}\upharpoonright }_B,{\mathrm{I}\upharpoonright }_T⟩=\underset{\dot{}}{0}\wedge \underset{\dot{}}{0}=⟨{\mathrm{I}\upharpoonright }_B,\left(f\in T⟼{\mathrm{I}\upharpoonright }_B\right)⟩\right)\to ⟨{\mathrm{I}\upharpoonright }_B,{\mathrm{I}\upharpoonright }_T⟩=⟨{\mathrm{I}\upharpoonright }_B,\left(f\in T⟼{\mathrm{I}\upharpoonright }_B\right)⟩$$
22		opthg	$$⊢\left({\mathrm{I}\upharpoonright }_B\in T\wedge {\mathrm{I}\upharpoonright }_T\in \mathrm{TEndo}\left(K\right)\left(W\right)\right)\to \left(⟨{\mathrm{I}\upharpoonright }_B,{\mathrm{I}\upharpoonright }_T⟩=⟨{\mathrm{I}\upharpoonright }_B,\left(f\in T⟼{\mathrm{I}\upharpoonright }_B\right)⟩\leftrightarrow \left({\mathrm{I}\upharpoonright }_B={\mathrm{I}\upharpoonright }_B\wedge {\mathrm{I}\upharpoonright }_T=\left(f\in T⟼{\mathrm{I}\upharpoonright }_B\right)\right)\right)$$
23	10 13 22	syl2anc	$$⊢\phi \to \left(⟨{\mathrm{I}\upharpoonright }_B,{\mathrm{I}\upharpoonright }_T⟩=⟨{\mathrm{I}\upharpoonright }_B,\left(f\in T⟼{\mathrm{I}\upharpoonright }_B\right)⟩\leftrightarrow \left({\mathrm{I}\upharpoonright }_B={\mathrm{I}\upharpoonright }_B\wedge {\mathrm{I}\upharpoonright }_T=\left(f\in T⟼{\mathrm{I}\upharpoonright }_B\right)\right)\right)$$
24		simpr	$$⊢\left({\mathrm{I}\upharpoonright }_B={\mathrm{I}\upharpoonright }_B\wedge {\mathrm{I}\upharpoonright }_T=\left(f\in T⟼{\mathrm{I}\upharpoonright }_B\right)\right)\to {\mathrm{I}\upharpoonright }_T=\left(f\in T⟼{\mathrm{I}\upharpoonright }_B\right)$$
25	23 24	biimtrdi	$$⊢\phi \to \left(⟨{\mathrm{I}\upharpoonright }_B,{\mathrm{I}\upharpoonright }_T⟩=⟨{\mathrm{I}\upharpoonright }_B,\left(f\in T⟼{\mathrm{I}\upharpoonright }_B\right)⟩\to {\mathrm{I}\upharpoonright }_T=\left(f\in T⟼{\mathrm{I}\upharpoonright }_B\right)\right)$$
26	21 25	syl5	$$⊢\phi \to \left(\left(⟨{\mathrm{I}\upharpoonright }_B,{\mathrm{I}\upharpoonright }_T⟩=\underset{\dot{}}{0}\wedge \underset{\dot{}}{0}=⟨{\mathrm{I}\upharpoonright }_B,\left(f\in T⟼{\mathrm{I}\upharpoonright }_B\right)⟩\right)\to {\mathrm{I}\upharpoonright }_T=\left(f\in T⟼{\mathrm{I}\upharpoonright }_B\right)\right)$$
27	20 26	mpan2d	$$⊢\phi \to \left(⟨{\mathrm{I}\upharpoonright }_B,{\mathrm{I}\upharpoonright }_T⟩=\underset{\dot{}}{0}\to {\mathrm{I}\upharpoonright }_T=\left(f\in T⟼{\mathrm{I}\upharpoonright }_B\right)\right)$$
28	27	necon3d	$$⊢\phi \to \left({\mathrm{I}\upharpoonright }_T\ne \left(f\in T⟼{\mathrm{I}\upharpoonright }_B\right)\to ⟨{\mathrm{I}\upharpoonright }_B,{\mathrm{I}\upharpoonright }_T⟩\ne \underset{\dot{}}{0}\right)$$
29	18 28	mpd	$$⊢\phi \to ⟨{\mathrm{I}\upharpoonright }_B,{\mathrm{I}\upharpoonright }_T⟩\ne \underset{\dot{}}{0}$$
30		eldifsn	$$⊢⟨{\mathrm{I}\upharpoonright }_B,{\mathrm{I}\upharpoonright }_T⟩\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow \left(⟨{\mathrm{I}\upharpoonright }_B,{\mathrm{I}\upharpoonright }_T⟩\in V\wedge ⟨{\mathrm{I}\upharpoonright }_B,{\mathrm{I}\upharpoonright }_T⟩\ne \underset{\dot{}}{0}\right)$$
31	15 29 30	sylanbrc	$$⊢\phi \to ⟨{\mathrm{I}\upharpoonright }_B,{\mathrm{I}\upharpoonright }_T⟩\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
32	7 31	eqeltrid	$$⊢\phi \to E\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$