Metamath Proof Explorer


Theorem cmcm3

Description: Commutation with orthocomplement. Remark in Kalmbach p. 23. (Contributed by NM, 13-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion cmcm3 ACBCA𝐶BA𝐶B

Proof

Step Hyp Ref Expression
1 breq1 A=ifACA0A𝐶BifACA0𝐶B
2 fveq2 A=ifACA0A=ifACA0
3 2 breq1d A=ifACA0A𝐶BifACA0𝐶B
4 1 3 bibi12d A=ifACA0A𝐶BA𝐶BifACA0𝐶BifACA0𝐶B
5 breq2 B=ifBCB0ifACA0𝐶BifACA0𝐶ifBCB0
6 breq2 B=ifBCB0ifACA0𝐶BifACA0𝐶ifBCB0
7 5 6 bibi12d B=ifBCB0ifACA0𝐶BifACA0𝐶BifACA0𝐶ifBCB0ifACA0𝐶ifBCB0
8 h0elch 0C
9 8 elimel ifACA0C
10 8 elimel ifBCB0C
11 9 10 cmcm3i ifACA0𝐶ifBCB0ifACA0𝐶ifBCB0
12 4 7 11 dedth2h ACBCA𝐶BA𝐶B