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 | |
|
pexmid.p | |
||
pexmid.o | |
||
Assertion | pexmidN | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pexmid.a | |
|
2 | pexmid.p | |
|
3 | pexmid.o | |
|
4 | simpll | |
|
5 | simplr | |
|
6 | 1 3 | polssatN | |
7 | 6 | adantr | |
8 | 1 2 3 | poldmj1N | |
9 | 4 5 7 8 | syl3anc | |
10 | 1 3 | pnonsingN | |
11 | 4 7 10 | syl2anc | |
12 | 9 11 | eqtrd | |
13 | 12 | fveq2d | |
14 | simpr | |
|
15 | eqid | |
|
16 | 1 3 15 | ispsubclN | |
17 | 16 | ad2antrr | |
18 | 5 14 17 | mpbir2and | |
19 | 1 3 15 | polsubclN | |
20 | 19 | adantr | |
21 | 1 3 | 2polssN | |
22 | 21 | adantr | |
23 | 2 3 15 | osumclN | |
24 | 4 18 20 22 23 | syl31anc | |
25 | 3 15 | psubcli2N | |
26 | 4 24 25 | syl2anc | |
27 | 1 3 | pol0N | |
28 | 27 | ad2antrr | |
29 | 13 26 28 | 3eqtr3d | |