Theorem cmcm2

Description: Commutation with orthocomplement. Theorem 2.3(i) of Beran p. 39. (Contributed by NM, 14-Jun-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	cmcm2	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(A{𝐶}_{\mathscr{H}}B\leftrightarrow A{𝐶}_{\mathscr{H}}\perp \left(B\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		cmcm3	$$⊢\left(B\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(B{𝐶}_{\mathscr{H}}A\leftrightarrow \perp \left(B\right){𝐶}_{\mathscr{H}}A\right)$$
2	1	ancoms	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(B{𝐶}_{\mathscr{H}}A\leftrightarrow \perp \left(B\right){𝐶}_{\mathscr{H}}A\right)$$
3		cmcm	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(A{𝐶}_{\mathscr{H}}B\leftrightarrow B{𝐶}_{\mathscr{H}}A\right)$$
4		choccl	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}\to \perp \left(B\right)\in {\mathbf{C}}_{\mathscr{H}}$$
5		cmcm	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge \perp \left(B\right)\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(A{𝐶}_{\mathscr{H}}\perp \left(B\right)\leftrightarrow \perp \left(B\right){𝐶}_{\mathscr{H}}A\right)$$
6	4 5	sylan2	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(A{𝐶}_{\mathscr{H}}\perp \left(B\right)\leftrightarrow \perp \left(B\right){𝐶}_{\mathscr{H}}A\right)$$
7	2 3 6	3bitr4d	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(A{𝐶}_{\mathscr{H}}B\leftrightarrow A{𝐶}_{\mathscr{H}}\perp \left(B\right)\right)$$