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 eqtrdi 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 eqtrdi 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