Theorem his1 8966

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
his1	|- (A .ih B) = (*` (B .ih A))

Proof of Theorem his1

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

Syntax hints:   = wceq 956   e. wcel 958  ` cfv 3182  (class class class)co 3963  *ccj 6749  H~chil 8788   .ih csp 8793

This theorem is referenced by:  normlem2 8977  bcseq 8986  bcsALT 9046  pjthlem5 9223  pjthlem6 9224  pjthlem13 9231  pjadj 9618  lnopunilem1 9935  lnophmlem2 9942

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

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain