# Metamath Proof Explorer

## Theorem orthcom

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

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

### Proof

Step Hyp Ref Expression
1 fveq2 ${⊢}{A}{\cdot }_{\mathrm{ih}}{B}=0\to \stackrel{‾}{{A}{\cdot }_{\mathrm{ih}}{B}}=\stackrel{‾}{0}$
2 cj0 ${⊢}\stackrel{‾}{0}=0$
3 1 2 eqtrdi ${⊢}{A}{\cdot }_{\mathrm{ih}}{B}=0\to \stackrel{‾}{{A}{\cdot }_{\mathrm{ih}}{B}}=0$
4 ax-his1 ${⊢}\left({B}\in ℋ\wedge {A}\in ℋ\right)\to {B}{\cdot }_{\mathrm{ih}}{A}=\stackrel{‾}{{A}{\cdot }_{\mathrm{ih}}{B}}$
5 4 ancoms ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to {B}{\cdot }_{\mathrm{ih}}{A}=\stackrel{‾}{{A}{\cdot }_{\mathrm{ih}}{B}}$
6 5 eqeq1d ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to \left({B}{\cdot }_{\mathrm{ih}}{A}=0↔\stackrel{‾}{{A}{\cdot }_{\mathrm{ih}}{B}}=0\right)$
7 3 6 syl5ibr ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\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 \stackrel{‾}{{B}{\cdot }_{\mathrm{ih}}{A}}=\stackrel{‾}{0}$
9 8 2 eqtrdi ${⊢}{B}{\cdot }_{\mathrm{ih}}{A}=0\to \stackrel{‾}{{B}{\cdot }_{\mathrm{ih}}{A}}=0$
10 ax-his1 ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to {A}{\cdot }_{\mathrm{ih}}{B}=\stackrel{‾}{{B}{\cdot }_{\mathrm{ih}}{A}}$
11 10 eqeq1d ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to \left({A}{\cdot }_{\mathrm{ih}}{B}=0↔\stackrel{‾}{{B}{\cdot }_{\mathrm{ih}}{A}}=0\right)$
12 9 11 syl5ibr ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to \left({B}{\cdot }_{\mathrm{ih}}{A}=0\to {A}{\cdot }_{\mathrm{ih}}{B}=0\right)$
13 7 12 impbid ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to \left({A}{\cdot }_{\mathrm{ih}}{B}=0↔{B}{\cdot }_{\mathrm{ih}}{A}=0\right)$