Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dochexmid Unicode version

Theorem dochexmid 30347
 Description: Excluded middle law for closed subspaces, which is equivalent to (and derived from) the orthomodular law dihoml4 30256. Lemma 3.3(2) in [Holland95] p. 215. In our proof, we use the variables , , , , in place of Hollands' l, m, P, Q, L respectively. (pexmidALTN 28856 analog.) (Contributed by NM, 15-Jan-2015.)
Hypotheses
Ref Expression
dochexmid.h
dochexmid.o
dochexmid.u
dochexmid.v
dochexmid.s
dochexmid.p
dochexmid.k
dochexmid.x
dochexmid.c
Assertion
Ref Expression
dochexmid

Proof of Theorem dochexmid
StepHypRef Expression
1 id 21 . . . 4
2 fveq2 5377 . . . 4
31, 2oveq12d 5728 . . 3
4 dochexmid.h . . . . . . 7
5 dochexmid.u . . . . . . 7
6 dochexmid.k . . . . . . 7
74, 5, 6dvhlmod 29989 . . . . . 6
8 dochexmid.v . . . . . . . . . 10
9 eqid 2253 . . . . . . . . . 10
108, 9lmod0vcl 15494 . . . . . . . . 9
117, 10syl 17 . . . . . . . 8
1211snssd 3660 . . . . . . 7
13 dochexmid.s . . . . . . . 8
14 dochexmid.o . . . . . . . 8
154, 5, 8, 13, 14dochlss 30233 . . . . . . 7
166, 12, 15syl2anc 645 . . . . . 6
1713lsssubg 15549 . . . . . 6 SubGrp
187, 16, 17syl2anc 645 . . . . 5 SubGrp
19 dochexmid.p . . . . . 6
209, 19lsm02 14816 . . . . 5 SubGrp
2118, 20syl 17 . . . 4
224, 5, 14, 8, 9doch0 30237 . . . . 5
236, 22syl 17 . . . 4
2421, 23eqtrd 2285 . . 3
253, 24sylan9eqr 2307 . 2
26 eqid 2253 . . 3
27 eqid 2253 . . 3 LSAtoms LSAtoms