HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  ax-his3 Structured version   Visualization version   GIF version

Axiom ax-his3 27107
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 27875 for why the physics definition is swapped. (Contributed by NM, 29-May-1999.) (New usage is discouraged.)
Assertion
Ref Expression
ax-his3 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶)))

Detailed syntax breakdown of Axiom ax-his3
StepHypRef Expression
1 cA . . . 4 class 𝐴
2 cc 9693 . . . 4 class
31, 2wcel 1938 . . 3 wff 𝐴 ∈ ℂ
4 cB . . . 4 class 𝐵
5 chil 26942 . . . 4 class
64, 5wcel 1938 . . 3 wff 𝐵 ∈ ℋ
7 cC . . . 4 class 𝐶
87, 5wcel 1938 . . 3 wff 𝐶 ∈ ℋ
93, 6, 8w3a 1030 . 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ)
10 csm 26944 . . . . 5 class ·
111, 4, 10co 6431 . . . 4 class (𝐴 · 𝐵)
12 csp 26945 . . . 4 class ·ih
1311, 7, 12co 6431 . . 3 class ((𝐴 · 𝐵) ·ih 𝐶)
144, 7, 12co 6431 . . . 4 class (𝐵 ·ih 𝐶)
15 cmul 9700 . . . 4 class ·
161, 14, 15co 6431 . . 3 class (𝐴 · (𝐵 ·ih 𝐶))
1713, 16wceq 1474 . 2 wff ((𝐴 · 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶))
189, 17wi 4 1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶)))
Colors of variables: wff setvar class
This axiom is referenced by:  his5  27109  his35  27111  hiassdi  27114  his2sub  27115  hi01  27119  normlem0  27132  normlem9  27141  bcseqi  27143  polid2i  27180  ocsh  27308  h1de2i  27578  normcan  27601  eigrei  27859  eigorthi  27862  bramul  27971  lnopunilem1  28035  hmopm  28046  riesz3i  28087  cnlnadjlem2  28093  adjmul  28117  branmfn  28130  kbass2  28142  kbass5  28145  leopmuli  28158  leopnmid  28163
  Copyright terms: Public domain W3C validator