Metamath Proof Explorer


Theorem lkrlspeqN

Description: Condition for colinear functionals to have equal kernels. (Contributed by NM, 20-Mar-2015) (New usage is discouraged.)

Ref Expression
Hypotheses lkrlspeq.f F = LFnl W
lkrlspeq.l L = LKer W
lkrlspeq.d D = LDual W
lkrlspeq.o 0 ˙ = 0 D
lkrlspeq.j N = LSpan D
lkrlspeq.w φ W LVec
lkrlspeq.h φ H F
lkrlspeq.g φ G N H 0 ˙
Assertion lkrlspeqN φ L G = L H

Proof

Step Hyp Ref Expression
1 lkrlspeq.f F = LFnl W
2 lkrlspeq.l L = LKer W
3 lkrlspeq.d D = LDual W
4 lkrlspeq.o 0 ˙ = 0 D
5 lkrlspeq.j N = LSpan D
6 lkrlspeq.w φ W LVec
7 lkrlspeq.h φ H F
8 lkrlspeq.g φ G N H 0 ˙
9 8 eldifad φ G N H
10 lveclmod W LVec W LMod
11 6 10 syl φ W LMod
12 3 11 lduallmod φ D LMod
13 eqid Base D = Base D
14 1 3 13 6 7 ldualelvbase φ H Base D
15 eqid Scalar D = Scalar D
16 eqid Base Scalar D = Base Scalar D
17 eqid D = D
18 15 16 13 17 5 ellspsn D LMod H Base D G N H k Base Scalar D G = k D H
19 12 14 18 syl2anc φ G N H k Base Scalar D G = k D H
20 9 19 mpbid φ k Base Scalar D G = k D H
21 eqid Scalar W = Scalar W
22 eqid Base Scalar W = Base Scalar W
23 21 22 3 15 16 6 ldualsbase φ Base Scalar D = Base Scalar W
24 20 23 rexeqtrdv φ k Base Scalar W G = k D H
25 eqid 0 Scalar W = 0 Scalar W
26 6 3ad2ant1 φ k Base Scalar W G = k D H W LVec
27 simp2 φ k Base Scalar W G = k D H k Base Scalar W
28 simp3 φ k Base Scalar W G = k D H G = k D H
29 eldifsni G N H 0 ˙ G 0 ˙
30 8 29 syl φ G 0 ˙
31 30 3ad2ant1 φ k Base Scalar W G = k D H G 0 ˙
32 28 31 eqnetrrd φ k Base Scalar W G = k D H k D H 0 ˙
33 eqid 0 Scalar D = 0 Scalar D
34 21 25 3 15 33 11 ldual0 φ 0 Scalar D = 0 Scalar W
35 34 3ad2ant1 φ k Base Scalar W G = k D H 0 Scalar D = 0 Scalar W
36 35 eqeq2d φ k Base Scalar W G = k D H k = 0 Scalar D k = 0 Scalar W
37 orc k = 0 Scalar D k = 0 Scalar D H = 0 ˙
38 36 37 biimtrrdi φ k Base Scalar W G = k D H k = 0 Scalar W k = 0 Scalar D H = 0 ˙
39 3 6 lduallvec φ D LVec
40 39 3ad2ant1 φ k Base Scalar W G = k D H D LVec
41 23 3ad2ant1 φ k Base Scalar W G = k D H Base Scalar D = Base Scalar W
42 27 41 eleqtrrd φ k Base Scalar W G = k D H k Base Scalar D
43 14 3ad2ant1 φ k Base Scalar W G = k D H H Base D
44 13 17 15 16 33 4 40 42 43 lvecvs0or φ k Base Scalar W G = k D H k D H = 0 ˙ k = 0 Scalar D H = 0 ˙
45 38 44 sylibrd φ k Base Scalar W G = k D H k = 0 Scalar W k D H = 0 ˙
46 45 necon3d φ k Base Scalar W G = k D H k D H 0 ˙ k 0 Scalar W
47 32 46 mpd φ k Base Scalar W G = k D H k 0 Scalar W
48 eldifsn k Base Scalar W 0 Scalar W k Base Scalar W k 0 Scalar W
49 27 47 48 sylanbrc φ k Base Scalar W G = k D H k Base Scalar W 0 Scalar W
50 7 3ad2ant1 φ k Base Scalar W G = k D H H F
51 21 22 25 1 2 3 17 26 49 50 28 lkreqN φ k Base Scalar W G = k D H L G = L H
52 51 rexlimdv3a φ k Base Scalar W G = k D H L G = L H
53 24 52 mpd φ L G = L H