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 29555 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 10524 | . . . 4 class ℂ | |
3 | 1, 2 | wcel 2105 | . . 3 wff 𝐴 ∈ ℂ |
4 | cB | . . . 4 class 𝐵 | |
5 | chba 28624 | . . . 4 class ℋ | |
6 | 4, 5 | wcel 2105 | . . 3 wff 𝐵 ∈ ℋ |
7 | cC | . . . 4 class 𝐶 | |
8 | 7, 5 | wcel 2105 | . . 3 wff 𝐶 ∈ ℋ |
9 | 3, 6, 8 | w3a 1079 | . 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) |
10 | csm 28626 | . . . . 5 class ·ℎ | |
11 | 1, 4, 10 | co 7145 | . . . 4 class (𝐴 ·ℎ 𝐵) |
12 | csp 28627 | . . . 4 class ·ih | |
13 | 11, 7, 12 | co 7145 | . . 3 class ((𝐴 ·ℎ 𝐵) ·ih 𝐶) |
14 | 4, 7, 12 | co 7145 | . . . 4 class (𝐵 ·ih 𝐶) |
15 | cmul 10531 | . . . 4 class · | |
16 | 1, 14, 15 | co 7145 | . . 3 class (𝐴 · (𝐵 ·ih 𝐶)) |
17 | 13, 16 | wceq 1528 | . 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 28791 his35 28793 hiassdi 28796 his2sub 28797 hi01 28801 normlem0 28814 normlem9 28823 bcseqi 28825 polid2i 28862 ocsh 28988 h1de2i 29258 normcan 29281 eigrei 29539 eigorthi 29542 bramul 29651 lnopunilem1 29715 hmopm 29726 riesz3i 29767 cnlnadjlem2 29773 adjmul 29797 branmfn 29810 kbass2 29822 kbass5 29825 leopmuli 29838 leopnmid 29843 |
Copyright terms: Public domain | W3C validator |