Theorem hdmapellkr

Description: Membership in the kernel (as shown by hdmaplkr ) of the vector to dual map. Line 17 in Holland95 p. 14. (Contributed by NM, 16-Jun-2015)

	Ref	Expression
Hypotheses	hdmapellkr.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hdmapellkr.o	$$⊢O=\mathrm{ocH}\left(K\right)\left(W\right)$$
	hdmapellkr.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hdmapellkr.v	$$⊢V={\mathrm{Base}}_U$$
	hdmapellkr.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
	hdmapellkr.z	$$⊢\underset{\dot{}}{0}=0_R$$
	hdmapellkr.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
	hdmapellkr.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	hdmapellkr.x	$$⊢\phi \to X\in V$$
	hdmapellkr.y	$$⊢\phi \to Y\in V$$
Assertion	hdmapellkr	$$⊢\phi \to \left(S\left(X\right)\left(Y\right)=\underset{\dot{}}{0}\leftrightarrow Y\in O\left(\left\{X\right\}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		hdmapellkr.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hdmapellkr.o	$$⊢O=\mathrm{ocH}\left(K\right)\left(W\right)$$
3		hdmapellkr.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
4		hdmapellkr.v	$$⊢V={\mathrm{Base}}_U$$
5		hdmapellkr.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
6		hdmapellkr.z	$$⊢\underset{\dot{}}{0}=0_R$$
7		hdmapellkr.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
8		hdmapellkr.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
9		hdmapellkr.x	$$⊢\phi \to X\in V$$
10		hdmapellkr.y	$$⊢\phi \to Y\in V$$
11		eqid	$$⊢\mathrm{LFnl}\left(U\right)=\mathrm{LFnl}\left(U\right)$$
12		eqid	$$⊢\mathrm{LKer}\left(U\right)=\mathrm{LKer}\left(U\right)$$
13	1 3 8	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
14		eqid	$$⊢\mathrm{LCDual}\left(K\right)\left(W\right)=\mathrm{LCDual}\left(K\right)\left(W\right)$$
15		eqid	$$⊢{\mathrm{Base}}_{\mathrm{LCDual}\left(K\right)\left(W\right)}={\mathrm{Base}}_{\mathrm{LCDual}\left(K\right)\left(W\right)}$$
16	1 3 4 14 15 7 8 9	hdmapcl	$$⊢\phi \to S\left(X\right)\in {\mathrm{Base}}_{\mathrm{LCDual}\left(K\right)\left(W\right)}$$
17	1 14 15 3 11 8 16	lcdvbaselfl	$$⊢\phi \to S\left(X\right)\in \mathrm{LFnl}\left(U\right)$$
18	4 5 6 11 12 13 17 10	ellkr2	$$⊢\phi \to \left(Y\in \mathrm{LKer}\left(U\right)\left(S\left(X\right)\right)\leftrightarrow S\left(X\right)\left(Y\right)=\underset{\dot{}}{0}\right)$$
19	1 2 3 4 11 12 7 8 9	hdmaplkr	$$⊢\phi \to \mathrm{LKer}\left(U\right)\left(S\left(X\right)\right)=O\left(\left\{X\right\}\right)$$
20	19	eleq2d	$$⊢\phi \to \left(Y\in \mathrm{LKer}\left(U\right)\left(S\left(X\right)\right)\leftrightarrow Y\in O\left(\left\{X\right\}\right)\right)$$
21	18 20	bitr3d	$$⊢\phi \to \left(S\left(X\right)\left(Y\right)=\underset{\dot{}}{0}\leftrightarrow Y\in O\left(\left\{X\right\}\right)\right)$$