This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 ) ) )