# 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 ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to {A}{\cdot }_{\mathrm{ih}}{B}=\stackrel{‾}{{B}{\cdot }_{\mathrm{ih}}{A}}$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cA ${class}{A}$
1 chba ${class}ℋ$
2 0 1 wcel ${wff}{A}\in ℋ$
3 cB ${class}{B}$
4 3 1 wcel ${wff}{B}\in ℋ$
5 2 4 wa ${wff}\left({A}\in ℋ\wedge {B}\in ℋ\right)$
6 csp ${class}{\cdot }_{\mathrm{ih}}$
7 0 3 6 co ${class}\left({A}{\cdot }_{\mathrm{ih}}{B}\right)$
8 ccj ${class}*$
9 3 0 6 co ${class}\left({B}{\cdot }_{\mathrm{ih}}{A}\right)$
10 9 8 cfv ${class}\stackrel{‾}{{B}{\cdot }_{\mathrm{ih}}{A}}$
11 7 10 wceq ${wff}{A}{\cdot }_{\mathrm{ih}}{B}=\stackrel{‾}{{B}{\cdot }_{\mathrm{ih}}{A}}$
12 5 11 wi ${wff}\left(\left({A}\in ℋ\wedge {B}\in ℋ\right)\to {A}{\cdot }_{\mathrm{ih}}{B}=\stackrel{‾}{{B}{\cdot }_{\mathrm{ih}}{A}}\right)$