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 ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ ) โ†’ ( ๐ด ยทih ๐ต ) = ( โˆ— โ€˜ ( ๐ต ยทih ๐ด ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA โŠข ๐ด
1 chba โŠข โ„‹
2 0 1 wcel โŠข ๐ด โˆˆ โ„‹
3 cB โŠข ๐ต
4 3 1 wcel โŠข ๐ต โˆˆ โ„‹
5 2 4 wa โŠข ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ )
6 csp โŠข ยทih
7 0 3 6 co โŠข ( ๐ด ยทih ๐ต )
8 ccj โŠข โˆ—
9 3 0 6 co โŠข ( ๐ต ยทih ๐ด )
10 9 8 cfv โŠข ( โˆ— โ€˜ ( ๐ต ยทih ๐ด ) )
11 7 10 wceq โŠข ( ๐ด ยทih ๐ต ) = ( โˆ— โ€˜ ( ๐ต ยทih ๐ด ) )
12 5 11 wi โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ ) โ†’ ( ๐ด ยทih ๐ต ) = ( โˆ— โ€˜ ( ๐ต ยทih ๐ด ) ) )