Metamath Proof Explorer


Theorem his1i

Description: Conjugate law for inner product. Postulate (S1) of Beran p. 95. (Contributed by NM, 15-May-2005) (New usage is discouraged.)

Ref Expression
Hypotheses his1.1
|- A e. ~H
his1.2
|- B e. ~H
Assertion his1i
|- ( A .ih B ) = ( * ` ( B .ih A ) )

Proof

Step Hyp Ref Expression
1 his1.1
 |-  A e. ~H
2 his1.2
 |-  B e. ~H
3 ax-his1
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( A .ih B ) = ( * ` ( B .ih A ) ) )
4 1 2 3 mp2an
 |-  ( A .ih B ) = ( * ` ( B .ih A ) )