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

Theorem pexmidALTN 30614
 Description: Excluded middle law for closed projective subspaces, which is equivalent to (and derived from) the orthomodular law poml4N 30589. 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. TODO: should we make this obsolete? (Contributed by NM, 3-Feb-2012.) (New usage is discouraged.)
Hypotheses
Ref Expression
pexmidALT.a
pexmidALT.p
pexmidALT.o
Assertion
Ref Expression
pexmidALTN

Proof of Theorem pexmidALTN
StepHypRef Expression
1 id 20 . . . 4
2 fveq2 5719 . . . 4
31, 2oveq12d 6090 . . 3
4 pexmidALT.a . . . . . . . 8
5 pexmidALT.o . . . . . . . 8
64, 5pol0N 30545 . . . . . . 7
7 eqimss 3392 . . . . . . 7
86, 7syl 16 . . . . . 6
9 pexmidALT.p . . . . . . 7
104, 9padd02 30448 . . . . . 6
118, 10mpdan 650 . . . . 5
1211, 6eqtrd 2467 . . . 4