Description: Subspace form of orthomodular law in the Hilbert lattice. Compare the orthomodular law in Theorem 2(ii) of Kalmbach p. 22. Derived using projections; compare omlsi . (Contributed by NM, 14-Jun-2006) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | pjoml | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sseq1 | |
|
2 | fveq2 | |
|
3 | 2 | ineq2d | |
4 | 3 | eqeq1d | |
5 | 1 4 | anbi12d | |
6 | eqeq1 | |
|
7 | 5 6 | imbi12d | |
8 | sseq2 | |
|
9 | ineq1 | |
|
10 | 9 | eqeq1d | |
11 | 8 10 | anbi12d | |
12 | eqeq2 | |
|
13 | 11 12 | imbi12d | |
14 | h0elch | |
|
15 | 14 | elimel | |
16 | h0elsh | |
|
17 | 16 | elimel | |
18 | 15 17 | pjomli | |
19 | 7 13 18 | dedth2h | |
20 | 19 | imp | |