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 )