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

Theorem dochexmid 32203
 Description: Excluded middle law for closed subspaces, which is equivalent to (and derived from) the orthomodular law dihoml4 32112. 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 30712 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 20 . . . 4
2 fveq2 5720 . . . 4
31, 2oveq12d 6091 . . 3
4 dochexmid.h . . . . . . 7
5 dochexmid.u . . . . . . 7
6 dochexmid.k . . . . . . 7
74, 5, 6dvhlmod 31845 . . . . . 6
8 dochexmid.v . . . . . . . . . 10
9 eqid 2435 . . . . . . . . . 10
108, 9lmod0vcl 15971 . . . . . . . . 9
117, 10syl 16 . . . . . . . 8
1211snssd 3935 . . . . . . 7
13 dochexmid.s . . . . . . . 8
14 dochexmid.o . . . . . . . 8
154, 5, 8, 13, 14dochlss 32089 . . . . . . 7
166, 12, 15syl2anc 643 . . . . . 6
1713lsssubg 16025 . . . . . 6 SubGrp
187, 16, 17syl2anc 643 . . . . 5 SubGrp
19 dochexmid.p . . . . . 6
209, 19lsm02 15296 . . . . 5 SubGrp
2118, 20syl 16 . . . 4
224, 5, 14, 8, 9doch0 32093 . . . . 5
236, 22syl 16 . . . 4
2421, 23eqtrd 2467 . . 3
253, 24sylan9eqr 2489 . 2
26 eqid 2435 . . 3
27 eqid 2435 . . 3 LSAtoms LSAtoms