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 29554 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 10523 | . . . 4 class ℂ | |
3 | 1, 2 | wcel 2105 | . . 3 wff 𝐴 ∈ ℂ |
4 | cB | . . . 4 class 𝐵 | |
5 | chba 28623 | . . . 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 28625 | . . . . 5 class ·ℎ | |
11 | 1, 4, 10 | co 7145 | . . . 4 class (𝐴 ·ℎ 𝐵) |
12 | csp 28626 | . . . 4 class ·ih | |
13 | 11, 7, 12 | co 7145 | . . 3 class ((𝐴 ·ℎ 𝐵) ·ih 𝐶) |
14 | 4, 7, 12 | co 7145 | . . . 4 class (𝐵 ·ih 𝐶) |
15 | cmul 10530 | . . . 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 28790 his35 28792 hiassdi 28795 his2sub 28796 hi01 28800 normlem0 28813 normlem9 28822 bcseqi 28824 polid2i 28861 ocsh 28987 h1de2i 29257 normcan 29280 eigrei 29538 eigorthi 29541 bramul 29650 lnopunilem1 29714 hmopm 29725 riesz3i 29766 cnlnadjlem2 29772 adjmul 29796 branmfn 29809 kbass2 29821 kbass5 29824 leopmuli 29837 leopnmid 29842 |
Copyright terms: Public domain | W3C validator |