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 𝐴C
pjoml.2 𝐵S
Assertion pjomli ( ( 𝐴𝐵 ∧ ( 𝐵 ∩ ( ⊥ ‘ 𝐴 ) ) = 0 ) → 𝐴 = 𝐵 )

Proof

Step Hyp Ref Expression
1 pjoml.1 𝐴C
2 pjoml.2 𝐵S
3 1 2 omlsi ( ( 𝐴𝐵 ∧ ( 𝐵 ∩ ( ⊥ ‘ 𝐴 ) ) = 0 ) → 𝐴 = 𝐵 )