# Metamath Proof Explorer

## Theorem dochsatshp

Description: The orthocomplement of a subspace atom is a hyperplane. (Contributed by NM, 27-Jul-2014) (Revised by Mario Carneiro, 1-Oct-2014)

Ref Expression
Hypotheses dochsatshp.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
dochsatshp.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
dochsatshp.o
dochsatshp.a ${⊢}{A}=\mathrm{LSAtoms}\left({U}\right)$
dochsatshp.y ${⊢}{Y}=\mathrm{LSHyp}\left({U}\right)$
dochsatshp.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
dochsatshp.q ${⊢}{\phi }\to {Q}\in {A}$
Assertion dochsatshp

### Proof

Step Hyp Ref Expression
1 dochsatshp.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 dochsatshp.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
3 dochsatshp.o
4 dochsatshp.a ${⊢}{A}=\mathrm{LSAtoms}\left({U}\right)$
5 dochsatshp.y ${⊢}{Y}=\mathrm{LSHyp}\left({U}\right)$
6 dochsatshp.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
7 dochsatshp.q ${⊢}{\phi }\to {Q}\in {A}$
8 eqid ${⊢}{\mathrm{Base}}_{{U}}={\mathrm{Base}}_{{U}}$
9 1 2 6 dvhlmod ${⊢}{\phi }\to {U}\in \mathrm{LMod}$
10 8 4 9 7 lsatssv ${⊢}{\phi }\to {Q}\subseteq {\mathrm{Base}}_{{U}}$
11 eqid ${⊢}\mathrm{LSubSp}\left({U}\right)=\mathrm{LSubSp}\left({U}\right)$
12 1 2 8 11 3 dochlss
13 6 10 12 syl2anc
14 eqid ${⊢}{0}_{{U}}={0}_{{U}}$
15 14 4 9 7 lsatn0 ${⊢}{\phi }\to {Q}\ne \left\{{0}_{{U}}\right\}$
16 1 2 3 8 14 doch0
17 6 16 syl
18 17 eqeq2d
19 eqid ${⊢}\mathrm{DIsoH}\left({K}\right)\left({W}\right)=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
20 1 2 19 4 dih1dimat ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {Q}\in {A}\right)\to {Q}\in \mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
21 6 7 20 syl2anc ${⊢}{\phi }\to {Q}\in \mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
22 1 19 2 14 dih0rn ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \left\{{0}_{{U}}\right\}\in \mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
23 6 22 syl ${⊢}{\phi }\to \left\{{0}_{{U}}\right\}\in \mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
24 1 19 3 6 21 23 doch11
25 18 24 bitr3d
26 25 necon3bid
27 15 26 mpbird
28 eqid ${⊢}\mathrm{LSpan}\left({U}\right)=\mathrm{LSpan}\left({U}\right)$
29 8 28 14 4 islsat ${⊢}{U}\in \mathrm{LMod}\to \left({Q}\in {A}↔\exists {v}\in \left({\mathrm{Base}}_{{U}}\setminus \left\{{0}_{{U}}\right\}\right)\phantom{\rule{.4em}{0ex}}{Q}=\mathrm{LSpan}\left({U}\right)\left(\left\{{v}\right\}\right)\right)$
30 9 29 syl ${⊢}{\phi }\to \left({Q}\in {A}↔\exists {v}\in \left({\mathrm{Base}}_{{U}}\setminus \left\{{0}_{{U}}\right\}\right)\phantom{\rule{.4em}{0ex}}{Q}=\mathrm{LSpan}\left({U}\right)\left(\left\{{v}\right\}\right)\right)$
31 7 30 mpbid ${⊢}{\phi }\to \exists {v}\in \left({\mathrm{Base}}_{{U}}\setminus \left\{{0}_{{U}}\right\}\right)\phantom{\rule{.4em}{0ex}}{Q}=\mathrm{LSpan}\left({U}\right)\left(\left\{{v}\right\}\right)$
32 eldifi ${⊢}{v}\in \left({\mathrm{Base}}_{{U}}\setminus \left\{{0}_{{U}}\right\}\right)\to {v}\in {\mathrm{Base}}_{{U}}$
33 32 adantr ${⊢}\left({v}\in \left({\mathrm{Base}}_{{U}}\setminus \left\{{0}_{{U}}\right\}\right)\wedge {Q}=\mathrm{LSpan}\left({U}\right)\left(\left\{{v}\right\}\right)\right)\to {v}\in {\mathrm{Base}}_{{U}}$
34 33 a1i ${⊢}{\phi }\to \left(\left({v}\in \left({\mathrm{Base}}_{{U}}\setminus \left\{{0}_{{U}}\right\}\right)\wedge {Q}=\mathrm{LSpan}\left({U}\right)\left(\left\{{v}\right\}\right)\right)\to {v}\in {\mathrm{Base}}_{{U}}\right)$
35 11 28 lspid
36 9 13 35 syl2anc
37 36 uneq1d
38 37 fveq2d
40 9 adantr ${⊢}\left({\phi }\wedge \left({v}\in \left({\mathrm{Base}}_{{U}}\setminus \left\{{0}_{{U}}\right\}\right)\wedge {Q}=\mathrm{LSpan}\left({U}\right)\left(\left\{{v}\right\}\right)\right)\right)\to {U}\in \mathrm{LMod}$
41 8 11 lssss
42 13 41 syl
44 32 snssd ${⊢}{v}\in \left({\mathrm{Base}}_{{U}}\setminus \left\{{0}_{{U}}\right\}\right)\to \left\{{v}\right\}\subseteq {\mathrm{Base}}_{{U}}$
45 44 adantr ${⊢}\left({v}\in \left({\mathrm{Base}}_{{U}}\setminus \left\{{0}_{{U}}\right\}\right)\wedge {Q}=\mathrm{LSpan}\left({U}\right)\left(\left\{{v}\right\}\right)\right)\to \left\{{v}\right\}\subseteq {\mathrm{Base}}_{{U}}$
46 45 adantl ${⊢}\left({\phi }\wedge \left({v}\in \left({\mathrm{Base}}_{{U}}\setminus \left\{{0}_{{U}}\right\}\right)\wedge {Q}=\mathrm{LSpan}\left({U}\right)\left(\left\{{v}\right\}\right)\right)\right)\to \left\{{v}\right\}\subseteq {\mathrm{Base}}_{{U}}$
47 8 28 lspun
48 40 43 46 47 syl3anc
49 uneq2
50 49 fveq2d
53 39 48 52 3eqtr4d
54 eqid ${⊢}\mathrm{joinH}\left({K}\right)\left({W}\right)=\mathrm{joinH}\left({K}\right)\left({W}\right)$
55 eqid ${⊢}\mathrm{LSSum}\left({U}\right)=\mathrm{LSSum}\left({U}\right)$
56 1 19 2 8 3 dochcl
57 6 10 56 syl2anc
58 1 19 54 2 55 4 6 57 7 dihjat2
59 1 2 8 54 6 42 10 djhcom
60 11 4 9 7 lsatlssel ${⊢}{\phi }\to {Q}\in \mathrm{LSubSp}\left({U}\right)$
61 11 28 55 lsmsp
62 9 13 60 61 syl3anc
63 58 59 62 3eqtr3rd
64 1 2 8 3 54 djhexmid
65 6 10 64 syl2anc
66 63 65 eqtrd
73 1 2 6 dvhlvec ${⊢}{\phi }\to {U}\in \mathrm{LVec}$