Metamath Proof Explorer


Theorem lcdlkreqN

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

Ref Expression
Hypotheses lcdlkreq.h H = LHyp K
lcdlkreq.u U = DVecH K W
lcdlkreq.l L = LKer U
lcdlkreq.c C = LCDual K W
lcdlkreq.o 0 ˙ = 0 C
lcdlkreq.n N = LSpan C
lcdlkreq.v V = Base C
lcdlkreq.k φ K HL W H
lcdlkreq.i φ I V
lcdlkreq.g φ G N I
lcdlkreq.z φ G 0 ˙
Assertion lcdlkreqN φ L G = L I

Proof

Step Hyp Ref Expression
1 lcdlkreq.h H = LHyp K
2 lcdlkreq.u U = DVecH K W
3 lcdlkreq.l L = LKer U
4 lcdlkreq.c C = LCDual K W
5 lcdlkreq.o 0 ˙ = 0 C
6 lcdlkreq.n N = LSpan C
7 lcdlkreq.v V = Base C
8 lcdlkreq.k φ K HL W H
9 lcdlkreq.i φ I V
10 lcdlkreq.g φ G N I
11 lcdlkreq.z φ G 0 ˙
12 eqid LFnl U = LFnl U
13 eqid LDual U = LDual U
14 eqid 0 LDual U = 0 LDual U
15 eqid LSpan LDual U = LSpan LDual U
16 1 2 8 dvhlvec φ U LVec
17 1 4 7 2 12 8 9 lcdvbaselfl φ I LFnl U
18 9 snssd φ I V
19 1 2 13 15 4 7 6 8 18 lcdlsp φ N I = LSpan LDual U I
20 10 19 eleqtrd φ G LSpan LDual U I
21 1 2 13 14 4 5 8 lcd0v2 φ 0 ˙ = 0 LDual U
22 11 21 neeqtrd φ G 0 LDual U
23 eldifsn G LSpan LDual U I 0 LDual U G LSpan LDual U I G 0 LDual U
24 20 22 23 sylanbrc φ G LSpan LDual U I 0 LDual U
25 12 3 13 14 15 16 17 24 lkrlspeqN φ L G = L I