# Metamath Proof Explorer

## Theorem dochkr1

Description: A nonzero functional has a value of 1 at some argument belonging to the orthocomplement of its kernel (when its kernel is a closed hyperplane). Tighter version of lfl1 . (Contributed by NM, 2-Jan-2015)

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

### Proof

Step Hyp Ref Expression
1 dochkr1.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 dochkr1.o
3 dochkr1.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
4 dochkr1.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
5 dochkr1.r ${⊢}{R}=\mathrm{Scalar}\left({U}\right)$
6 dochkr1.z
7 dochkr1.i
8 dochkr1.f ${⊢}{F}=\mathrm{LFnl}\left({U}\right)$
9 dochkr1.l ${⊢}{L}=\mathrm{LKer}\left({U}\right)$
10 dochkr1.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
11 dochkr1.g ${⊢}{\phi }\to {G}\in {F}$
12 dochkr1.n
13 eqid ${⊢}{0}_{{U}}={0}_{{U}}$
14 eqid ${⊢}\mathrm{LSAtoms}\left({U}\right)=\mathrm{LSAtoms}\left({U}\right)$
15 1 3 10 dvhlmod ${⊢}{\phi }\to {U}\in \mathrm{LMod}$
16 1 2 3 4 14 8 9 10 11 dochkrsat2
17 12 16 mpbid
18 13 14 15 17 lsateln0
19 eqid ${⊢}{0}_{{R}}={0}_{{R}}$
22 eldifsn
23 22 biimpri
25 1 2 3 4 5 19 13 8 9 20 21 24 dochfln0
26 25 ex
27 26 reximdva
28 18 27 mpd
29 4 8 9 15 11 lkrssv ${⊢}{\phi }\to {L}\left({G}\right)\subseteq {V}$
30 eqid ${⊢}\mathrm{LSubSp}\left({U}\right)=\mathrm{LSubSp}\left({U}\right)$
31 1 3 4 30 2 dochlss
32 10 29 31 syl2anc
33 15 32 jca
35 1 3 10 dvhlvec ${⊢}{\phi }\to {U}\in \mathrm{LVec}$
37 5 lvecdrng ${⊢}{U}\in \mathrm{LVec}\to {R}\in \mathrm{DivRing}$
38 36 37 syl
41 1 3 4 2 dochssv
42 10 29 41 syl2anc
43 42 sselda
45 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
46 5 45 4 8 lflcl ${⊢}\left({U}\in \mathrm{LMod}\wedge {G}\in {F}\wedge {z}\in {V}\right)\to {G}\left({z}\right)\in {\mathrm{Base}}_{{R}}$
47 39 40 44 46 syl3anc
48 simp3
49 eqid ${⊢}{inv}_{r}\left({R}\right)={inv}_{r}\left({R}\right)$
50 45 19 49 drnginvrcl ${⊢}\left({R}\in \mathrm{DivRing}\wedge {G}\left({z}\right)\in {\mathrm{Base}}_{{R}}\wedge {G}\left({z}\right)\ne {0}_{{R}}\right)\to {inv}_{r}\left({R}\right)\left({G}\left({z}\right)\right)\in {\mathrm{Base}}_{{R}}$
51 38 47 48 50 syl3anc
52 simp2
53 51 52 jca
54 eqid ${⊢}{\cdot }_{{U}}={\cdot }_{{U}}$
55 5 54 45 30 lssvscl
56 34 53 55 syl2anc
57 45 19 49 drnginvrn0 ${⊢}\left({R}\in \mathrm{DivRing}\wedge {G}\left({z}\right)\in {\mathrm{Base}}_{{R}}\wedge {G}\left({z}\right)\ne {0}_{{R}}\right)\to {inv}_{r}\left({R}\right)\left({G}\left({z}\right)\right)\ne {0}_{{R}}$
58 38 47 48 57 syl3anc
61 5 19 6 8 lfl0
62 59 60 61 syl2anc
63 fveqeq2
64 62 63 syl5ibrcom
65 64 necon3d
66 65 3impia
67 4 54 5 45 19 6 36 51 44 lvecvsn0
68 58 66 67 mpbir2and
69 eldifsn
70 56 68 69 sylanbrc
71 eqid ${⊢}{\cdot }_{{R}}={\cdot }_{{R}}$
72 5 45 71 4 54 8 lflmul ${⊢}\left({U}\in \mathrm{LMod}\wedge {G}\in {F}\wedge \left({inv}_{r}\left({R}\right)\left({G}\left({z}\right)\right)\in {\mathrm{Base}}_{{R}}\wedge {z}\in {V}\right)\right)\to {G}\left({inv}_{r}\left({R}\right)\left({G}\left({z}\right)\right){\cdot }_{{U}}{z}\right)={inv}_{r}\left({R}\right)\left({G}\left({z}\right)\right){\cdot }_{{R}}{G}\left({z}\right)$
73 39 40 51 44 72 syl112anc
74 45 19 71 7 49 drnginvrl
75 38 47 48 74 syl3anc
76 73 75 eqtrd
77 fveqeq2
78 77 rspcev
79 70 76 78 syl2anc
80 79 rexlimdv3a
81 28 80 mpd