# Metamath Proof Explorer

## Theorem dochexmid

Description: Excluded middle law for closed subspaces, which is equivalent to (and derived from) the orthomodular law dihoml4 . Lemma 3.3(2) in Holland95 p. 215. In our proof, we use the variables X , M , p , q , r in place of Hollands' l, m, P, Q, L respectively. ( pexmidALTN analog.) (Contributed by NM, 15-Jan-2015)

Ref Expression
Hypotheses dochexmid.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
dochexmid.o
dochexmid.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
dochexmid.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
dochexmid.s ${⊢}{S}=\mathrm{LSubSp}\left({U}\right)$
dochexmid.p
dochexmid.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
dochexmid.x ${⊢}{\phi }\to {X}\in {S}$
dochexmid.c
Assertion dochexmid

### Proof

Step Hyp Ref Expression
1 dochexmid.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 dochexmid.o
3 dochexmid.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
4 dochexmid.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
5 dochexmid.s ${⊢}{S}=\mathrm{LSubSp}\left({U}\right)$
6 dochexmid.p
7 dochexmid.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
8 dochexmid.x ${⊢}{\phi }\to {X}\in {S}$
9 dochexmid.c
10 id ${⊢}{X}=\left\{{0}_{{U}}\right\}\to {X}=\left\{{0}_{{U}}\right\}$
11 fveq2
12 10 11 oveq12d
13 1 3 7 dvhlmod ${⊢}{\phi }\to {U}\in \mathrm{LMod}$
14 eqid ${⊢}{0}_{{U}}={0}_{{U}}$
15 4 14 lmod0vcl ${⊢}{U}\in \mathrm{LMod}\to {0}_{{U}}\in {V}$
16 13 15 syl ${⊢}{\phi }\to {0}_{{U}}\in {V}$
17 16 snssd ${⊢}{\phi }\to \left\{{0}_{{U}}\right\}\subseteq {V}$
18 1 3 4 5 2 dochlss
19 7 17 18 syl2anc
20 5 lsssubg
21 13 19 20 syl2anc
22 14 6 lsm02
23 21 22 syl
24 1 3 2 4 14 doch0
25 7 24 syl
26 23 25 eqtrd
27 12 26 sylan9eqr
28 eqid ${⊢}\mathrm{LSpan}\left({U}\right)=\mathrm{LSpan}\left({U}\right)$
29 eqid ${⊢}\mathrm{LSAtoms}\left({U}\right)=\mathrm{LSAtoms}\left({U}\right)$
30 7 adantr ${⊢}\left({\phi }\wedge {X}\ne \left\{{0}_{{U}}\right\}\right)\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
31 8 adantr ${⊢}\left({\phi }\wedge {X}\ne \left\{{0}_{{U}}\right\}\right)\to {X}\in {S}$
32 simpr ${⊢}\left({\phi }\wedge {X}\ne \left\{{0}_{{U}}\right\}\right)\to {X}\ne \left\{{0}_{{U}}\right\}$