![]() |
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 29049 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 10136 | . . . 4 class ℂ | |
3 | 1, 2 | wcel 2145 | . . 3 wff 𝐴 ∈ ℂ |
4 | cB | . . . 4 class 𝐵 | |
5 | chil 28116 | . . . 4 class ℋ | |
6 | 4, 5 | wcel 2145 | . . 3 wff 𝐵 ∈ ℋ |
7 | cC | . . . 4 class 𝐶 | |
8 | 7, 5 | wcel 2145 | . . 3 wff 𝐶 ∈ ℋ |
9 | 3, 6, 8 | w3a 1071 | . 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) |
10 | csm 28118 | . . . . 5 class ·ℎ | |
11 | 1, 4, 10 | co 6793 | . . . 4 class (𝐴 ·ℎ 𝐵) |
12 | csp 28119 | . . . 4 class ·ih | |
13 | 11, 7, 12 | co 6793 | . . 3 class ((𝐴 ·ℎ 𝐵) ·ih 𝐶) |
14 | 4, 7, 12 | co 6793 | . . . 4 class (𝐵 ·ih 𝐶) |
15 | cmul 10143 | . . . 4 class · | |
16 | 1, 14, 15 | co 6793 | . . 3 class (𝐴 · (𝐵 ·ih 𝐶)) |
17 | 13, 16 | wceq 1631 | . 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 28283 his35 28285 hiassdi 28288 his2sub 28289 hi01 28293 normlem0 28306 normlem9 28315 bcseqi 28317 polid2i 28354 ocsh 28482 h1de2i 28752 normcan 28775 eigrei 29033 eigorthi 29036 bramul 29145 lnopunilem1 29209 hmopm 29220 riesz3i 29261 cnlnadjlem2 29267 adjmul 29291 branmfn 29304 kbass2 29316 kbass5 29319 leopmuli 29332 leopnmid 29337 |
Copyright terms: Public domain | W3C validator |