Metamath Proof Explorer


Theorem hire

Description: A necessary and sufficient condition for an inner product to be real. (Contributed by NM, 2-Jul-2005) (New usage is discouraged.)

Ref Expression
Assertion hire A B A ih B A ih B = B ih A

Proof

Step Hyp Ref Expression
1 hicl A B A ih B
2 cjreb A ih B A ih B A ih B = A ih B
3 1 2 syl A B A ih B A ih B = A ih B
4 eqcom A ih B = A ih B A ih B = A ih B
5 3 4 bitrdi A B A ih B A ih B = A ih B
6 ax-his1 B A B ih A = A ih B
7 6 ancoms A B B ih A = A ih B
8 7 eqeq2d A B A ih B = B ih A A ih B = A ih B
9 5 8 bitr4d A B A ih B A ih B = B ih A