![]() |
Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > HSE Home > Th. List > ax-his3 | Structured version Visualization version GIF version |
Description: Associative law for inner product. Postulate (S3) of [Beran] p. 95. Warning: Mathematics textbooks usually use our version of the axiom. Physics textbooks, on the other hand, usually replace the left-hand side with (𝐵 ·ih (𝐴 ·ℎ 𝐶)) (e.g., Equation 1.21b of [Hughes] p. 44; Definition (iii) of [ReedSimon] p. 36). See the comments in df-bra 29253 for why the physics definition is swapped. (Contributed by NM, 29-May-1999.) (New usage is discouraged.) |
Ref | Expression |
---|---|
ax-his3 | ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . . 4 class 𝐴 | |
2 | cc 10250 | . . . 4 class ℂ | |
3 | 1, 2 | wcel 2164 | . . 3 wff 𝐴 ∈ ℂ |
4 | cB | . . . 4 class 𝐵 | |
5 | chba 28320 | . . . 4 class ℋ | |
6 | 4, 5 | wcel 2164 | . . 3 wff 𝐵 ∈ ℋ |
7 | cC | . . . 4 class 𝐶 | |
8 | 7, 5 | wcel 2164 | . . 3 wff 𝐶 ∈ ℋ |
9 | 3, 6, 8 | w3a 1111 | . 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) |
10 | csm 28322 | . . . . 5 class ·ℎ | |
11 | 1, 4, 10 | co 6905 | . . . 4 class (𝐴 ·ℎ 𝐵) |
12 | csp 28323 | . . . 4 class ·ih | |
13 | 11, 7, 12 | co 6905 | . . 3 class ((𝐴 ·ℎ 𝐵) ·ih 𝐶) |
14 | 4, 7, 12 | co 6905 | . . . 4 class (𝐵 ·ih 𝐶) |
15 | cmul 10257 | . . . 4 class · | |
16 | 1, 14, 15 | co 6905 | . . 3 class (𝐴 · (𝐵 ·ih 𝐶)) |
17 | 13, 16 | wceq 1656 | . 2 wff ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶)) |
18 | 9, 17 | wi 4 | 1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶))) |
Colors of variables: wff setvar class |
This axiom is referenced by: his5 28487 his35 28489 hiassdi 28492 his2sub 28493 hi01 28497 normlem0 28510 normlem9 28519 bcseqi 28521 polid2i 28558 ocsh 28686 h1de2i 28956 normcan 28979 eigrei 29237 eigorthi 29240 bramul 29349 lnopunilem1 29413 hmopm 29424 riesz3i 29465 cnlnadjlem2 29471 adjmul 29495 branmfn 29508 kbass2 29520 kbass5 29523 leopmuli 29536 leopnmid 29541 |
Copyright terms: Public domain | W3C validator |