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

Theorem pexmidN 28847
 Description: Excluded middle law for closed projective subspaces, which can be shown to be equivalent to (and derivable from) the orthomodular law poml4N 28831. Lemma 3.3(2) in [Holland95] p. 215, which we prove as a special case of osumclN 28845. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.)
Hypotheses
Ref Expression
pexmid.a
pexmid.p
pexmid.o
Assertion
Ref Expression
pexmidN

Proof of Theorem pexmidN
StepHypRef Expression
1 simpll 733 . . . . 5
2 simplr 734 . . . . 5
3 pexmid.a . . . . . . 7
4 pexmid.o . . . . . . 7
53, 4polssatN 28786 . . . . . 6
65adantr 453 . . . . 5
7 pexmid.p . . . . . 6
83, 7, 4poldmj1N 28806 . . . . 5
91, 2, 6, 8syl3anc 1187 . . . 4
103, 4pnonsingN 28811 . . . . 5
111, 6, 10syl2anc 645 . . . 4
129, 11eqtrd 2285 . . 3
1312fveq2d 5381 . 2
14 simpr 449 . . . . 5
15 eqid 2253 . . . . . . 7
163, 4, 15ispsubclN 28815 . . . . . 6
1716ad2antrr 709 . . . . 5
182, 14, 17mpbir2and 893 . . . 4
193, 4, 15polsubclN 28830 . . . . 5
2019adantr 453 . . . 4
213, 42polssN 28793 . . . . 5
2221adantr 453 . . . 4
237, 4, 15osumclN 28845 . . . 4
241, 18, 20, 22, 23syl31anc 1190 . . 3
254, 15psubcli2N 28817 . . 3
261, 24, 25syl2anc 645 . 2
273, 4pol0N 28787 . . 3