Theorem lcdlkreqN

Description: Colinear functionals have equal kernels. (Contributed by NM, 28-Mar-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	lcdlkreq.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	lcdlkreq.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	lcdlkreq.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
	lcdlkreq.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	lcdlkreq.o	$$⊢\underset{\dot{}}{0}=0_C$$
	lcdlkreq.n	$$⊢N=\mathrm{LSpan}\left(C\right)$$
	lcdlkreq.v	$$⊢V={\mathrm{Base}}_C$$
	lcdlkreq.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	lcdlkreq.i	$$⊢\phi \to I\in V$$
	lcdlkreq.g	$$⊢\phi \to G\in N\left(\left\{I\right\}\right)$$
	lcdlkreq.z	$$⊢\phi \to G\ne \underset{\dot{}}{0}$$
Assertion	lcdlkreqN	$$⊢\phi \to L\left(G\right)=L\left(I\right)$$

Proof

Step	Hyp	Ref	Expression
1		lcdlkreq.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		lcdlkreq.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		lcdlkreq.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
4		lcdlkreq.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
5		lcdlkreq.o	$$⊢\underset{\dot{}}{0}=0_C$$
6		lcdlkreq.n	$$⊢N=\mathrm{LSpan}\left(C\right)$$
7		lcdlkreq.v	$$⊢V={\mathrm{Base}}_C$$
8		lcdlkreq.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
9		lcdlkreq.i	$$⊢\phi \to I\in V$$
10		lcdlkreq.g	$$⊢\phi \to G\in N\left(\left\{I\right\}\right)$$
11		lcdlkreq.z	$$⊢\phi \to G\ne \underset{\dot{}}{0}$$
12		eqid	$$⊢\mathrm{LFnl}\left(U\right)=\mathrm{LFnl}\left(U\right)$$
13		eqid	$$⊢\mathrm{LDual}\left(U\right)=\mathrm{LDual}\left(U\right)$$
14		eqid	$$⊢0_{\mathrm{LDual}\left(U\right)}=0_{\mathrm{LDual}\left(U\right)}$$
15		eqid	$$⊢\mathrm{LSpan}\left(\mathrm{LDual}\left(U\right)\right)=\mathrm{LSpan}\left(\mathrm{LDual}\left(U\right)\right)$$
16	1 2 8	dvhlvec	$$⊢\phi \to U\in \mathrm{LVec}$$
17	1 4 7 2 12 8 9	lcdvbaselfl	$$⊢\phi \to I\in \mathrm{LFnl}\left(U\right)$$
18	9	snssd	$$⊢\phi \to \left\{I\right\}\subseteq V$$
19	1 2 13 15 4 7 6 8 18	lcdlsp	$$⊢\phi \to N\left(\left\{I\right\}\right)=\mathrm{LSpan}\left(\mathrm{LDual}\left(U\right)\right)\left(\left\{I\right\}\right)$$
20	10 19	eleqtrd	$$⊢\phi \to G\in \mathrm{LSpan}\left(\mathrm{LDual}\left(U\right)\right)\left(\left\{I\right\}\right)$$
21	1 2 13 14 4 5 8	lcd0v2	$$⊢\phi \to \underset{\dot{}}{0}=0_{\mathrm{LDual}\left(U\right)}$$
22	11 21	neeqtrd	$$⊢\phi \to G\ne 0_{\mathrm{LDual}\left(U\right)}$$
23		eldifsn	$$⊢G\in \left(\mathrm{LSpan}\left(\mathrm{LDual}\left(U\right)\right)\left(\left\{I\right\}\right)\setminus \left\{0_{\mathrm{LDual}\left(U\right)}\right\}\right)\leftrightarrow \left(G\in \mathrm{LSpan}\left(\mathrm{LDual}\left(U\right)\right)\left(\left\{I\right\}\right)\wedge G\ne 0_{\mathrm{LDual}\left(U\right)}\right)$$
24	20 22 23	sylanbrc	$$⊢\phi \to G\in \left(\mathrm{LSpan}\left(\mathrm{LDual}\left(U\right)\right)\left(\left\{I\right\}\right)\setminus \left\{0_{\mathrm{LDual}\left(U\right)}\right\}\right)$$
25	12 3 13 14 15 16 17 24	lkrlspeqN	$$⊢\phi \to L\left(G\right)=L\left(I\right)$$