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 28709 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 9934 | . . . 4 class ℂ | |
3 | 1, 2 | wcel 1990 | . . 3 wff 𝐴 ∈ ℂ |
4 | cB | . . . 4 class 𝐵 | |
5 | chil 27776 | . . . 4 class ℋ | |
6 | 4, 5 | wcel 1990 | . . 3 wff 𝐵 ∈ ℋ |
7 | cC | . . . 4 class 𝐶 | |
8 | 7, 5 | wcel 1990 | . . 3 wff 𝐶 ∈ ℋ |
9 | 3, 6, 8 | w3a 1037 | . 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) |
10 | csm 27778 | . . . . 5 class ·ℎ | |
11 | 1, 4, 10 | co 6650 | . . . 4 class (𝐴 ·ℎ 𝐵) |
12 | csp 27779 | . . . 4 class ·ih | |
13 | 11, 7, 12 | co 6650 | . . 3 class ((𝐴 ·ℎ 𝐵) ·ih 𝐶) |
14 | 4, 7, 12 | co 6650 | . . . 4 class (𝐵 ·ih 𝐶) |
15 | cmul 9941 | . . . 4 class · | |
16 | 1, 14, 15 | co 6650 | . . 3 class (𝐴 · (𝐵 ·ih 𝐶)) |
17 | 13, 16 | wceq 1483 | . 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 27943 his35 27945 hiassdi 27948 his2sub 27949 hi01 27953 normlem0 27966 normlem9 27975 bcseqi 27977 polid2i 28014 ocsh 28142 h1de2i 28412 normcan 28435 eigrei 28693 eigorthi 28696 bramul 28805 lnopunilem1 28869 hmopm 28880 riesz3i 28921 cnlnadjlem2 28927 adjmul 28951 branmfn 28964 kbass2 28976 kbass5 28979 leopmuli 28992 leopnmid 28997 |
Copyright terms: Public domain | W3C validator |