Theorem lcdlkreq2N

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

	Ref	Expression
Hypotheses	lcdlkreq2.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	lcdlkreq2.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	lcdlkreq2.s	⊢ 𝑆 = ( Scalar ‘ 𝑈 )
	lcdlkreq2.r	⊢ 𝑅 = ( Base ‘ 𝑆 )
	lcdlkreq2.o	⊢ 0 = ( 0g ‘ 𝑆 )
	lcdlkreq2.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
	lcdlkreq2.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
	lcdlkreq2.v	⊢ 𝑉 = ( Base ‘ 𝐶 )
	lcdlkreq2.t	⊢ · = ( ·𝑠 ‘ 𝐶 )
	lcdlkreq2.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	lcdlkreq2.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝑅 ∖ { 0 } ) )
	lcdlkreq2.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	lcdlkreq2.g	⊢ ( 𝜑 → 𝐺 = ( 𝐴 · 𝐼 ) )
Assertion	lcdlkreq2N	⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝐼 ) )

Proof

Step	Hyp	Ref	Expression
1		lcdlkreq2.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		lcdlkreq2.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3		lcdlkreq2.s	⊢ 𝑆 = ( Scalar ‘ 𝑈 )
4		lcdlkreq2.r	⊢ 𝑅 = ( Base ‘ 𝑆 )
5		lcdlkreq2.o	⊢ 0 = ( 0g ‘ 𝑆 )
6		lcdlkreq2.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
7		lcdlkreq2.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
8		lcdlkreq2.v	⊢ 𝑉 = ( Base ‘ 𝐶 )
9		lcdlkreq2.t	⊢ · = ( ·𝑠 ‘ 𝐶 )
10		lcdlkreq2.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
11		lcdlkreq2.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝑅 ∖ { 0 } ) )
12		lcdlkreq2.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
13		lcdlkreq2.g	⊢ ( 𝜑 → 𝐺 = ( 𝐴 · 𝐼 ) )
14		eqid	⊢ ( LFnl ‘ 𝑈 ) = ( LFnl ‘ 𝑈 )
15		eqid	⊢ ( LDual ‘ 𝑈 ) = ( LDual ‘ 𝑈 )
16		eqid	⊢ ( ·𝑠 ‘ ( LDual ‘ 𝑈 ) ) = ( ·𝑠 ‘ ( LDual ‘ 𝑈 ) )
17	1 2 10	dvhlvec	⊢ ( 𝜑 → 𝑈 ∈ LVec )
18	1 7 8 2 14 10 12	lcdvbaselfl	⊢ ( 𝜑 → 𝐼 ∈ ( LFnl ‘ 𝑈 ) )
19	1 2 15 16 7 9 10	lcdvs	⊢ ( 𝜑 → · = ( ·𝑠 ‘ ( LDual ‘ 𝑈 ) ) )
20	19	oveqd	⊢ ( 𝜑 → ( 𝐴 · 𝐼 ) = ( 𝐴 ( ·𝑠 ‘ ( LDual ‘ 𝑈 ) ) 𝐼 ) )
21	13 20	eqtrd	⊢ ( 𝜑 → 𝐺 = ( 𝐴 ( ·𝑠 ‘ ( LDual ‘ 𝑈 ) ) 𝐼 ) )
22	3 4 5 14 6 15 16 17 11 18 21	lkreqN	⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝐼 ) )