Theorem hdmapevec2

Description: The inner product of the reference vector E with itself is nonzero. This shows the inner product condition in the proof of Theorem 3.6 of Holland95 p. 14 line 32, [ e , e ] =/= 0 is satisfied. TODO: remove redundant hypothesis hdmapevec.j. (Contributed by NM, 1-Jun-2015)

	Ref	Expression
Hypotheses	hdmapevec.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hdmapevec.e	$$⊢E=⟨{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\mathrm{LTrn}\left(K\right)\left(W\right)}⟩$$
	hdmapevec.j	$$⊢J=\mathrm{HVMap}\left(K\right)\left(W\right)$$
	hdmapevec.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
	hdmapevec.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	hdmapevec2.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hdmapevec2.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
	hdmapevec2.i	$$⊢\underset{\dot{}}{1}=1_R$$
Assertion	hdmapevec2	$$⊢\phi \to S\left(E\right)\left(E\right)=\underset{\dot{}}{1}$$

Proof

Step	Hyp	Ref	Expression
1		hdmapevec.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hdmapevec.e	$$⊢E=⟨{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\mathrm{LTrn}\left(K\right)\left(W\right)}⟩$$
3		hdmapevec.j	$$⊢J=\mathrm{HVMap}\left(K\right)\left(W\right)$$
4		hdmapevec.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
5		hdmapevec.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
6		hdmapevec2.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
7		hdmapevec2.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
8		hdmapevec2.i	$$⊢\underset{\dot{}}{1}=1_R$$
9	1 2 3 4 5	hdmapevec	$$⊢\phi \to S\left(E\right)=J\left(E\right)$$
10		eqid	$$⊢\mathrm{ocH}\left(K\right)\left(W\right)=\mathrm{ocH}\left(K\right)\left(W\right)$$
11		eqid	$$⊢{\mathrm{Base}}_U={\mathrm{Base}}_U$$
12		eqid	$$⊢{+}_U={+}_U$$
13		eqid	$$⊢{\cdot }_U={\cdot }_U$$
14		eqid	$$⊢0_U=0_U$$
15		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
16		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
17		eqid	$$⊢\mathrm{LTrn}\left(K\right)\left(W\right)=\mathrm{LTrn}\left(K\right)\left(W\right)$$
18	1 16 17 6 11 14 2 5	dvheveccl	$$⊢\phi \to E\in \left({\mathrm{Base}}_U\setminus \left\{0_U\right\}\right)$$
19	1 6 10 11 12 13 14 7 15 3 5 18	hvmapval	$$⊢\phi \to J\left(E\right)=\left(v\in {\mathrm{Base}}_U⟼\left(\iota k\in {\mathrm{Base}}_R|\exists w\in \mathrm{ocH}\left(K\right)\left(W\right)\left(\left\{E\right\}\right)v=w{+}_U\left(k{\cdot }_{U}E\right)\right)\right)$$
20	9 19	eqtrd	$$⊢\phi \to S\left(E\right)=\left(v\in {\mathrm{Base}}_U⟼\left(\iota k\in {\mathrm{Base}}_R|\exists w\in \mathrm{ocH}\left(K\right)\left(W\right)\left(\left\{E\right\}\right)v=w{+}_U\left(k{\cdot }_{U}E\right)\right)\right)$$
21	20	fveq1d	$$⊢\phi \to S\left(E\right)\left(E\right)=\left(v\in {\mathrm{Base}}_U⟼\left(\iota k\in {\mathrm{Base}}_R|\exists w\in \mathrm{ocH}\left(K\right)\left(W\right)\left(\left\{E\right\}\right)v=w{+}_U\left(k{\cdot }_{U}E\right)\right)\right)\left(E\right)$$
22		eqid	$$⊢\left(v\in {\mathrm{Base}}_U⟼\left(\iota k\in {\mathrm{Base}}_R|\exists w\in \mathrm{ocH}\left(K\right)\left(W\right)\left(\left\{E\right\}\right)v=w{+}_U\left(k{\cdot }_{U}E\right)\right)\right)=\left(v\in {\mathrm{Base}}_U⟼\left(\iota k\in {\mathrm{Base}}_R|\exists w\in \mathrm{ocH}\left(K\right)\left(W\right)\left(\left\{E\right\}\right)v=w{+}_U\left(k{\cdot }_{U}E\right)\right)\right)$$
23	1 10 6 11 12 13 14 7 15 8 5 18 22	dochfl1	$$⊢\phi \to \left(v\in {\mathrm{Base}}_U⟼\left(\iota k\in {\mathrm{Base}}_R|\exists w\in \mathrm{ocH}\left(K\right)\left(W\right)\left(\left\{E\right\}\right)v=w{+}_U\left(k{\cdot }_{U}E\right)\right)\right)\left(E\right)=\underset{\dot{}}{1}$$
24	21 23	eqtrd	$$⊢\phi \to S\left(E\right)\left(E\right)=\underset{\dot{}}{1}$$