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 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 \mathscr{H}\wedge B\in \mathscr{H}\right)\to A{\cdot }_{\mathrm{ih}}B=\overline{B{\cdot }_{\mathrm{ih}}A}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1		chba	$$class\mathscr{H}$$
2	0 1	wcel	$$wffA\in \mathscr{H}$$
3		cB	$$classB$$
4	3 1	wcel	$$wffB\in \mathscr{H}$$
5	2 4	wa	$$wff\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\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\overline{B{\cdot }_{\mathrm{ih}}A}$$
11	7 10	wceq	$$wffA{\cdot }_{\mathrm{ih}}B=\overline{B{\cdot }_{\mathrm{ih}}A}$$
12	5 11	wi	$$wff\left(\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to A{\cdot }_{\mathrm{ih}}B=\overline{B{\cdot }_{\mathrm{ih}}A}\right)$$