Theorem his1i 10599

Description: Conjugate law for inner product. Postulate (S1) of [Beran] p. 95.

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 10582	. 2 |- ((A e. ~H /\ B e. ~H) -> (A .ih B) = (*` (B .ih A)))
4	1, 2, 3	mp2an 761	1 |- (A .ih B) = (*` (B .ih A))

Syntax hints:   = wceq 1298   e. wcel 1300  ` cfv 3998  (class class class)co 4884  *ccj 7999  ~Hchil 10420   .ih csp 10425

This theorem is referenced by:  normlem2 10610  bcseqi 10619  bcsiALT 10679  pjthlem5 10856  pjthlem6 10857  pjthlem13 10864  pjadjii 11253  lnopunilem1 11572  lnophmlem2 11579

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

This theorem depends on definitions:  df-bi 164  df-an 242

Copyright terms: Public domain