Theorem lcdlkreq2N

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

	Ref	Expression
Hypotheses	lcdlkreq2.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	lcdlkreq2.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	lcdlkreq2.s	$$⊢S=\mathrm{Scalar}\left(U\right)$$
	lcdlkreq2.r	$$⊢R={\mathrm{Base}}_S$$
	lcdlkreq2.o	$$⊢\underset{\dot{}}{0}=0_S$$
	lcdlkreq2.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
	lcdlkreq2.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	lcdlkreq2.v	$$⊢V={\mathrm{Base}}_C$$
	lcdlkreq2.t	$$⊢\underset{\dot{}}{·}={\cdot }_C$$
	lcdlkreq2.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	lcdlkreq2.a	$$⊢\phi \to A\in \left(R\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	lcdlkreq2.i	$$⊢\phi \to I\in V$$
	lcdlkreq2.g	$$⊢\phi \to G=A\underset{\dot{}}{·}I$$
Assertion	lcdlkreq2N	$$⊢\phi \to L\left(G\right)=L\left(I\right)$$

Proof

Step	Hyp	Ref	Expression
1		lcdlkreq2.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		lcdlkreq2.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		lcdlkreq2.s	$$⊢S=\mathrm{Scalar}\left(U\right)$$
4		lcdlkreq2.r	$$⊢R={\mathrm{Base}}_S$$
5		lcdlkreq2.o	$$⊢\underset{\dot{}}{0}=0_S$$
6		lcdlkreq2.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
7		lcdlkreq2.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
8		lcdlkreq2.v	$$⊢V={\mathrm{Base}}_C$$
9		lcdlkreq2.t	$$⊢\underset{\dot{}}{·}={\cdot }_C$$
10		lcdlkreq2.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
11		lcdlkreq2.a	$$⊢\phi \to A\in \left(R\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
12		lcdlkreq2.i	$$⊢\phi \to I\in V$$
13		lcdlkreq2.g	$$⊢\phi \to G=A\underset{\dot{}}{·}I$$
14		eqid	$$⊢\mathrm{LFnl}\left(U\right)=\mathrm{LFnl}\left(U\right)$$
15		eqid	$$⊢\mathrm{LDual}\left(U\right)=\mathrm{LDual}\left(U\right)$$
16		eqid	$$⊢{\cdot }_{\mathrm{LDual}\left(U\right)}={\cdot }_{\mathrm{LDual}\left(U\right)}$$
17	1 2 10	dvhlvec	$$⊢\phi \to U\in \mathrm{LVec}$$
18	1 7 8 2 14 10 12	lcdvbaselfl	$$⊢\phi \to I\in \mathrm{LFnl}\left(U\right)$$
19	1 2 15 16 7 9 10	lcdvs	$$⊢\phi \to \underset{\dot{}}{·}={\cdot }_{\mathrm{LDual}\left(U\right)}$$
20	19	oveqd	$$⊢\phi \to A\underset{\dot{}}{·}I=A{\cdot }_{\mathrm{LDual}\left(U\right)}I$$
21	13 20	eqtrd	$$⊢\phi \to G=A{\cdot }_{\mathrm{LDual}\left(U\right)}I$$
22	3 4 5 14 6 15 16 17 11 18 21	lkreqN	$$⊢\phi \to L\left(G\right)=L\left(I\right)$$