Theorem lcdlkreqN

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

	Ref	Expression
Hypotheses	lcdlkreq.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	lcdlkreq.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	lcdlkreq.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
	lcdlkreq.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
	lcdlkreq.o	⊢ 0 = ( 0g ‘ 𝐶 )
	lcdlkreq.n	⊢ 𝑁 = ( LSpan ‘ 𝐶 )
	lcdlkreq.v	⊢ 𝑉 = ( Base ‘ 𝐶 )
	lcdlkreq.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	lcdlkreq.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	lcdlkreq.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑁 ‘ { 𝐼 } ) )
	lcdlkreq.z	⊢ ( 𝜑 → 𝐺 ≠ 0 )
Assertion	lcdlkreqN	⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝐼 ) )

Proof

Step	Hyp	Ref	Expression
1		lcdlkreq.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		lcdlkreq.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3		lcdlkreq.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
4		lcdlkreq.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
5		lcdlkreq.o	⊢ 0 = ( 0g ‘ 𝐶 )
6		lcdlkreq.n	⊢ 𝑁 = ( LSpan ‘ 𝐶 )
7		lcdlkreq.v	⊢ 𝑉 = ( Base ‘ 𝐶 )
8		lcdlkreq.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9		lcdlkreq.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
10		lcdlkreq.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑁 ‘ { 𝐼 } ) )
11		lcdlkreq.z	⊢ ( 𝜑 → 𝐺 ≠ 0 )
12		eqid	⊢ ( LFnl ‘ 𝑈 ) = ( LFnl ‘ 𝑈 )
13		eqid	⊢ ( LDual ‘ 𝑈 ) = ( LDual ‘ 𝑈 )
14		eqid	⊢ ( 0g ‘ ( LDual ‘ 𝑈 ) ) = ( 0g ‘ ( LDual ‘ 𝑈 ) )
15		eqid	⊢ ( LSpan ‘ ( LDual ‘ 𝑈 ) ) = ( LSpan ‘ ( LDual ‘ 𝑈 ) )
16	1 2 8	dvhlvec	⊢ ( 𝜑 → 𝑈 ∈ LVec )
17	1 4 7 2 12 8 9	lcdvbaselfl	⊢ ( 𝜑 → 𝐼 ∈ ( LFnl ‘ 𝑈 ) )
18	9	snssd	⊢ ( 𝜑 → { 𝐼 } ⊆ 𝑉 )
19	1 2 13 15 4 7 6 8 18	lcdlsp	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝐼 } ) = ( ( LSpan ‘ ( LDual ‘ 𝑈 ) ) ‘ { 𝐼 } ) )
20	10 19	eleqtrd	⊢ ( 𝜑 → 𝐺 ∈ ( ( LSpan ‘ ( LDual ‘ 𝑈 ) ) ‘ { 𝐼 } ) )
21	1 2 13 14 4 5 8	lcd0v2	⊢ ( 𝜑 → 0 = ( 0g ‘ ( LDual ‘ 𝑈 ) ) )
22	11 21	neeqtrd	⊢ ( 𝜑 → 𝐺 ≠ ( 0g ‘ ( LDual ‘ 𝑈 ) ) )
23		eldifsn	⊢ ( 𝐺 ∈ ( ( ( LSpan ‘ ( LDual ‘ 𝑈 ) ) ‘ { 𝐼 } ) ∖ { ( 0g ‘ ( LDual ‘ 𝑈 ) ) } ) ↔ ( 𝐺 ∈ ( ( LSpan ‘ ( LDual ‘ 𝑈 ) ) ‘ { 𝐼 } ) ∧ 𝐺 ≠ ( 0g ‘ ( LDual ‘ 𝑈 ) ) ) )
24	20 22 23	sylanbrc	⊢ ( 𝜑 → 𝐺 ∈ ( ( ( LSpan ‘ ( LDual ‘ 𝑈 ) ) ‘ { 𝐼 } ) ∖ { ( 0g ‘ ( LDual ‘ 𝑈 ) ) } ) )
25	12 3 13 14 15 16 17 24	lkrlspeqN	⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝐼 ) )