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

Proof

Step Hyp Ref Expression
1 sseq1 A=ifACA0ABifACA0B
2 fveq2 A=ifACA0A=ifACA0
3 2 ineq2d A=ifACA0BA=BifACA0
4 3 eqeq1d A=ifACA0BA=0BifACA0=0
5 1 4 anbi12d A=ifACA0ABBA=0ifACA0BBifACA0=0
6 eqeq1 A=ifACA0A=BifACA0=B
7 5 6 imbi12d A=ifACA0ABBA=0A=BifACA0BBifACA0=0ifACA0=B
8 sseq2 B=ifBSB0ifACA0BifACA0ifBSB0
9 ineq1 B=ifBSB0BifACA0=ifBSB0ifACA0
10 9 eqeq1d B=ifBSB0BifACA0=0ifBSB0ifACA0=0
11 8 10 anbi12d B=ifBSB0ifACA0BBifACA0=0ifACA0ifBSB0ifBSB0ifACA0=0
12 eqeq2 B=ifBSB0ifACA0=BifACA0=ifBSB0
13 11 12 imbi12d B=ifBSB0ifACA0BBifACA0=0ifACA0=BifACA0ifBSB0ifBSB0ifACA0=0ifACA0=ifBSB0
14 h0elch 0C
15 14 elimel ifACA0C
16 h0elsh 0S
17 16 elimel ifBSB0S
18 15 17 pjomli ifACA0ifBSB0ifBSB0ifACA0=0ifACA0=ifBSB0
19 7 13 18 dedth2h ACBSABBA=0A=B
20 19 imp ACBSABBA=0A=B