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

Theorem pexmidN 30703
 Description: Excluded middle law for closed projective subspaces, which can be shown to be equivalent to (and derivable from) the orthomodular law poml4N 30687. Lemma 3.3(2) in [Holland95] p. 215, which we prove as a special case of osumclN 30701. (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 731 . . . . 5
2 simplr 732 . . . . 5
3 pexmid.a . . . . . . 7
4 pexmid.o . . . . . . 7
53, 4polssatN 30642 . . . . . 6
65adantr 452 . . . . 5
7 pexmid.p . . . . . 6
83, 7, 4poldmj1N 30662 . . . . 5
91, 2, 6, 8syl3anc 1184 . . . 4
103, 4pnonsingN 30667 . . . . 5
111, 6, 10syl2anc 643 . . . 4
129, 11eqtrd 2467 . . 3
1312fveq2d 5724 . 2
14 simpr 448 . . . . 5
15 eqid 2435 . . . . . . 7
163, 4, 15ispsubclN 30671 . . . . . 6
1716ad2antrr 707 . . . . 5
182, 14, 17mpbir2and 889 . . . 4
193, 4, 15polsubclN 30686 . . . . 5
2019adantr 452 . . . 4
213, 42polssN 30649 . . . . 5
2221adantr 452 . . . 4
237, 4, 15osumclN 30701 . . . 4
241, 18, 20, 22, 23syl31anc 1187 . . 3
254, 15psubcli2N 30673 . . 3
261, 24, 25syl2anc 643 . 2
273, 4pol0N 30643 . . 3