# 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}=\mathrm{LHyp}\left({K}\right)$
hdmaplkr.o ${⊢}{O}=\mathrm{ocH}\left({K}\right)\left({W}\right)$
hdmaplkr.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
hdmaplkr.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
hdmaplkr.f ${⊢}{F}=\mathrm{LFnl}\left({U}\right)$
hdmaplkr.y ${⊢}{Y}=\mathrm{LKer}\left({U}\right)$
hdmaplkr.s ${⊢}{S}=\mathrm{HDMap}\left({K}\right)\left({W}\right)$
hdmaplkr.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
hdmaplkr.x ${⊢}{\phi }\to {X}\in {V}$
Assertion hdmaplkr ${⊢}{\phi }\to {Y}\left({S}\left({X}\right)\right)={O}\left(\left\{{X}\right\}\right)$

### Proof

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