Metamath Proof Explorer


Theorem pexmidN

Description: Excluded middle law for closed projective subspaces, which can be shown to be equivalent to (and derivable from) the orthomodular law poml4N . Lemma 3.3(2) in Holland95 p. 215, which we prove as a special case of osumclN . (Contributed by NM, 25-Mar-2012) (New usage is discouraged.)

Ref Expression
Hypotheses pexmid.a A=AtomsK
pexmid.p +˙=+𝑃K
pexmid.o ˙=𝑃K
Assertion pexmidN KHLXA˙˙X=XX+˙˙X=A

Proof

Step Hyp Ref Expression
1 pexmid.a A=AtomsK
2 pexmid.p +˙=+𝑃K
3 pexmid.o ˙=𝑃K
4 simpll KHLXA˙˙X=XKHL
5 simplr KHLXA˙˙X=XXA
6 1 3 polssatN KHLXA˙XA
7 6 adantr KHLXA˙˙X=X˙XA
8 1 2 3 poldmj1N KHLXA˙XA˙X+˙˙X=˙X˙˙X
9 4 5 7 8 syl3anc KHLXA˙˙X=X˙X+˙˙X=˙X˙˙X
10 1 3 pnonsingN KHL˙XA˙X˙˙X=
11 4 7 10 syl2anc KHLXA˙˙X=X˙X˙˙X=
12 9 11 eqtrd KHLXA˙˙X=X˙X+˙˙X=
13 12 fveq2d KHLXA˙˙X=X˙˙X+˙˙X=˙
14 simpr KHLXA˙˙X=X˙˙X=X
15 eqid PSubClK=PSubClK
16 1 3 15 ispsubclN KHLXPSubClKXA˙˙X=X
17 16 ad2antrr KHLXA˙˙X=XXPSubClKXA˙˙X=X
18 5 14 17 mpbir2and KHLXA˙˙X=XXPSubClK
19 1 3 15 polsubclN KHLXA˙XPSubClK
20 19 adantr KHLXA˙˙X=X˙XPSubClK
21 1 3 2polssN KHLXAX˙˙X
22 21 adantr KHLXA˙˙X=XX˙˙X
23 2 3 15 osumclN KHLXPSubClK˙XPSubClKX˙˙XX+˙˙XPSubClK
24 4 18 20 22 23 syl31anc KHLXA˙˙X=XX+˙˙XPSubClK
25 3 15 psubcli2N KHLX+˙˙XPSubClK˙˙X+˙˙X=X+˙˙X
26 4 24 25 syl2anc KHLXA˙˙X=X˙˙X+˙˙X=X+˙˙X
27 1 3 pol0N KHL˙=A
28 27 ad2antrr KHLXA˙˙X=X˙=A
29 13 26 28 3eqtr3d KHLXA˙˙X=XX+˙˙X=A