| 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 31869 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 11153 | . . . 4 class ℂ | |
| 3 | 1, 2 | wcel 2108 | . . 3 wff 𝐴 ∈ ℂ |
| 4 | cB | . . . 4 class 𝐵 | |
| 5 | chba 30938 | . . . 4 class ℋ | |
| 6 | 4, 5 | wcel 2108 | . . 3 wff 𝐵 ∈ ℋ |
| 7 | cC | . . . 4 class 𝐶 | |
| 8 | 7, 5 | wcel 2108 | . . 3 wff 𝐶 ∈ ℋ |
| 9 | 3, 6, 8 | w3a 1087 | . 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) |
| 10 | csm 30940 | . . . . 5 class ·ℎ | |
| 11 | 1, 4, 10 | co 7431 | . . . 4 class (𝐴 ·ℎ 𝐵) |
| 12 | csp 30941 | . . . 4 class ·ih | |
| 13 | 11, 7, 12 | co 7431 | . . 3 class ((𝐴 ·ℎ 𝐵) ·ih 𝐶) |
| 14 | 4, 7, 12 | co 7431 | . . . 4 class (𝐵 ·ih 𝐶) |
| 15 | cmul 11160 | . . . 4 class · | |
| 16 | 1, 14, 15 | co 7431 | . . 3 class (𝐴 · (𝐵 ·ih 𝐶)) |
| 17 | 13, 16 | wceq 1540 | . 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 31105 his35 31107 hiassdi 31110 his2sub 31111 hi01 31115 normlem0 31128 normlem9 31137 bcseqi 31139 polid2i 31176 ocsh 31302 h1de2i 31572 normcan 31595 eigrei 31853 eigorthi 31856 bramul 31965 lnopunilem1 32029 hmopm 32040 riesz3i 32081 cnlnadjlem2 32087 adjmul 32111 branmfn 32124 kbass2 32136 kbass5 32139 leopmuli 32152 leopnmid 32157 |
| Copyright terms: Public domain | W3C validator |