Theorem lcdlkreq2N

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

	Ref	Expression
Hypotheses	lcdlkreq2.h	|- H = ( LHyp ` K )
	lcdlkreq2.u	|- U = ( ( DVecH ` K ) ` W )
	lcdlkreq2.s	|- S = ( Scalar ` U )
	lcdlkreq2.r	|- R = ( Base ` S )
	lcdlkreq2.o	|- .0. = ( 0g ` S )
	lcdlkreq2.l	|- L = ( LKer ` U )
	lcdlkreq2.c	|- C = ( ( LCDual ` K ) ` W )
	lcdlkreq2.v	|- V = ( Base ` C )
	lcdlkreq2.t	|- .x. = ( .s ` C )
	lcdlkreq2.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	lcdlkreq2.a	|- ( ph -> A e. ( R \ { .0. } ) )
	lcdlkreq2.i	|- ( ph -> I e. V )
	lcdlkreq2.g	|- ( ph -> G = ( A .x. I ) )
Assertion	lcdlkreq2N	|- ( ph -> ( L ` G ) = ( L ` I ) )

Proof

Step	Hyp	Ref	Expression
1		lcdlkreq2.h	|- H = ( LHyp ` K )
2		lcdlkreq2.u	|- U = ( ( DVecH ` K ) ` W )
3		lcdlkreq2.s	|- S = ( Scalar ` U )
4		lcdlkreq2.r	|- R = ( Base ` S )
5		lcdlkreq2.o	|- .0. = ( 0g ` S )
6		lcdlkreq2.l	|- L = ( LKer ` U )
7		lcdlkreq2.c	|- C = ( ( LCDual ` K ) ` W )
8		lcdlkreq2.v	|- V = ( Base ` C )
9		lcdlkreq2.t	|- .x. = ( .s ` C )
10		lcdlkreq2.k	|- ( ph -> ( K e. HL /\ W e. H ) )
11		lcdlkreq2.a	|- ( ph -> A e. ( R \ { .0. } ) )
12		lcdlkreq2.i	|- ( ph -> I e. V )
13		lcdlkreq2.g	|- ( ph -> G = ( A .x. I ) )
14		eqid	|- ( LFnl ` U ) = ( LFnl ` U )
15		eqid	|- ( LDual ` U ) = ( LDual ` U )
16		eqid	|- ( .s ` ( LDual ` U ) ) = ( .s ` ( LDual ` U ) )
17	1 2 10	dvhlvec	|- ( ph -> U e. LVec )
18	1 7 8 2 14 10 12	lcdvbaselfl	|- ( ph -> I e. ( LFnl ` U ) )
19	1 2 15 16 7 9 10	lcdvs	|- ( ph -> .x. = ( .s ` ( LDual ` U ) ) )
20	19	oveqd	|- ( ph -> ( A .x. I ) = ( A ( .s ` ( LDual ` U ) ) I ) )
21	13 20	eqtrd	|- ( ph -> G = ( A ( .s ` ( LDual ` U ) ) I ) )
22	3 4 5 14 6 15 16 17 11 18 21	lkreqN	|- ( ph -> ( L ` G ) = ( L ` I ) )