Metamath Proof Explorer

Theorem orthcom

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

Ref Expression
Assertion orthcom ⊢ A ∈ ℋ ∧ B ∈ ℋ → A ⋅ ih B = 0 ↔ B ⋅ ih A = 0

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ A ⋅ ih B = 0 → A ⋅ ih B ‾ = 0 ‾
2 cj0 ⊢ 0 ‾ = 0
3 1 2 syl6eq ⊢ A ⋅ ih B = 0 → A ⋅ ih B ‾ = 0
4 ax-his1 ⊢ B ∈ ℋ ∧ A ∈ ℋ → B ⋅ ih A = A ⋅ ih B ‾
5 4 ancoms ⊢ A ∈ ℋ ∧ B ∈ ℋ → B ⋅ ih A = A ⋅ ih B ‾
6 5 eqeq1d ⊢ A ∈ ℋ ∧ B ∈ ℋ → B ⋅ ih A = 0 ↔ A ⋅ ih B ‾ = 0
7 3 6 syl5ibr ⊢ A ∈ ℋ ∧ B ∈ ℋ → A ⋅ ih B = 0 → B ⋅ ih A = 0
8 fveq2 ⊢ B ⋅ ih A = 0 → B ⋅ ih A ‾ = 0 ‾
9 8 2 syl6eq ⊢ B ⋅ ih A = 0 → B ⋅ ih A ‾ = 0
10 ax-his1 ⊢ A ∈ ℋ ∧ B ∈ ℋ → A ⋅ ih B = B ⋅ ih A ‾
11 10 eqeq1d ⊢ A ∈ ℋ ∧ B ∈ ℋ → A ⋅ ih B = 0 ↔ B ⋅ ih A ‾ = 0
12 9 11 syl5ibr ⊢ A ∈ ℋ ∧ B ∈ ℋ → B ⋅ ih A = 0 → A ⋅ ih B = 0
13 7 12 impbid ⊢ A ∈ ℋ ∧ B ∈ ℋ → A ⋅ ih B = 0 ↔ B ⋅ ih A = 0