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 28093 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 9813 | . . . 4 class ℂ | |
3 | 1, 2 | wcel 1977 | . . 3 wff 𝐴 ∈ ℂ |
4 | cB | . . . 4 class 𝐵 | |
5 | chil 27160 | . . . 4 class ℋ | |
6 | 4, 5 | wcel 1977 | . . 3 wff 𝐵 ∈ ℋ |
7 | cC | . . . 4 class 𝐶 | |
8 | 7, 5 | wcel 1977 | . . 3 wff 𝐶 ∈ ℋ |
9 | 3, 6, 8 | w3a 1031 | . 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) |
10 | csm 27162 | . . . . 5 class ·ℎ | |
11 | 1, 4, 10 | co 6549 | . . . 4 class (𝐴 ·ℎ 𝐵) |
12 | csp 27163 | . . . 4 class ·ih | |
13 | 11, 7, 12 | co 6549 | . . 3 class ((𝐴 ·ℎ 𝐵) ·ih 𝐶) |
14 | 4, 7, 12 | co 6549 | . . . 4 class (𝐵 ·ih 𝐶) |
15 | cmul 9820 | . . . 4 class · | |
16 | 1, 14, 15 | co 6549 | . . 3 class (𝐴 · (𝐵 ·ih 𝐶)) |
17 | 13, 16 | wceq 1475 | . 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 27327 his35 27329 hiassdi 27332 his2sub 27333 hi01 27337 normlem0 27350 normlem9 27359 bcseqi 27361 polid2i 27398 ocsh 27526 h1de2i 27796 normcan 27819 eigrei 28077 eigorthi 28080 bramul 28189 lnopunilem1 28253 hmopm 28264 riesz3i 28305 cnlnadjlem2 28311 adjmul 28335 branmfn 28348 kbass2 28360 kbass5 28363 leopmuli 28376 leopnmid 28381 |
Copyright terms: Public domain | W3C validator |