Theorem hdmapinvlem1

Description: Line 27 in Baer p. 110. We use C for Baer's u. Our unit vector E has the required properties for his w by hdmapevec2 . Our ( ( SE )C ) means the inner product <. C , E >. i.e. his f(u,w) (note argument reversal). (Contributed by NM, 11-Jun-2015)

	Ref	Expression
Hypotheses	hdmapinvlem1.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hdmapinvlem1.e	$$⊢E=⟨{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\mathrm{LTrn}\left(K\right)\left(W\right)}⟩$$
	hdmapinvlem1.o	$$⊢O=\mathrm{ocH}\left(K\right)\left(W\right)$$
	hdmapinvlem1.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hdmapinvlem1.v	$$⊢V={\mathrm{Base}}_U$$
	hdmapinvlem1.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
	hdmapinvlem1.b	$$⊢B={\mathrm{Base}}_R$$
	hdmapinvlem1.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	hdmapinvlem1.z	$$⊢\underset{\dot{}}{0}=0_R$$
	hdmapinvlem1.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
	hdmapinvlem1.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	hdmapinvlem1.c	$$⊢\phi \to C\in O\left(\left\{E\right\}\right)$$
Assertion	hdmapinvlem1	$$⊢\phi \to S\left(E\right)\left(C\right)=\underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		hdmapinvlem1.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hdmapinvlem1.e	$$⊢E=⟨{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\mathrm{LTrn}\left(K\right)\left(W\right)}⟩$$
3		hdmapinvlem1.o	$$⊢O=\mathrm{ocH}\left(K\right)\left(W\right)$$
4		hdmapinvlem1.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
5		hdmapinvlem1.v	$$⊢V={\mathrm{Base}}_U$$
6		hdmapinvlem1.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
7		hdmapinvlem1.b	$$⊢B={\mathrm{Base}}_R$$
8		hdmapinvlem1.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
9		hdmapinvlem1.z	$$⊢\underset{\dot{}}{0}=0_R$$
10		hdmapinvlem1.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
11		hdmapinvlem1.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
12		hdmapinvlem1.c	$$⊢\phi \to C\in O\left(\left\{E\right\}\right)$$
13		eqid	$$⊢\mathrm{LFnl}\left(U\right)=\mathrm{LFnl}\left(U\right)$$
14		eqid	$$⊢\mathrm{LKer}\left(U\right)=\mathrm{LKer}\left(U\right)$$
15		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
16		eqid	$$⊢\mathrm{LTrn}\left(K\right)\left(W\right)=\mathrm{LTrn}\left(K\right)\left(W\right)$$
17		eqid	$$⊢0_U=0_U$$
18	1 15 16 4 5 17 2 11	dvheveccl	$$⊢\phi \to E\in \left(V\setminus \left\{0_U\right\}\right)$$
19	18	eldifad	$$⊢\phi \to E\in V$$
20	1 3 4 5 13 14 10 11 19	hdmaplkr	$$⊢\phi \to \mathrm{LKer}\left(U\right)\left(S\left(E\right)\right)=O\left(\left\{E\right\}\right)$$
21	12 20	eleqtrrd	$$⊢\phi \to C\in \mathrm{LKer}\left(U\right)\left(S\left(E\right)\right)$$
22	1 4 11	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
23		eqid	$$⊢\mathrm{LCDual}\left(K\right)\left(W\right)=\mathrm{LCDual}\left(K\right)\left(W\right)$$
24		eqid	$$⊢{\mathrm{Base}}_{\mathrm{LCDual}\left(K\right)\left(W\right)}={\mathrm{Base}}_{\mathrm{LCDual}\left(K\right)\left(W\right)}$$
25	1 4 5 23 24 10 11 19	hdmapcl	$$⊢\phi \to S\left(E\right)\in {\mathrm{Base}}_{\mathrm{LCDual}\left(K\right)\left(W\right)}$$
26	1 23 24 4 13 11 25	lcdvbaselfl	$$⊢\phi \to S\left(E\right)\in \mathrm{LFnl}\left(U\right)$$
27	19	snssd	$$⊢\phi \to \left\{E\right\}\subseteq V$$
28	1 4 5 3	dochssv	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left\{E\right\}\subseteq V\right)\to O\left(\left\{E\right\}\right)\subseteq V$$
29	11 27 28	syl2anc	$$⊢\phi \to O\left(\left\{E\right\}\right)\subseteq V$$
30	29 12	sseldd	$$⊢\phi \to C\in V$$
31	5 6 9 13 14 22 26 30	ellkr2	$$⊢\phi \to \left(C\in \mathrm{LKer}\left(U\right)\left(S\left(E\right)\right)\leftrightarrow S\left(E\right)\left(C\right)=\underset{\dot{}}{0}\right)$$
32	21 31	mpbid	$$⊢\phi \to S\left(E\right)\left(C\right)=\underset{\dot{}}{0}$$