Metamath Proof Explorer


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 ˙ = 0 S
lcdlkreq2.l L = LKer U
lcdlkreq2.c C = LCDual K W
lcdlkreq2.v V = Base C
lcdlkreq2.t · ˙ = C
lcdlkreq2.k φ K HL W H
lcdlkreq2.a φ A R 0 ˙
lcdlkreq2.i φ I V
lcdlkreq2.g φ G = A · ˙ I
Assertion lcdlkreq2N φ 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 ˙ = 0 S
6 lcdlkreq2.l L = LKer U
7 lcdlkreq2.c C = LCDual K W
8 lcdlkreq2.v V = Base C
9 lcdlkreq2.t · ˙ = C
10 lcdlkreq2.k φ K HL W H
11 lcdlkreq2.a φ A R 0 ˙
12 lcdlkreq2.i φ I V
13 lcdlkreq2.g φ G = A · ˙ I
14 eqid LFnl U = LFnl U
15 eqid LDual U = LDual U
16 eqid LDual U = LDual U
17 1 2 10 dvhlvec φ U LVec
18 1 7 8 2 14 10 12 lcdvbaselfl φ I LFnl U
19 1 2 15 16 7 9 10 lcdvs φ · ˙ = LDual U
20 19 oveqd φ A · ˙ I = A LDual U I
21 13 20 eqtrd φ G = A LDual U I
22 3 4 5 14 6 15 16 17 11 18 21 lkreqN φ L G = L I