Metamath Proof Explorer


Axiom ax-his1

Description: Conjugate law for inner product. Postulate (S1) of Beran p. 95. Note that *x is the complex conjugate cjval of x . In the literature, the inner product of A and B is usually written <. A , B >. , but our operation notation co allows us to use existing theorems about operations and also avoids a clash with the definition of an ordered pair df-op . Physicists use <. B | A >. , called Dirac bra-ket notation, to represent this operation; see comments in df-bra . (Contributed by NM, 29-Jul-1999) (New usage is discouraged.)

Ref Expression
Assertion ax-his1
|- ( ( A e. ~H /\ B e. ~H ) -> ( A .ih B ) = ( * ` ( B .ih A ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA
 |-  A
1 chba
 |-  ~H
2 0 1 wcel
 |-  A e. ~H
3 cB
 |-  B
4 3 1 wcel
 |-  B e. ~H
5 2 4 wa
 |-  ( A e. ~H /\ B e. ~H )
6 csp
 |-  .ih
7 0 3 6 co
 |-  ( A .ih B )
8 ccj
 |-  *
9 3 0 6 co
 |-  ( B .ih A )
10 9 8 cfv
 |-  ( * ` ( B .ih A ) )
11 7 10 wceq
 |-  ( A .ih B ) = ( * ` ( B .ih A ) )
12 5 11 wi
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( A .ih B ) = ( * ` ( B .ih A ) ) )