Metamath Proof Explorer


Theorem pjoml

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 A C B S A B B A = 0 A = B

Proof

Step Hyp Ref Expression
1 sseq1 A = if A C A 0 A B if A C A 0 B
2 fveq2 A = if A C A 0 A = if A C A 0
3 2 ineq2d A = if A C A 0 B A = B if A C A 0
4 3 eqeq1d A = if A C A 0 B A = 0 B if A C A 0 = 0
5 1 4 anbi12d A = if A C A 0 A B B A = 0 if A C A 0 B B if A C A 0 = 0
6 eqeq1 A = if A C A 0 A = B if A C A 0 = B
7 5 6 imbi12d A = if A C A 0 A B B A = 0 A = B if A C A 0 B B if A C A 0 = 0 if A C A 0 = B
8 sseq2 B = if B S B 0 if A C A 0 B if A C A 0 if B S B 0
9 ineq1 B = if B S B 0 B if A C A 0 = if B S B 0 if A C A 0
10 9 eqeq1d B = if B S B 0 B if A C A 0 = 0 if B S B 0 if A C A 0 = 0
11 8 10 anbi12d B = if B S B 0 if A C A 0 B B if A C A 0 = 0 if A C A 0 if B S B 0 if B S B 0 if A C A 0 = 0
12 eqeq2 B = if B S B 0 if A C A 0 = B if A C A 0 = if B S B 0
13 11 12 imbi12d B = if B S B 0 if A C A 0 B B if A C A 0 = 0 if A C A 0 = B if A C A 0 if B S B 0 if B S B 0 if A C A 0 = 0 if A C A 0 = if B S B 0
14 h0elch 0 C
15 14 elimel if A C A 0 C
16 h0elsh 0 S
17 16 elimel if B S B 0 S
18 15 17 pjomli if A C A 0 if B S B 0 if B S B 0 if A C A 0 = 0 if A C A 0 = if B S B 0
19 7 13 18 dedth2h A C B S A B B A = 0 A = B
20 19 imp A C B S A B B A = 0 A = B