Metamath Proof Explorer

Theorem dochsnkr

Description: A (closed) kernel expressed in terms of a nonzero vector in its orthocomplement. TODO: consolidate lemmas unless they're needed for something else (in which case break out as theorems). (Contributed by NM, 2-Jan-2015)

Ref Expression
Hypotheses dochsnkr.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
dochsnkr.o
dochsnkr.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
dochsnkr.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
dochsnkr.z
dochsnkr.f ${⊢}{F}=\mathrm{LFnl}\left({U}\right)$
dochsnkr.l ${⊢}{L}=\mathrm{LKer}\left({U}\right)$
dochsnkr.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
dochsnkr.g ${⊢}{\phi }\to {G}\in {F}$
dochsnkr.x
Assertion dochsnkr

Proof

Step Hyp Ref Expression
1 dochsnkr.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 dochsnkr.o
3 dochsnkr.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
4 dochsnkr.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
5 dochsnkr.z
6 dochsnkr.f ${⊢}{F}=\mathrm{LFnl}\left({U}\right)$
7 dochsnkr.l ${⊢}{L}=\mathrm{LKer}\left({U}\right)$
8 dochsnkr.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
9 dochsnkr.g ${⊢}{\phi }\to {G}\in {F}$
10 dochsnkr.x
11 eqid ${⊢}\mathrm{LSpan}\left({U}\right)=\mathrm{LSpan}\left({U}\right)$
12 eqid ${⊢}\mathrm{LSAtoms}\left({U}\right)=\mathrm{LSAtoms}\left({U}\right)$
13 1 3 8 dvhlvec ${⊢}{\phi }\to {U}\in \mathrm{LVec}$
14 1 2 3 4 5 6 7 8 9 10 12 dochsnkrlem2
16 eldifsni
17 10 16 syl
18 5 11 12 13 14 15 17 lsatel
19 18 fveq2d
20 1 2 3 4 5 6 7 8 9 10 dochsnkrlem3
21 1 3 8 dvhlmod ${⊢}{\phi }\to {U}\in \mathrm{LMod}$
22 4 6 7 21 9 lkrssv ${⊢}{\phi }\to {L}\left({G}\right)\subseteq {V}$
23 1 3 4 2 dochssv
24 8 22 23 syl2anc
25 24 ssdifssd
26 25 10 sseldd ${⊢}{\phi }\to {X}\in {V}$
27 26 snssd ${⊢}{\phi }\to \left\{{X}\right\}\subseteq {V}$
28 1 3 2 4 11 8 27 dochocsp
29 19 20 28 3eqtr3d