Theorem orthcom

Description: Orthogonality commutes. (Contributed by NM, 10-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Assertion	orthcom	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to \left(A{\cdot }_{\mathrm{ih}}B=0\leftrightarrow B{\cdot }_{\mathrm{ih}}A=0\right)$$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$$⊢A{\cdot }_{\mathrm{ih}}B=0\to \overline{A{\cdot }_{\mathrm{ih}}B}=\bar{0}$$
2		cj0	$$⊢\bar{0}=0$$
3	1 2	eqtrdi	$$⊢A{\cdot }_{\mathrm{ih}}B=0\to \overline{A{\cdot }_{\mathrm{ih}}B}=0$$
4		ax-his1	$$⊢\left(B\in \mathscr{H}\wedge A\in \mathscr{H}\right)\to B{\cdot }_{\mathrm{ih}}A=\overline{A{\cdot }_{\mathrm{ih}}B}$$
5	4	ancoms	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to B{\cdot }_{\mathrm{ih}}A=\overline{A{\cdot }_{\mathrm{ih}}B}$$
6	5	eqeq1d	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to \left(B{\cdot }_{\mathrm{ih}}A=0\leftrightarrow \overline{A{\cdot }_{\mathrm{ih}}B}=0\right)$$
7	3 6	imbitrrid	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to \left(A{\cdot }_{\mathrm{ih}}B=0\to B{\cdot }_{\mathrm{ih}}A=0\right)$$
8		fveq2	$$⊢B{\cdot }_{\mathrm{ih}}A=0\to \overline{B{\cdot }_{\mathrm{ih}}A}=\bar{0}$$
9	8 2	eqtrdi	$$⊢B{\cdot }_{\mathrm{ih}}A=0\to \overline{B{\cdot }_{\mathrm{ih}}A}=0$$
10		ax-his1	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to A{\cdot }_{\mathrm{ih}}B=\overline{B{\cdot }_{\mathrm{ih}}A}$$
11	10	eqeq1d	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to \left(A{\cdot }_{\mathrm{ih}}B=0\leftrightarrow \overline{B{\cdot }_{\mathrm{ih}}A}=0\right)$$
12	9 11	imbitrrid	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to \left(B{\cdot }_{\mathrm{ih}}A=0\to A{\cdot }_{\mathrm{ih}}B=0\right)$$
13	7 12	impbid	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to \left(A{\cdot }_{\mathrm{ih}}B=0\leftrightarrow B{\cdot }_{\mathrm{ih}}A=0\right)$$