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 \in ℋ \land B \in ℋ) \to A \cdot_{ih} B = \overline{B \cdot_{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 (A \in ℋ \land B \in ℋ)$
6		csp	$class \cdot_{ih}$
7	0 3 6	co	$class (A \cdot_{ih} B)$
8		ccj	$class *$
9	3 0 6	co	$class (B \cdot_{ih} A)$
10	9 8	cfv	$class \overline{B \cdot_{ih} A}$
11	7 10	wceq	$wff A \cdot_{ih} B = \overline{B \cdot_{ih} A}$
12	5 11	wi	$wff ((A \in ℋ \land B \in ℋ) \to A \cdot_{ih} B = \overline{B \cdot_{ih} A})$

Metamath Proof Explorer

Axiom ax-his1

Detailed syntax breakdown