Metamath Proof Explorer


Theorem pjomli

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 )

Proof

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 )