Theorem his1i 27957

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

Hypotheses

Ref	Expression
his1.1	|- A e. ~H
his1.2	|- B e. ~H

Assertion

Ref	Expression
his1i	|- ( A .ih B ) = ( * ` ( B .ih A ) )

Proof of Theorem his1i

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

Syntax hints:   = wceq 1483   e. wcel 1990   ` cfv 5888  (class class class)co 6650   *ccj 13836   ~Hchil 27776   .ih csp 27779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-his1 27939

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  normlem2  27968  bcseqi  27977  bcsiALT  28036  pjadjii  28533  lnopunilem1  28869  lnophmlem2  28876