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