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 lspsnel ⊢ 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 23 rexeqdv ⊢ φ → ∃ k ∈ Base Scalar ⁡ D G = k ⋅ D H ↔ ∃ k ∈ Base Scalar ⁡ W G = k ⋅ D H
25 20 24 mpbid ⊢ φ → ∃ k ∈ Base Scalar ⁡ W G = k ⋅ D H
26 eqid ⊢ 0 Scalar ⁡ W = 0 Scalar ⁡ W
27 6 3ad2ant1 ⊢ φ ∧ k ∈ Base Scalar ⁡ W ∧ G = k ⋅ D H → W ∈ LVec
28 simp2 ⊢ φ ∧ k ∈ Base Scalar ⁡ W ∧ G = k ⋅ D H → k ∈ Base Scalar ⁡ W
29 simp3 ⊢ φ ∧ k ∈ Base Scalar ⁡ W ∧ G = k ⋅ D H → G = k ⋅ D H
30 eldifsni ⊢ G ∈ N ⁡ H ∖ 0 ˙ → G ≠ 0 ˙
31 8 30 syl ⊢ φ → G ≠ 0 ˙
32 31 3ad2ant1 ⊢ φ ∧ k ∈ Base Scalar ⁡ W ∧ G = k ⋅ D H → G ≠ 0 ˙
33 29 32 eqnetrrd ⊢ φ ∧ k ∈ Base Scalar ⁡ W ∧ G = k ⋅ D H → k ⋅ D H ≠ 0 ˙
34 eqid ⊢ 0 Scalar ⁡ D = 0 Scalar ⁡ D
35 21 26 3 15 34 11 ldual0 ⊢ φ → 0 Scalar ⁡ D = 0 Scalar ⁡ W
36 35 3ad2ant1 ⊢ φ ∧ k ∈ Base Scalar ⁡ W ∧ G = k ⋅ D H → 0 Scalar ⁡ D = 0 Scalar ⁡ W
37 36 eqeq2d ⊢ φ ∧ k ∈ Base Scalar ⁡ W ∧ G = k ⋅ D H → k = 0 Scalar ⁡ D ↔ k = 0 Scalar ⁡ W
38 orc ⊢ k = 0 Scalar ⁡ D → k = 0 Scalar ⁡ D ∨ H = 0 ˙
39 37 38 syl6bir ⊢ φ ∧ k ∈ Base Scalar ⁡ W ∧ G = k ⋅ D H → k = 0 Scalar ⁡ W → k = 0 Scalar ⁡ D ∨ H = 0 ˙
40 3 6 lduallvec ⊢ φ → D ∈ LVec
41 40 3ad2ant1 ⊢ φ ∧ k ∈ Base Scalar ⁡ W ∧ G = k ⋅ D H → D ∈ LVec
42 23 3ad2ant1 ⊢ φ ∧ k ∈ Base Scalar ⁡ W ∧ G = k ⋅ D H → Base Scalar ⁡ D = Base Scalar ⁡ W
43 28 42 eleqtrrd ⊢ φ ∧ k ∈ Base Scalar ⁡ W ∧ G = k ⋅ D H → k ∈ Base Scalar ⁡ D
44 14 3ad2ant1 ⊢ φ ∧ k ∈ Base Scalar ⁡ W ∧ G = k ⋅ D H → H ∈ Base D
45 13 17 15 16 34 4 41 43 44 lvecvs0or ⊢ φ ∧ k ∈ Base Scalar ⁡ W ∧ G = k ⋅ D H → k ⋅ D H = 0 ˙ ↔ k = 0 Scalar ⁡ D ∨ H = 0 ˙
46 39 45 sylibrd ⊢ φ ∧ k ∈ Base Scalar ⁡ W ∧ G = k ⋅ D H → k = 0 Scalar ⁡ W → k ⋅ D H = 0 ˙
47 46 necon3d ⊢ φ ∧ k ∈ Base Scalar ⁡ W ∧ G = k ⋅ D H → k ⋅ D H ≠ 0 ˙ → k ≠ 0 Scalar ⁡ W
48 33 47 mpd ⊢ φ ∧ k ∈ Base Scalar ⁡ W ∧ G = k ⋅ D H → k ≠ 0 Scalar ⁡ W
49 eldifsn ⊢ k ∈ Base Scalar ⁡ W ∖ 0 Scalar ⁡ W ↔ k ∈ Base Scalar ⁡ W ∧ k ≠ 0 Scalar ⁡ W
50 28 48 49 sylanbrc ⊢ φ ∧ k ∈ Base Scalar ⁡ W ∧ G = k ⋅ D H → k ∈ Base Scalar ⁡ W ∖ 0 Scalar ⁡ W
51 7 3ad2ant1 ⊢ φ ∧ k ∈ Base Scalar ⁡ W ∧ G = k ⋅ D H → H ∈ F
52 21 22 26 1 2 3 17 27 50 51 29 lkreqN ⊢ φ ∧ k ∈ Base Scalar ⁡ W ∧ G = k ⋅ D H → L ⁡ G = L ⁡ H
53 52 rexlimdv3a ⊢ φ → ∃ k ∈ Base Scalar ⁡ W G = k ⋅ D H → L ⁡ G = L ⁡ H
54 25 53 mpd ⊢ φ → L ⁡ G = L ⁡ H