Theorem hdmapip1

Description: Construct a proportional vector Y whose inner product with the original X equals one. (Contributed by NM, 13-Jun-2015)

	Ref	Expression
Hypotheses	hdmapip1.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hdmapip1.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hdmapip1.v	$$⊢V={\mathrm{Base}}_U$$
	hdmapip1.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
	hdmapip1.o	$$⊢\underset{\dot{}}{0}=0_U$$
	hdmapip1.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
	hdmapip1.i	$$⊢\underset{\dot{}}{1}=1_R$$
	hdmapip1.n	$$⊢N={inv}_r\left(R\right)$$
	hdmapip1.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
	hdmapip1.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	hdmapip1.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	hdmapip1.y	$$⊢Y=N\left(S\left(X\right)\left(X\right)\right)\underset{\dot{}}{·}X$$
Assertion	hdmapip1	$$⊢\phi \to S\left(X\right)\left(Y\right)=\underset{\dot{}}{1}$$

Proof

Step	Hyp	Ref	Expression
1		hdmapip1.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hdmapip1.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		hdmapip1.v	$$⊢V={\mathrm{Base}}_U$$
4		hdmapip1.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
5		hdmapip1.o	$$⊢\underset{\dot{}}{0}=0_U$$
6		hdmapip1.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
7		hdmapip1.i	$$⊢\underset{\dot{}}{1}=1_R$$
8		hdmapip1.n	$$⊢N={inv}_r\left(R\right)$$
9		hdmapip1.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
10		hdmapip1.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
11		hdmapip1.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
12		hdmapip1.y	$$⊢Y=N\left(S\left(X\right)\left(X\right)\right)\underset{\dot{}}{·}X$$
13	12	fveq2i	$$⊢S\left(X\right)\left(Y\right)=S\left(X\right)\left(N\left(S\left(X\right)\left(X\right)\right)\underset{\dot{}}{·}X\right)$$
14		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
15		eqid	$$⊢{\cdot }_R={\cdot }_R$$
16	11	eldifad	$$⊢\phi \to X\in V$$
17	1 2 10	dvhlvec	$$⊢\phi \to U\in \mathrm{LVec}$$
18	6	lvecdrng	$$⊢U\in \mathrm{LVec}\to R\in \mathrm{DivRing}$$
19	17 18	syl	$$⊢\phi \to R\in \mathrm{DivRing}$$
20	1 2 3 6 14 9 10 16 16	hdmapipcl	$$⊢\phi \to S\left(X\right)\left(X\right)\in {\mathrm{Base}}_R$$
21		eldifsni	$$⊢X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\to X\ne \underset{\dot{}}{0}$$
22	11 21	syl	$$⊢\phi \to X\ne \underset{\dot{}}{0}$$
23		eqid	$$⊢0_R=0_R$$
24	1 2 3 5 6 23 9 10 16	hdmapip0	$$⊢\phi \to \left(S\left(X\right)\left(X\right)=0_R\leftrightarrow X=\underset{\dot{}}{0}\right)$$
25	24	necon3bid	$$⊢\phi \to \left(S\left(X\right)\left(X\right)\ne 0_R\leftrightarrow X\ne \underset{\dot{}}{0}\right)$$
26	22 25	mpbird	$$⊢\phi \to S\left(X\right)\left(X\right)\ne 0_R$$
27	14 23 8	drnginvrcl	$$⊢\left(R\in \mathrm{DivRing}\wedge S\left(X\right)\left(X\right)\in {\mathrm{Base}}_R\wedge S\left(X\right)\left(X\right)\ne 0_R\right)\to N\left(S\left(X\right)\left(X\right)\right)\in {\mathrm{Base}}_R$$
28	19 20 26 27	syl3anc	$$⊢\phi \to N\left(S\left(X\right)\left(X\right)\right)\in {\mathrm{Base}}_R$$
29	1 2 3 4 6 14 15 9 10 16 16 28	hdmaplnm1	$$⊢\phi \to S\left(X\right)\left(N\left(S\left(X\right)\left(X\right)\right)\underset{\dot{}}{·}X\right)=N\left(S\left(X\right)\left(X\right)\right){\cdot }_{R}S\left(X\right)\left(X\right)$$
30	14 23 15 7 8	drnginvrl	$$⊢\left(R\in \mathrm{DivRing}\wedge S\left(X\right)\left(X\right)\in {\mathrm{Base}}_R\wedge S\left(X\right)\left(X\right)\ne 0_R\right)\to N\left(S\left(X\right)\left(X\right)\right){\cdot }_{R}S\left(X\right)\left(X\right)=\underset{\dot{}}{1}$$
31	19 20 26 30	syl3anc	$$⊢\phi \to N\left(S\left(X\right)\left(X\right)\right){\cdot }_{R}S\left(X\right)\left(X\right)=\underset{\dot{}}{1}$$
32	29 31	eqtrd	$$⊢\phi \to S\left(X\right)\left(N\left(S\left(X\right)\left(X\right)\right)\underset{\dot{}}{·}X\right)=\underset{\dot{}}{1}$$
33	13 32	syl5eq	$$⊢\phi \to S\left(X\right)\left(Y\right)=\underset{\dot{}}{1}$$