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, 6-Nov-1999) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | pjoml.1 | |- A e. CH |
|
pjoml.2 | |- B e. SH |
||
Assertion | pjomli | |- ( ( A C_ B /\ ( B i^i ( _|_ ` A ) ) = 0H ) -> A = B ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pjoml.1 | |- A e. CH |
|
2 | pjoml.2 | |- B e. SH |
|
3 | 1 2 | omlsi | |- ( ( A C_ B /\ ( B i^i ( _|_ ` A ) ) = 0H ) -> A = B ) |