![]() |
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 15089 of ๐ฅ. In the literature, the inner product of ๐ด and ๐ต is usually written โจ๐ด, ๐ตโฉ, but our operation notation co 7426 allows to use existing theorems about operations and also avoids a clash with the definition of an ordered pair df-op 4639. Physicists use โจ๐ต โฃ ๐ดโฉ, called Dirac bra-ket notation, to represent this operation; see comments in df-bra 31680. (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 30749 | . . . 4 class โ | |
3 | 1, 2 | wcel 2098 | . . 3 wff ๐ด โ โ |
4 | cB | . . . 4 class ๐ต | |
5 | 4, 2 | wcel 2098 | . . 3 wff ๐ต โ โ |
6 | 3, 5 | wa 394 | . 2 wff (๐ด โ โ โง ๐ต โ โ) |
7 | csp 30752 | . . . 4 class ยทih | |
8 | 1, 4, 7 | co 7426 | . . 3 class (๐ด ยทih ๐ต) |
9 | 4, 1, 7 | co 7426 | . . . 4 class (๐ต ยทih ๐ด) |
10 | ccj 15083 | . . . 4 class โ | |
11 | 9, 10 | cfv 6553 | . . 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 30916 his7 30920 his2sub2 30923 hire 30924 hi02 30927 his1i 30930 abshicom 30931 hial2eq2 30937 orthcom 30938 adjsym 31663 cnvadj 31722 adj2 31764 |
Copyright terms: Public domain | W3C validator |