Theorem his1 8887

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

Syntax hints:   = wceq 953   e. wcel 955  ` cfv 3172  (class class class)co 3948  *ccj 6680  H~chil 8727   .ih csp 8732

This theorem is referenced by:  normlem2 8898  bcseq 8907  bcsALT 8967  pjthlem5 9138  pjthlem6 9139  pjthlem13 9146  pjadj 9535  lnopunilem1 9850  lnophmlem2 9857

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

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

Copyright terms: Public domain