![]() |
Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > HSE Home > Th. List > ax-his1 | Structured version Visualization version GIF version |
Description: Conjugate law for inner product. Postulate (S1) of [Beran] p. 95. Note that โโ๐ฅ is the complex conjugate cjval 15052 of ๐ฅ. In the literature, the inner product of ๐ด and ๐ต is usually written โจ๐ด, ๐ตโฉ, but our operation notation co 7404 allows to use existing theorems about operations and also avoids a clash with the definition of an ordered pair df-op 4630. Physicists use โจ๐ต โฃ ๐ดโฉ, called Dirac bra-ket notation, to represent this operation; see comments in df-bra 31607. (Contributed by NM, 29-Jul-1999.) (New usage is discouraged.) |
Ref | Expression |
---|---|
ax-his1 | โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด ยทih ๐ต) = (โโ(๐ต ยทih ๐ด))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . . 4 class ๐ด | |
2 | chba 30676 | . . . 4 class โ | |
3 | 1, 2 | wcel 2098 | . . 3 wff ๐ด โ โ |
4 | cB | . . . 4 class ๐ต | |
5 | 4, 2 | wcel 2098 | . . 3 wff ๐ต โ โ |
6 | 3, 5 | wa 395 | . 2 wff (๐ด โ โ โง ๐ต โ โ) |
7 | csp 30679 | . . . 4 class ยทih | |
8 | 1, 4, 7 | co 7404 | . . 3 class (๐ด ยทih ๐ต) |
9 | 4, 1, 7 | co 7404 | . . . 4 class (๐ต ยทih ๐ด) |
10 | ccj 15046 | . . . 4 class โ | |
11 | 9, 10 | cfv 6536 | . . 3 class (โโ(๐ต ยทih ๐ด)) |
12 | 8, 11 | wceq 1533 | . 2 wff (๐ด ยทih ๐ต) = (โโ(๐ต ยทih ๐ด)) |
13 | 6, 12 | wi 4 | 1 wff ((๐ด โ โ โง ๐ต โ โ) โ (๐ด ยทih ๐ต) = (โโ(๐ต ยทih ๐ด))) |
Colors of variables: wff setvar class |
This axiom is referenced by: his5 30843 his7 30847 his2sub2 30850 hire 30851 hi02 30854 his1i 30857 abshicom 30858 hial2eq2 30864 orthcom 30865 adjsym 31590 cnvadj 31649 adj2 31691 |
Copyright terms: Public domain | W3C validator |