![]() |
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 31068 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 11095 | . . . 4 class ℂ | |
3 | 1, 2 | wcel 2107 | . . 3 wff 𝐴 ∈ ℂ |
4 | cB | . . . 4 class 𝐵 | |
5 | chba 30137 | . . . 4 class ℋ | |
6 | 4, 5 | wcel 2107 | . . 3 wff 𝐵 ∈ ℋ |
7 | cC | . . . 4 class 𝐶 | |
8 | 7, 5 | wcel 2107 | . . 3 wff 𝐶 ∈ ℋ |
9 | 3, 6, 8 | w3a 1088 | . 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) |
10 | csm 30139 | . . . . 5 class ·ℎ | |
11 | 1, 4, 10 | co 7396 | . . . 4 class (𝐴 ·ℎ 𝐵) |
12 | csp 30140 | . . . 4 class ·ih | |
13 | 11, 7, 12 | co 7396 | . . 3 class ((𝐴 ·ℎ 𝐵) ·ih 𝐶) |
14 | 4, 7, 12 | co 7396 | . . . 4 class (𝐵 ·ih 𝐶) |
15 | cmul 11102 | . . . 4 class · | |
16 | 1, 14, 15 | co 7396 | . . 3 class (𝐴 · (𝐵 ·ih 𝐶)) |
17 | 13, 16 | wceq 1542 | . 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 30304 his35 30306 hiassdi 30309 his2sub 30310 hi01 30314 normlem0 30327 normlem9 30336 bcseqi 30338 polid2i 30375 ocsh 30501 h1de2i 30771 normcan 30794 eigrei 31052 eigorthi 31055 bramul 31164 lnopunilem1 31228 hmopm 31239 riesz3i 31280 cnlnadjlem2 31286 adjmul 31310 branmfn 31323 kbass2 31335 kbass5 31338 leopmuli 31351 leopnmid 31356 |
Copyright terms: Public domain | W3C validator |