# Metamath Proof Explorer

## Theorem hdmaplkr

Description: Kernel of the vector to dual map. Line 16 in Holland95 p. 14. TODO: eliminate F hypothesis. (Contributed by NM, 9-Jun-2015)

Ref Expression
Hypotheses hdmaplkr.h $⊢ H = LHyp ⁡ K$
hdmaplkr.o $⊢ O = ocH ⁡ K ⁡ W$
hdmaplkr.u $⊢ U = DVecH ⁡ K ⁡ W$
hdmaplkr.v $⊢ V = Base U$
hdmaplkr.f $⊢ F = LFnl ⁡ U$
hdmaplkr.y $⊢ Y = LKer ⁡ U$
hdmaplkr.s $⊢ S = HDMap ⁡ K ⁡ W$
hdmaplkr.k $⊢ φ → K ∈ HL ∧ W ∈ H$
hdmaplkr.x $⊢ φ → X ∈ V$
Assertion hdmaplkr $⊢ φ → Y ⁡ S ⁡ X = O ⁡ X$

### Proof

Step Hyp Ref Expression
1 hdmaplkr.h $⊢ H = LHyp ⁡ K$
2 hdmaplkr.o $⊢ O = ocH ⁡ K ⁡ W$
3 hdmaplkr.u $⊢ U = DVecH ⁡ K ⁡ W$
4 hdmaplkr.v $⊢ V = Base U$
5 hdmaplkr.f $⊢ F = LFnl ⁡ U$
6 hdmaplkr.y $⊢ Y = LKer ⁡ U$
7 hdmaplkr.s $⊢ S = HDMap ⁡ K ⁡ W$
8 hdmaplkr.k $⊢ φ → K ∈ HL ∧ W ∈ H$
9 hdmaplkr.x $⊢ φ → X ∈ V$
10 fveq2 $⊢ X = 0 U → S ⁡ X = S ⁡ 0 U$
11 10 fveq2d $⊢ X = 0 U → Y ⁡ S ⁡ X = Y ⁡ S ⁡ 0 U$
12 sneq $⊢ X = 0 U → X = 0 U$
13 12 fveq2d $⊢ X = 0 U → O ⁡ X = O ⁡ 0 U$
14 11 13 sseq12d $⊢ X = 0 U → Y ⁡ S ⁡ X ⊆ O ⁡ X ↔ Y ⁡ S ⁡ 0 U ⊆ O ⁡ 0 U$
15 eqid $⊢ LCDual ⁡ K ⁡ W = LCDual ⁡ K ⁡ W$
16 1 15 8 lcdlmod $⊢ φ → LCDual ⁡ K ⁡ W ∈ LMod$
17 eqid $⊢ Base LCDual ⁡ K ⁡ W = Base LCDual ⁡ K ⁡ W$
18 1 3 4 15 17 7 8 9 hdmapcl $⊢ φ → S ⁡ X ∈ Base LCDual ⁡ K ⁡ W$
19 eqid $⊢ LSpan ⁡ LCDual ⁡ K ⁡ W = LSpan ⁡ LCDual ⁡ K ⁡ W$
20 17 19 lspsnid $⊢ LCDual ⁡ K ⁡ W ∈ LMod ∧ S ⁡ X ∈ Base LCDual ⁡ K ⁡ W → S ⁡ X ∈ LSpan ⁡ LCDual ⁡ K ⁡ W ⁡ S ⁡ X$
21 16 18 20 syl2anc $⊢ φ → S ⁡ X ∈ LSpan ⁡ LCDual ⁡ K ⁡ W ⁡ S ⁡ X$
22 eqid $⊢ LSpan ⁡ U = LSpan ⁡ U$
23 eqid $⊢ mapd ⁡ K ⁡ W = mapd ⁡ K ⁡ W$
24 1 3 4 22 15 19 23 7 8 9 hdmap10 $⊢ φ → mapd ⁡ K ⁡ W ⁡ LSpan ⁡ U ⁡ X = LSpan ⁡ LCDual ⁡ K ⁡ W ⁡ S ⁡ X$
25 eqid $⊢ LFnl ⁡ U = LFnl ⁡ U$
26 1 2 23 3 4 22 25 6 8 9 mapdsn $⊢ φ → mapd ⁡ K ⁡ W ⁡ LSpan ⁡ U ⁡ X = f ∈ LFnl ⁡ U | O ⁡ X ⊆ Y ⁡ f$
27 24 26 eqtr3d $⊢ φ → LSpan ⁡ LCDual ⁡ K ⁡ W ⁡ S ⁡ X = f ∈ LFnl ⁡ U | O ⁡ X ⊆ Y ⁡ f$
28 21 27 eleqtrd $⊢ φ → S ⁡ X ∈ f ∈ LFnl ⁡ U | O ⁡ X ⊆ Y ⁡ f$
29 1 15 17 3 25 8 18 lcdvbaselfl $⊢ φ → S ⁡ X ∈ LFnl ⁡ U$
30 fveq2 $⊢ f = S ⁡ X → Y ⁡ f = Y ⁡ S ⁡ X$
31 30 sseq2d $⊢ f = S ⁡ X → O ⁡ X ⊆ Y ⁡ f ↔ O ⁡ X ⊆ Y ⁡ S ⁡ X$
32 31 elrab3 $⊢ S ⁡ X ∈ LFnl ⁡ U → S ⁡ X ∈ f ∈ LFnl ⁡ U | O ⁡ X ⊆ Y ⁡ f ↔ O ⁡ X ⊆ Y ⁡ S ⁡ X$
33 29 32 syl $⊢ φ → S ⁡ X ∈ f ∈ LFnl ⁡ U | O ⁡ X ⊆ Y ⁡ f ↔ O ⁡ X ⊆ Y ⁡ S ⁡ X$
34 28 33 mpbid $⊢ φ → O ⁡ X ⊆ Y ⁡ S ⁡ X$
35 34 adantr $⊢ φ ∧ X ≠ 0 U → O ⁡ X ⊆ Y ⁡ S ⁡ X$
36 eqid $⊢ LSHyp ⁡ U = LSHyp ⁡ U$
37 1 3 8 dvhlvec $⊢ φ → U ∈ LVec$
38 37 adantr $⊢ φ ∧ X ≠ 0 U → U ∈ LVec$
39 eqid $⊢ 0 U = 0 U$
40 8 adantr $⊢ φ ∧ X ≠ 0 U → K ∈ HL ∧ W ∈ H$
41 9 anim1i $⊢ φ ∧ X ≠ 0 U → X ∈ V ∧ X ≠ 0 U$
42 eldifsn $⊢ X ∈ V ∖ 0 U ↔ X ∈ V ∧ X ≠ 0 U$
43 41 42 sylibr $⊢ φ ∧ X ≠ 0 U → X ∈ V ∖ 0 U$
44 1 2 3 4 39 36 40 43 dochsnshp $⊢ φ ∧ X ≠ 0 U → O ⁡ X ∈ LSHyp ⁡ U$
45 29 adantr $⊢ φ ∧ X ≠ 0 U → S ⁡ X ∈ LFnl ⁡ U$
46 eqid $⊢ Scalar ⁡ U = Scalar ⁡ U$
47 eqid $⊢ 0 Scalar ⁡ U = 0 Scalar ⁡ U$
48 eqid $⊢ 0 LCDual ⁡ K ⁡ W = 0 LCDual ⁡ K ⁡ W$
49 1 3 4 46 47 15 48 8 lcd0v $⊢ φ → 0 LCDual ⁡ K ⁡ W = V × 0 Scalar ⁡ U$
50 49 eqeq2d $⊢ φ → S ⁡ X = 0 LCDual ⁡ K ⁡ W ↔ S ⁡ X = V × 0 Scalar ⁡ U$
51 1 3 4 39 15 48 7 8 9 hdmapeq0 $⊢ φ → S ⁡ X = 0 LCDual ⁡ K ⁡ W ↔ X = 0 U$
52 50 51 bitr3d $⊢ φ → S ⁡ X = V × 0 Scalar ⁡ U ↔ X = 0 U$
53 52 necon3bid $⊢ φ → S ⁡ X ≠ V × 0 Scalar ⁡ U ↔ X ≠ 0 U$
54 53 biimpar $⊢ φ ∧ X ≠ 0 U → S ⁡ X ≠ V × 0 Scalar ⁡ U$
55 4 46 47 36 25 6 lkrshp $⊢ U ∈ LVec ∧ S ⁡ X ∈ LFnl ⁡ U ∧ S ⁡ X ≠ V × 0 Scalar ⁡ U → Y ⁡ S ⁡ X ∈ LSHyp ⁡ U$
56 38 45 54 55 syl3anc $⊢ φ ∧ X ≠ 0 U → Y ⁡ S ⁡ X ∈ LSHyp ⁡ U$
57 36 38 44 56 lshpcmp $⊢ φ ∧ X ≠ 0 U → O ⁡ X ⊆ Y ⁡ S ⁡ X ↔ O ⁡ X = Y ⁡ S ⁡ X$
58 35 57 mpbid $⊢ φ ∧ X ≠ 0 U → O ⁡ X = Y ⁡ S ⁡ X$
59 eqimss2 $⊢ O ⁡ X = Y ⁡ S ⁡ X → Y ⁡ S ⁡ X ⊆ O ⁡ X$
60 58 59 syl $⊢ φ ∧ X ≠ 0 U → Y ⁡ S ⁡ X ⊆ O ⁡ X$
61 1 3 8 dvhlmod $⊢ φ → U ∈ LMod$
62 4 39 lmod0vcl $⊢ U ∈ LMod → 0 U ∈ V$
63 61 62 syl $⊢ φ → 0 U ∈ V$
64 1 3 4 15 17 7 8 63 hdmapcl $⊢ φ → S ⁡ 0 U ∈ Base LCDual ⁡ K ⁡ W$
65 1 15 17 3 25 8 64 lcdvbaselfl $⊢ φ → S ⁡ 0 U ∈ LFnl ⁡ U$
66 4 25 6 61 65 lkrssv $⊢ φ → Y ⁡ S ⁡ 0 U ⊆ V$
67 1 3 2 4 39 doch0 $⊢ K ∈ HL ∧ W ∈ H → O ⁡ 0 U = V$
68 8 67 syl $⊢ φ → O ⁡ 0 U = V$
69 66 68 sseqtrrd $⊢ φ → Y ⁡ S ⁡ 0 U ⊆ O ⁡ 0 U$
70 14 60 69 pm2.61ne $⊢ φ → Y ⁡ S ⁡ X ⊆ O ⁡ X$
71 70 34 eqssd $⊢ φ → Y ⁡ S ⁡ X = O ⁡ X$