Theorem his1 8905

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

Syntax hints:   = wceq 954   e. wcel 956  ` cfv 3177  (class class class)co 3954  *ccj 6688  H~chil 8727   .ih csp 8732

This theorem is referenced by:  normlem2 8916  bcseq 8925  bcsALT 8985  pjthlem5 9161  pjthlem6 9162  pjthlem13 9169  pjadj 9558  lnopunilem1 9873  lnophmlem2 9880

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

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

Copyright terms: Public domain